# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1669861875 -32400
# Node ID 2da8dcbb0825b9d1c34865c10c8f7546744c024d
# Parent  382680c3e9be4490b8c4bac895df5ca28eda3048
ch-init again, because ch-is-sup require u<x which is not valid supf o∅

diff -r 382680c3e9be -r 2da8dcbb0825 src/zorn.agda
--- a/src/zorn.agda	Wed Nov 30 20:43:01 2022 +0900
+++ b/src/zorn.agda	Thu Dec 01 11:31:15 2022 +0900
@@ -286,23 +286,16 @@
 ∈∧P→o< :  {A : HOD } {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A
 ∈∧P→o< {A } {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p )))
 
--- Union of supf z which o< x
---
--- UnionCF : ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y )
---     ( supf : Ordinal → Ordinal ) ( x : Ordinal ) → HOD
--- UnionCF A f supf x
---    = record { od = record { def = λ z → odef A z ∧ UChain A f supf x z } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
+-- Union of supf z and FClosure A f y 
 
---      order : {x y w : Ordinal } → x o< y → FClosure A f (supf x) w → w ≤ supf y
---
+data UChain  { A : HOD } { f : Ordinal → Ordinal }  {supf : Ordinal → Ordinal} {y : Ordinal } (ay : odef A y ) 
+       (x : Ordinal) : (z : Ordinal) → Set n where
+    ch-init : {z : Ordinal } (fc : FClosure A f y z) → UChain ay x z
+    ch-is-sup  : (u : Ordinal) {z : Ordinal }  (u<x : u o< x) (supu=u : supf u ≡ u) ( fc : FClosure A f (supf u) z ) → UChain ay x z
 
-data UChain  { A : HOD } { f : Ordinal → Ordinal }  
-       {supf : Ordinal → Ordinal} (x : Ordinal) : (z : Ordinal) → Set n where
-    ch-is-sup  : (u : Ordinal) {z : Ordinal }  (u<x : u o< x) (supu=u : supf u ≡ u) ( fc : FClosure A f (supf u) z ) → UChain x z
-
-UnionCF : ( A : HOD )    ( f : Ordinal → Ordinal )  ( supf : Ordinal → Ordinal ) ( x : Ordinal ) → HOD
-UnionCF A f supf x
-   = record { od = record { def = λ z → odef A z ∧ UChain {A} {f} {supf} x z } ;   
+UnionCF : ( A : HOD )    ( f : Ordinal → Ordinal ) {y : Ordinal } (ay : odef A y ) ( supf : Ordinal → Ordinal ) ( x : Ordinal ) → HOD
+UnionCF A f ay supf x
+   = record { od = record { def = λ z → odef A z ∧ UChain {A} {f} {supf} ay x z } ;   
        odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
 
 
@@ -335,11 +328,11 @@
 
 M→S  : { A : HOD } { f : Ordinal → Ordinal } {mf : ≤-monotonic-f A f} {y : Ordinal} {ay : odef A y}  { x : Ordinal }
       →  (supf : Ordinal → Ordinal )
-      →  MinSUP A (UnionCF A f supf x)
-      → SUP A (UnionCF A f supf x)
+      →  MinSUP A (UnionCF A f ay supf x)
+      → SUP A (UnionCF A f ay supf x)
 M→S {A} {f} {mf} {y} {ay} {x} supf ms = record { sup = * (MinSUP.sup ms)
         ; isSUP = record { ax = subst (λ k → odef A k) (sym &iso) (MinSUP.as ms) ; x≤sup = ms00 } } where
-   ms00 :  {z : Ordinal} → odef (UnionCF A f supf x) z → (z ≡ & (* (MinSUP.sup ms))) ∨ (z << & (* (MinSUP.sup ms)))
+   ms00 :  {z : Ordinal} → odef (UnionCF A f ay supf x) z → (z ≡ & (* (MinSUP.sup ms))) ∨ (z << & (* (MinSUP.sup ms)))
    ms00 {z} uz with MinSUP.x≤sup ms uz
    ... | case1 eq = case1 (subst (λ k → z ≡ k) (sym &iso) eq)
    ... | case2 lt = case2  (subst (λ k →  * z < k ) (sym *iso) lt )
@@ -347,7 +340,8 @@
 
 chain-mono : {A : HOD}  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal )
    (supf-mono : {x y : Ordinal } →  x o≤  y  → supf x o≤ supf y ) {a b c : Ordinal} → a o≤ b
-        → odef (UnionCF A f supf a) c → odef (UnionCF A f supf b) c
+        → odef (UnionCF A f ay supf a) c → odef (UnionCF A f ay supf b) c
+chain-mono f mf ay supf supf-mono {a} {b} {c} a≤b ⟪ ua , ch-init fc ⟫ = ⟪ ua , ch-init fc ⟫ 
 chain-mono f mf ay supf supf-mono {a} {b} {c} a≤b ⟪ ua , ch-is-sup u u<x supu=u fc ⟫ = ⟪ ua , ch-is-sup u (ordtrans<-≤ u<x a≤b) supu=u fc ⟫ 
 
 record ZChain ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
@@ -355,38 +349,30 @@
    field
       supf :  Ordinal → Ordinal
 
+      order : {x y w : Ordinal } → x o< y → FClosure A f (supf x) w → w ≤ supf y
+
       cfcs : (mf< : <-monotonic-f A f)
-         {a b w : Ordinal } → a o< b → b o≤ z → supf a o< b  → FClosure A f (supf a) w → odef (UnionCF A f supf b) w
-      fcy<sup  : {w : Ordinal } → FClosure A f y w → (w ≡ supf o∅  ) ∨ ( w << supf o∅  ) 
-      order : {x y w : Ordinal } → x o< y → FClosure A f (supf x) w → w ≤ supf y
+         {a b w : Ordinal } → a o< b → b o≤ z → supf a o< b  → FClosure A f (supf a) w → odef (UnionCF A f ay supf b) w
 
       asupf :  {x : Ordinal } → odef A (supf x)
       supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
       supfmax : {x : Ordinal } → z o< x → supf x ≡ supf z
 
-      is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → IsMinSUP A (UnionCF A f supf x) (supf x) 
+      is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → IsMinSUP A (UnionCF A f ay supf x) (supf x) 
       sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z
-           → IsSUP A (UnionCF A f supf b) b ∧ (¬ HasPrev A (UnionCF A f supf b) f b ) → supf b ≡ b
+           → IsSUP A (UnionCF A f ay supf b) b ∧ (¬ HasPrev A (UnionCF A f ay supf b) f b ) → supf b ≡ b
 
    chain : HOD
-   chain = UnionCF A f supf z
+   chain = UnionCF A f ay supf z
    chain⊆A : chain ⊆' A
    chain⊆A = λ lt → proj1 lt
 
-   chain∋init : odef chain y
-   chain∋init = ⟪ ay , ?   ⟫
-   f-next : {a z : Ordinal} → odef (UnionCF A f supf z) a → odef (UnionCF A f supf z) (f a)
-   f-next {a} ⟪ aa , cp  ⟫ = ?
-   initial : {z : Ordinal } → odef chain z →  y ≤  z
-   initial {a} ⟪ aa , ua ⟫  = ?
-   f-total : IsTotalOrderSet chain
-   f-total {a} {b} ca cb = ?
-  -- subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
-  --     uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
-   --    uz01 with trio< (& a) (& b)
-   --    ... | tri> ¬a ¬b c = ?
-    --   ... | tri≈ ¬a b ¬c = ?
-     --  ... | tri< a ¬b ¬c = ? 
+   chain∋init : {x : Ordinal } → x o≤ z → odef (UnionCF A f ay supf x) y
+   chain∋init {x} x≤z = ⟪ ay , ch-init (init ay refl)  ⟫
+
+   f-next : {a z : Ordinal} → odef (UnionCF A f ay supf z) a → odef (UnionCF A f ay supf z) (f a)
+   f-next {a} ⟪ ua , ch-init fc ⟫ = ⟪ proj2 ( mf _ ua)  , ch-init (fsuc _ fc) ⟫ 
+   f-next {a} ⟪ ua , ch-is-sup u su<x su=u fc ⟫ = ⟪ proj2 ( mf _ ua)  , ch-is-sup u su<x su=u (fsuc _ fc) ⟫ 
 
    supf-inject : {x y : Ordinal } → supf x o< supf y → x o<  y
    supf-inject {x} {y} sx<sy with trio< x y
@@ -400,39 +386,56 @@
    supf<A = z09 asupf
 
    csupf : (mf< : <-monotonic-f A f) {b : Ordinal } 
-      → supf b o< supf z → supf b o< z → odef (UnionCF A f supf z) (supf b) -- supf z is not an element of this chain
+      → supf b o< supf z → supf b o< z → odef (UnionCF A f ay supf z) (supf b) -- supf z is not an element of this chain
    csupf mf< {b} sb<sz sb<z = cfcs mf< (supf-inject sb<sz) o≤-refl sb<z (init asupf refl)
 
-   minsup : {x : Ordinal } → x o≤ z  → MinSUP A (UnionCF A f supf x)
+   minsup : {x : Ordinal } → x o≤ z  → MinSUP A (UnionCF A f ay supf x)
    minsup {x} x≤z = record { sup = supf x ; isMinSUP = is-minsup x≤z }
 
    supf-is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ MinSUP.sup (minsup x≤z)
    supf-is-minsup _ = refl
 
-   chain-minsup : {x : Ordinal} → IsMinSUP A (UnionCF A f supf x) (supf x)
-   chain-minsup {x} = record { as = as ; x≤sup = cp1 ; minsup = cpm } where
-        as : odef A (supf x)
-        as = asupf
-        cp1 : {z : Ordinal} → odef (UnionCF A f supf x) z → (z ≡ supf x) ∨ (z << supf x)
-        cp1 {z} ⟪ az , ch-is-sup u u<x supu=u fc ⟫ = order u<x fc
-        cpm :  {s : Ordinal} → odef A s → ({z : Ordinal} → odef (UnionCF A f supf x) z → (z ≡ s) ∨ (z << s)) → supf x o≤ s 
-        cpm {s} as z≤s with trio< (supf x) s
-        ... | tri< a ¬b ¬c = o<→≤ a
-        ... | tri≈ ¬a b ¬c = o≤-refl0 b
-        ... | tri> ¬a ¬b c = ? where
-             cp4 : supf (supf s) ≡ supf s
-             cp4 = ?
-             cp3 : supf s o< x
-             cp3 = ?
-             cp2 : odef (UnionCF A f supf x) (supf s)
-             cp2 =  ⟪ asupf , ch-is-sup (supf s) cp3 cp4 (init asupf cp4)  ⟫
---        ... | case1 eq = ?
---        ... | case2 lt = ?
+   -- different from order because y o< supf
+   fcy<sup  : {u w : Ordinal } → u o≤ z  → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) 
+   fcy<sup  {u} {w} u≤z fc with MinSUP.x≤sup (minsup u≤z) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc)
+       , ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫
+   ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso  (trans eq (sym (supf-is-minsup u≤z ) ) ))
+   ... | case2 lt = case2 (subst₂ (λ j k → j << k ) &iso (sym (supf-is-minsup u≤z )) lt )
+
+   initial : {x : Ordinal } → x o≤ z → odef (UnionCF A f ay supf x) x →  y ≤ x
+   initial {x} x≤z ⟪ aa , ch-init fc ⟫ = s≤fc y f mf fc
+   initial {x} x≤z ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ = ≤-ftrans (fcy<sup (ordtrans u<x x≤z) (init ay refl)) (s≤fc _ f mf fc)  
+
+   f-total : IsTotalOrderSet chain
+   f-total {a} {b} ⟪ uaa , ch-is-sup ua sua<x sua=ua fca ⟫ ⟪ uab , ch-is-sup ub sub<x sub=ub fcb ⟫ =
+     subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso (fc-total A f mf supf order fca fcb)
+   f-total {a} {b} ⟪ uaa , ch-init fca ⟫ ⟪ uab , ch-is-sup ub sub<x sub=ub fcb ⟫ = ft00 where
+      ft01 : (& a) ≤ (& b) → Tri ( a <  b) ( a ≡  b) ( b <  a )
+      ft01 (case1 eq) = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym a=b)) lt)) a=b  (λ lt → ⊥-elim (<-irr (case1 a=b) lt))  where
+         a=b : a ≡ b 
+         a=b = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq)
+      ft01 (case2 lt) = tri< a<b (λ eq → <-irr (case1 (sym eq)) a<b ) (λ lt → <-irr (case2 a<b ) lt)  where
+         a<b : a < b 
+         a<b = subst₂ (λ j k → j < k ) *iso *iso lt
+      ft00 :   Tri ( a <  b) ( a ≡  b) ( b <  a )
+      ft00 = ft01 (≤-ftrans (fcy<sup (o<→≤ sub<x) fca) (s≤fc {A} _ f mf fcb))
+   f-total {a} {b} ⟪ uaa , ch-is-sup ua sua<x sua=ua fca ⟫ ⟪ uab , ch-init fcb ⟫ = ft00 where
+      ft01 : (& b) ≤ (& a) → Tri ( a <  b) ( a ≡  b) ( b <  a )
+      ft01 (case1 eq) = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym a=b)) lt)) a=b  (λ lt → ⊥-elim (<-irr (case1 a=b) lt))  where
+         a=b : a ≡ b 
+         a=b = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) (sym eq))
+      ft01 (case2 lt) = tri> (λ lt → <-irr (case2 b<a ) lt) (λ eq → <-irr (case1 eq) b<a ) b<a where
+         b<a : b < a 
+         b<a = subst₂ (λ j k → j < k ) *iso *iso lt
+      ft00 :   Tri ( a <  b) ( a ≡  b) ( b <  a )
+      ft00 = ft01 (≤-ftrans (fcy<sup (o<→≤ sua<x) fcb) (s≤fc {A} _ f mf fca))
+   f-total {a} {b} ⟪ uaa , ch-init fca ⟫ ⟪ uab , ch-init fcb ⟫ =  
+      subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso  (fcn-cmp y f mf fca fcb )
 
    IsMinSUP→NotHasPrev : {x sp : Ordinal } → odef A sp
-       → ({y : Ordinal} → odef (UnionCF A f supf x) y → (y ≡ sp ) ∨ (y << sp ))
+       → ({y : Ordinal} → odef (UnionCF A f ay supf x) y → (y ≡ sp ) ∨ (y << sp ))
        → ( {a : Ordinal } → odef A a → a << f a )
-       → ¬ ( HasPrev A (UnionCF A f supf x) f sp )
+       → ¬ ( HasPrev A (UnionCF A f ay supf x) f sp )
    IsMinSUP→NotHasPrev {x} {sp} asp is-sup <-mono-f hp = ⊥-elim (<<-irr fsp≤sp sp<fsp ) where
        sp<fsp : sp << f sp
        sp<fsp = <-mono-f asp
@@ -444,18 +447,19 @@
 
    supf-¬hp : {x  : Ordinal } → x o≤ z 
        → ( {a : Ordinal } → odef A a → a << f a )
-       → ¬ ( HasPrev A (UnionCF A f supf x) f (supf x) )
+       → ¬ ( HasPrev A (UnionCF A f ay supf x) f (supf x) )
    supf-¬hp {x} x≤z <-mono hp = IsMinSUP→NotHasPrev asupf (λ {w} uw → 
        (subst (λ k → w ≤ k) (sym (supf-is-minsup x≤z)) ( MinSUP.x≤sup (minsup x≤z) uw) )) <-mono hp
 
    supf-idem : (mf< : <-monotonic-f A f) {b : Ordinal } → b o≤ z → supf b o≤ z  → supf (supf b) ≡ supf b
    supf-idem  mf< {b} b≤z sfb≤x = z52 where
-       z54 :  {w : Ordinal} → odef (UnionCF A f supf (supf b)) w → (w ≡ supf b) ∨ (w << supf b)
+       z54 :  {w : Ordinal} → odef (UnionCF A f ay supf (supf b)) w → (w ≡ supf b) ∨ (w << supf b)
+       z54 {w} ⟪ aw , ch-init fc ⟫ = fcy<sup b≤z fc
        z54 {w} ⟪ aw , ch-is-sup u u<x su=u fc ⟫ = order su<b fc where
                su<b : u o< b
                su<b = supf-inject (subst (λ k → k o< supf b ) (sym (su=u)) u<x )
        z52 : supf (supf b) ≡ supf b
-       z52 = sup=u asupf sfb≤x ⟪ record { x≤sup = z54  } , IsMinSUP→NotHasPrev asupf z54 ( λ ax → proj1 (mf< _ ax)) ⟫ 
+       z52 = sup=u asupf sfb≤x ⟪ record { ax = asupf  ; x≤sup = z54  } , IsMinSUP→NotHasPrev asupf z54 ( λ ax → proj1 (mf< _ ax)) ⟫ 
 
    -- cp : (mf< : <-monotonic-f A f) {b : Ordinal } → b o≤ z → supf b o≤ z  → ChainP A f supf (supf b)
    --    the condition of cfcs is satisfied, this is obvious
@@ -464,9 +468,9 @@
         {y : Ordinal} (ay : odef A y)  (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
    supf = ZChain.supf zc
    field
-      is-max :  {a b : Ordinal } → (ca : odef (UnionCF A f supf z) a ) → b o< z  → (ab : odef A b)
-          → HasPrev A (UnionCF A f supf z) f b ∨  IsSUP A (UnionCF A f supf b) b
-          → * a < * b  → odef ((UnionCF A f supf z)) b
+      is-max :  {a b : Ordinal } → (ca : odef (UnionCF A f ay supf z) a ) → b o< z  → (ab : odef A b)
+          → HasPrev A (UnionCF A f ay supf z) f b ∨  IsSUP A (UnionCF A f ay supf b) b
+          → * a < * b  → odef ((UnionCF A f ay supf z)) b
 
 record Maximal ( A : HOD )  : Set (Level.suc n) where
    field
@@ -474,10 +478,6 @@
       as : A ∋ maximal
       ¬maximal<x : {x : HOD} → A ∋ x  → ¬ maximal < x       -- A is Partial, use negative
 
-init-uchain : (A : HOD)  ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } → (ay : odef A y )
-    { supf : Ordinal → Ordinal } { x : Ordinal } → odef (UnionCF A f supf x) y
-init-uchain A f mf ay = ⟪ ay , ?   ⟫
-
 record IChain  (A : HOD)  ( f : Ordinal → Ordinal ) {x : Ordinal } (supfz : {z : Ordinal } → z o< x → Ordinal) (z : Ordinal ) : Set n where
   field
      i : Ordinal  
@@ -513,7 +513,7 @@
                  spa ≡⟨ sym sax=spa ⟩ 
                  supfa x ∎ ) a ) where 
                     open o≤-Reasoning O
-                    z53 : {z : Ordinal } →  odef (UnionCF A f (ZChain.supf zb) x) z →  odef (UnionCF A f (ZChain.supf za) x) z
+                    z53 : {z : Ordinal } →  odef (UnionCF A f ay (ZChain.supf zb) x) z →  odef (UnionCF A f ay (ZChain.supf za) x) z
                     z53 {z} ⟪ as , cp ⟫ =  ⟪ as , ?  ⟫ 
            ... | tri> ¬a ¬b c = ⊥-elim ( o≤> (
                begin
@@ -522,13 +522,13 @@
                  spb  ≡⟨ sym sbx=spb ⟩
                  supfb x ∎ ) c ) where 
                     open o≤-Reasoning O
-                    z53 : {z : Ordinal } →  odef (UnionCF A f (ZChain.supf za) x) z →  odef (UnionCF A f (ZChain.supf zb) x) z
+                    z53 : {z : Ordinal } →  odef (UnionCF A f ay (ZChain.supf za) x) z →  odef (UnionCF A f ay (ZChain.supf zb) x) z
                     z53 {z} ⟪ as , cp ⟫ =  ⟪ as , ?  ⟫ 
 
 UChain-eq : { A : HOD }    { f : Ordinal → Ordinal }  {mf : ≤-monotonic-f A f}
         {z y : Ordinal} {ay : odef A y}  { supf0 supf1 : Ordinal → Ordinal }
         → (seq : {x : Ordinal } →  x o<  z  → supf0 x ≡ supf1 x )
-        → UnionCF A f supf0 z ≡ UnionCF A f supf1 z
+        → UnionCF A f ay supf0 z ≡ UnionCF A f ay supf1 z
 UChain-eq {A} {f} {mf} {z} {y} {ay} {supf0} {supf1} seq = ==→o≡  record { eq← = ueq← ; eq→ = ueq→ } where
       ueq← :  {x : Ordinal} → odef A x ∧ ? → odef A x ∧ ?
       ueq← {z} ⟪ ab , cp ⟫ = ⟪ ab , ? ⟫ 
@@ -646,11 +646,11 @@
         {init : Ordinal} (ay : odef A init) (zc : ZChain A f mf ay (& A)) (x : Ordinal) → x o≤ & A → ZChain1 A f mf ay zc x
      SZ1 f mf mf< {y} ay zc x x≤A = zc1 x x≤A  where
         chain-mono1 :  {a b c : Ordinal} → a o≤ b
-            → odef (UnionCF A f (ZChain.supf zc) a) c → odef (UnionCF A f (ZChain.supf zc) b) c
+            → odef (UnionCF A f ay (ZChain.supf zc) a) c → odef (UnionCF A f ay (ZChain.supf zc) b) c
         chain-mono1  {a} {b} {c} a≤b = chain-mono f mf ay (ZChain.supf zc) (ZChain.supf-mono zc) a≤b
-        is-max-hp : (x : Ordinal) {a : Ordinal} {b : Ordinal} → odef (UnionCF A f (ZChain.supf zc) x) a → (ab : odef A b)
-            → HasPrev A (UnionCF A f (ZChain.supf zc) x) f b
-            → * a < * b → odef (UnionCF A f (ZChain.supf zc) x) b
+        is-max-hp : (x : Ordinal) {a : Ordinal} {b : Ordinal} → odef (UnionCF A f ay (ZChain.supf zc) x) a → (ab : odef A b)
+            → HasPrev A (UnionCF A f ay (ZChain.supf zc) x) f b
+            → * a < * b → odef (UnionCF A f ay (ZChain.supf zc) x) b
         is-max-hp x {a} {b} ua ab has-prev a<b with HasPrev.ay has-prev
         ... | ⟪ ab0 , cp ⟫ = ⟪ ab , ? ⟫
 
@@ -660,25 +660,25 @@
         zc1 x x≤A with Oprev-p x  
         ... | yes op = record { is-max = is-max } where
                px = Oprev.oprev op
-               is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f supf x) a →
+               is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f ay supf x) a →
                   b o< x → (ab : odef A b) →
-                  HasPrev A (UnionCF A f supf x) f b  ∨ IsSUP A (UnionCF A f supf b) ? →
-                  * a < * b → odef (UnionCF A f supf x) b
+                  HasPrev A (UnionCF A f ay supf x) f b  ∨ IsSUP A (UnionCF A f ay supf b) ? →
+                  * a < * b → odef (UnionCF A f ay supf x) b
                is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P
                is-max {a} {b} ua b<x ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b
                is-max {a} {b} ua b<x ab P a<b | case2 is-sup with osuc-≡< (ZChain.supf-mono zc (o<→≤ b<x))
                ... | case2 sb<sx = m10 where
                   b<A : b o< & A
                   b<A = z09 ab
-                  m04 : ¬ HasPrev A (UnionCF A f supf b) f b
+                  m04 : ¬ HasPrev A (UnionCF A f ay supf b) f b
                   m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay =
                         chain-mono1 (o<→≤ b<x) (HasPrev.ay  nhp) ; x=fy = HasPrev.x=fy nhp } )
                   m05 : ZChain.supf zc b ≡ b
                   m05 =  ZChain.sup=u zc ab (o<→≤ (z09 ab) ) ⟪ record { x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz  }  , m04 ⟫
-                  m10 : odef (UnionCF A f supf x) b
+                  m10 : odef (UnionCF A f ay supf x) b
                   m10 = ZChain.cfcs zc mf< b<x x≤A (subst (λ k → k o< x) (sym m05) b<x) (init (ZChain.asupf zc) m05)
                ... | case1 sb=sx = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf b) (ZChain.asupf zc)))) where
-                  m17 : MinSUP A (UnionCF A f supf x) -- supf z o< supf ( supf x )
+                  m17 : MinSUP A (UnionCF A f ay supf x) -- supf z o< supf ( supf x )
                   m17 = ZChain.minsup zc x≤A
                   m18 : supf x ≡ MinSUP.sup m17 
                   m18 = ZChain.supf-is-minsup zc x≤A
@@ -686,39 +686,39 @@
                   m10 = fc-stop A f mf (ZChain.asupf zc) m11 sb=sx where
                       m11 : {z : Ordinal} → FClosure A f (supf b) z → (z ≡ ZChain.supf zc x) ∨ (z << ZChain.supf zc x)
                       m11 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (sym m18) ( MinSUP.x≤sup m17 m13 ) where
-                          m04 : ¬ HasPrev A (UnionCF A f supf b) f b
+                          m04 : ¬ HasPrev A (UnionCF A f ay supf b) f b
                           m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay =
                                 chain-mono1 (o<→≤ b<x) (HasPrev.ay  nhp) ; x=fy = HasPrev.x=fy nhp } )
                           m05 : ZChain.supf zc b ≡ b
                           m05 =  ZChain.sup=u zc ab (o<→≤ (z09 ab) ) ⟪ record { x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz  }  , m04 ⟫
                           m14 : ZChain.supf zc b o< x
                           m14 = subst (λ k → k o< x ) (sym m05)  b<x
-                          m13 :  odef (UnionCF A f supf x) z
+                          m13 :  odef (UnionCF A f ay supf x) z
                           m13 = ZChain.cfcs zc mf< b<x x≤A m14 fc
 
         ... | no lim = record { is-max = is-max }  where
-               is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f supf x) a →
+               is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f ay supf x) a →
                   b o< x → (ab : odef A b) →
-                  HasPrev A (UnionCF A f supf x) f b  ∨ IsSUP A (UnionCF A f supf b) b →
-                  * a < * b → odef (UnionCF A f supf x) b
+                  HasPrev A (UnionCF A f ay supf x) f b  ∨ IsSUP A (UnionCF A f ay supf b) b →
+                  * a < * b → odef (UnionCF A f ay supf x) b
                is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P
                is-max {a} {b} ua b<x ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b
-               is-max {a} {b} ua b<x ab P a<b | case2 is-sup with IsSUP.x≤sup (proj2 is-sup) (init-uchain A f mf ay )
+               is-max {a} {b} ua b<x ab P a<b | case2 is-sup with IsSUP.x≤sup (proj2 is-sup) (ZChain.chain∋init zc ? )
                ... | case1 b=y = ⟪ subst (λ k → odef A k ) b=y ay , ?  ⟫
                ... | case2 y<b with osuc-≡< (ZChain.supf-mono zc (o<→≤ b<x))
                ... | case2 sb<sx = m10 where
                   m09 : b o< & A
                   m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
-                  m04 : ¬ HasPrev A (UnionCF A f supf b) f b
+                  m04 : ¬ HasPrev A (UnionCF A f ay supf b) f b
                   m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay =
                           chain-mono1 (o<→≤ b<x) (HasPrev.ay  nhp)
                      ; x=fy = HasPrev.x=fy nhp } )
                   m05 : ZChain.supf zc b ≡ b
                   m05 = ZChain.sup=u zc ab (o<→≤  m09) ⟪ record { x≤sup = λ lt → IsSUP.x≤sup (proj2 is-sup) lt } , m04 ⟫    -- ZChain on x
-                  m10 : odef (UnionCF A f supf x) b
+                  m10 : odef (UnionCF A f ay supf x) b
                   m10 = ZChain.cfcs zc mf< b<x x≤A (subst (λ k → k o< x) (sym m05) b<x) (init (ZChain.asupf zc) m05)
                ... | case1 sb=sx = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf b) (ZChain.asupf zc)))) where
-                  m17 : MinSUP A (UnionCF A f supf x) -- supf z o< supf ( supf x )
+                  m17 : MinSUP A (UnionCF A f ay supf x) -- supf z o< supf ( supf x )
                   m17 = ZChain.minsup zc x≤A
                   m18 : supf x ≡ MinSUP.sup m17 
                   m18 = ZChain.supf-is-minsup zc x≤A
@@ -726,14 +726,14 @@
                   m10 = fc-stop A f mf (ZChain.asupf zc) m11 sb=sx where
                       m11 : {z : Ordinal} → FClosure A f (supf b) z → (z ≡ ZChain.supf zc x) ∨ (z << ZChain.supf zc x)
                       m11 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (sym m18) ( MinSUP.x≤sup m17 m13 ) where
-                          m04 : ¬ HasPrev A (UnionCF A f supf b) f b
+                          m04 : ¬ HasPrev A (UnionCF A f ay supf b) f b
                           m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay =
                                 chain-mono1 (o<→≤ b<x) (HasPrev.ay  nhp) ; x=fy = HasPrev.x=fy nhp } )
                           m05 : ZChain.supf zc b ≡ b
                           m05 =  ZChain.sup=u zc ab (o<→≤ (z09 ab) ) ⟪ record { x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz  }  , m04 ⟫
                           m14 : ZChain.supf zc b o< x
                           m14 = subst (λ k → k o< x ) (sym m05)  b<x
-                          m13 :  odef (UnionCF A f supf x) z
+                          m13 :  odef (UnionCF A f ay supf x) z
                           m13 = ZChain.cfcs zc mf< b<x x≤A m14 fc
 
      uchain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → HOD
@@ -784,7 +784,7 @@
 
           supf0 = ZChain.supf zc
           pchain  : HOD
-          pchain   = UnionCF A f supf0 px
+          pchain   = UnionCF A f ay supf0 px
 
           supf-mono : {a b : Ordinal } → a o≤ b → supf0 a o≤ supf0 b
           supf-mono = ZChain.supf-mono zc
@@ -893,18 +893,18 @@
                  ... | tri≈ ¬a b ¬c =  subst₂ (λ j k → j o≤ k ) (sym (sf1=sf0 (subst (λ k → a o≤ k) b a≤b))) refl ( supf-mono a≤b )
                  supf1-mono {a} {b} a≤b | tri> ¬a ¬b c with trio< a px
                  ... | tri< a<px ¬b ¬c = zc19 where
-                       zc21 : MinSUP A (UnionCF A f supf0 a)
+                       zc21 : MinSUP A (UnionCF A f ay supf0 a)
                        zc21 = ZChain.minsup zc (o<→≤ a<px)
-                       zc24 : {x₁ : Ordinal} → odef (UnionCF A f supf0 a) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1)
+                       zc24 : {x₁ : Ordinal} → odef (UnionCF A f ay supf0 a) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1)
                        zc24 {x₁} ux = MinSUP.x≤sup sup1 (case1 (chain-mono f mf ay supf0 (ZChain.supf-mono zc) (o<→≤ a<px) ux ) )
                        zc19 : supf0 a o≤ sp1
                        zc19 = subst (λ k → k o≤ sp1) (sym (ZChain.supf-is-minsup zc  (o<→≤ a<px))) ( MinSUP.minsup zc21 (MinSUP.as sup1) zc24 )
                  ... | tri≈ ¬a b ¬c = zc18 where
-                       zc21 : MinSUP A (UnionCF A f supf0 a)
+                       zc21 : MinSUP A (UnionCF A f ay supf0 a)
                        zc21 = ZChain.minsup zc (o≤-refl0 b)
                        zc20 : MinSUP.sup zc21 ≡ supf0 a
                        zc20 = sym (ZChain.supf-is-minsup zc (o≤-refl0 b))
-                       zc24 : {x₁ : Ordinal} → odef (UnionCF A f supf0 a) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1)
+                       zc24 : {x₁ : Ordinal} → odef (UnionCF A f ay supf0 a) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1)
                        zc24 {x₁} ux = MinSUP.x≤sup sup1 (case1 (chain-mono f mf ay supf0 (ZChain.supf-mono zc) (o≤-refl0 b) ux ) )
                        zc18 : supf0 a o≤ sp1
                        zc18 = subst (λ k → k o≤ sp1) zc20( MinSUP.minsup zc21 (MinSUP.as sup1) zc24 )
@@ -926,7 +926,7 @@
                  -- this is a kind of maximality, so we cannot prove this without <-monotonicity
                  --
                  cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal } 
-                     → a o< b → b o≤ x → supf1 a o< b  → FClosure A f (supf1 a) w → odef (UnionCF A f supf1 b) w
+                     → a o< b → b o≤ x → supf1 a o< b  → FClosure A f (supf1 a) w → odef (UnionCF A f ay supf1 b) w
                  cfcs mf< {a} {b} {w} a<b b≤x sa<b fc with zc43 (supf0 a) px
                  ... | case2 px≤sa = z50 where
                       a<x : a o< x
@@ -935,7 +935,7 @@
                       a≤px = subst (λ k → a o< k) (sym (Oprev.oprev=x op)) (ordtrans<-≤ a<b b≤x)
                       --  supf0 a ≡ px we cannot use previous cfcs, it is in the chain because
                       --       supf0 a ≡ supf0 (supf0 a) ≡ supf0 px o< x
-                      z50 : odef (UnionCF A f supf1 b) w
+                      z50 : odef (UnionCF A f ay supf1 b) w
                       z50 with osuc-≡< px≤sa
                       ... | case1 px=sa = ⟪ A∋fc {A} _ f mf fc , ?  ⟫ where
                           sa≤px : supf0 a o≤ px
@@ -955,7 +955,7 @@
                                 supf0 (supf0 a) ≡⟨ sym (sf1=sf0 sa≤px)  ⟩ 
                                 supf1 (supf0 a) ≡⟨ cong supf1 (sym spx=sa) ⟩ 
                                 supf1 (supf0 px) ∎ where open ≡-Reasoning
-                          m : MinSUP A (UnionCF A f supf0 px)
+                          m : MinSUP A (UnionCF A f ay supf0 px)
                           m = ZChain.minsup zc o≤-refl
                           m=spx : MinSUP.sup m ≡ supf1 (supf0 px)
                           m=spx = begin 
@@ -972,7 +972,7 @@
                                 supf0 px  ∎  where open ≡-Reasoning 
                           cp : ?
                           cp = ? where
-                             uz : {s z1 : Ordinal } → supf1 s o< supf1 (supf0 px) → FClosure A f (supf1 s) z1 → odef (UnionCF A f supf0 px) z1
+                             uz : {s z1 : Ordinal } → supf1 s o< supf1 (supf0 px) → FClosure A f (supf1 s) z1 → odef (UnionCF A f ay supf0 px) z1
                              uz {s} {z1} ss<sp fc = ZChain.cfcs zc mf< s<px o≤-refl ss<px (subst (λ k → FClosure A f k z1) 
                                      (sf1=sf0 (o<→≤ s<px))  fc ) where
                                 s<spx : s o< supf0 px
@@ -999,7 +999,7 @@
                           z53  = ordtrans<-≤ sa<b b≤x
                  ... | case1 sa<px with trio< a px
                  ... | tri< a<px ¬b ¬c = z50 where
-                      z50 : odef (UnionCF A f supf1 b) w
+                      z50 : odef (UnionCF A f ay supf1 b) w
                       z50 with osuc-≡< b≤x
                       ... | case2 lt with ZChain.cfcs zc mf< a<b (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt) sa<b fc  
                       ... | ⟪ az , cp ⟫ = ⟪ az , ?  ⟫  -- u o< px → u o< b ?
@@ -1018,7 +1018,7 @@
                       z51 = subst (λ k → FClosure A f k w) (sym (trans (cong supf1 (sym a=px)) (sf1=sf0 (o≤-refl0 a=px) ))) fc
                       z53 : odef A w
                       z53 = A∋fc {A} _ f mf fc
-                      csupf1 : odef (UnionCF A f supf1 b) w
+                      csupf1 : odef (UnionCF A f ay supf1 b) w
                       csupf1 with trio< (supf0 px) x
                       ... | tri< sfpx<x ¬b ¬c = ⟪ z53 , ? ⟫  where
                           spx = supf0 px
@@ -1056,7 +1056,7 @@
                       ... | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl (ordtrans<-≤ c (OrdTrans ? sp≤x)))   -- x o< supf0 px o≤ sp1 ≤ x
                  ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → a o< k ) (sym (Oprev.oprev=x op)) ( ordtrans<-≤ a<b b≤x) ⟫ ) --  px o< a o< b o≤ x
 
-                 zc11 : {z : Ordinal} → odef (UnionCF A f supf1 x) z → odef pchainpx z
+                 zc11 : {z : Ordinal} → odef (UnionCF A f ay supf1 x) z → odef pchainpx z
                  zc11 {z} ⟪ az , cp ⟫ = zc21 ? where
                     zc21 : {z1 : Ordinal } → FClosure A f (supf1 ?) z1 → odef pchainpx z1
                     zc21 {z1} (fsuc z2 fc ) with zc21 fc
@@ -1066,7 +1066,7 @@
 
                  record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where
                      field
-                         tsup : MinSUP A (UnionCF A f supf1 z)
+                         tsup : MinSUP A (UnionCF A f ay supf1 z)
                          tsup=sup : supf1 z ≡ MinSUP.sup tsup
 
                  sup : {z : Ordinal} → (z≤x : z o≤ x ) → STMP z≤x
@@ -1074,26 +1074,26 @@
                  ... | tri< a ¬b ¬c = record { tsup = record { sup = MinSUP.sup m  ; asm = MinSUP.as m
                          ; x≤sup = ms00 ; minsup = ms01 } ; tsup=sup = trans (sf1=sf0 (o<→≤ a) ) (ZChain.supf-is-minsup zc (o<→≤ a)) } where
                     m = ZChain.minsup zc (o<→≤ a)
-                    ms00 :  {x : Ordinal} → odef (UnionCF A f supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m)
+                    ms00 :  {x : Ordinal} → odef (UnionCF A f ay supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m)
                     ms00 {w} ⟪ az , cp ⟫ = MinSUP.x≤sup m ⟪ az , ? ⟫ 
                     ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} →
-                        odef (UnionCF A f supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2
+                        odef (UnionCF A f ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2
                     ms01 {sup2} us P = MinSUP.minsup m us ?
                  ... | tri≈ ¬a b ¬c = record { tsup = record { sup = MinSUP.sup m  ; asm = MinSUP.as m
                          ; x≤sup = ms00 ; minsup = ms01 } ; tsup=sup = trans (sf1=sf0 (o≤-refl0 b) ) (ZChain.supf-is-minsup zc (o≤-refl0 b))  } where
                     m = ZChain.minsup zc (o≤-refl0 b)
-                    ms00 :  {x : Ordinal} → odef (UnionCF A f supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m)
+                    ms00 :  {x : Ordinal} → odef (UnionCF A f ay supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m)
                     ms00 {x} ux = MinSUP.x≤sup m ?
                     ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} →
-                        odef (UnionCF A f supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2
+                        odef (UnionCF A f ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2
                     ms01 {sup2} us P = MinSUP.minsup m us ?
                  ... | tri> ¬a ¬b px<z = record { tsup = record { sup = sp1 ; asm = MinSUP.as sup1
                          ; x≤sup = ms00 ; minsup = ms01 } ; tsup=sup = sf1=sp1 px<z } where
                     m = sup1
-                    ms00 :  {x : Ordinal} → odef (UnionCF A f supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m)
+                    ms00 :  {x : Ordinal} → odef (UnionCF A f ay supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m)
                     ms00 {x} ux = MinSUP.x≤sup m ?
                     ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} →
-                        odef (UnionCF A f supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2
+                        odef (UnionCF A f ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2
                     ms01 {sup2} us P = MinSUP.minsup m us ?
 
 
@@ -1104,7 +1104,7 @@
                  --     supf1 x ≡ supf0 px because of supfmax
 
                  cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal } 
-                     → a o< b → b o≤ x →  supf0 a o< b → FClosure A f (supf0 a) w → odef (UnionCF A f supf0 b) w
+                     → a o< b → b o≤ x →  supf0 a o< b → FClosure A f (supf0 a) w → odef (UnionCF A f ay supf0 b) w
                  cfcs mf< {a} {b} {w} a<b b≤x sa<b fc with trio< b px 
                  ... | tri< a ¬b ¬c = ZChain.cfcs zc mf< a<b (o<→≤ a) sa<b fc
                  ... | tri≈ ¬a refl ¬c = ZChain.cfcs zc mf< a<b o≤-refl sa<b fc 
@@ -1120,7 +1120,7 @@
                      --      supf a ≡ px    -- a o< px → odef U w
                      --                        a ≡ px → supf px ≡ px → odef U w
 
-                     cfcs0 : a ≡ px → odef (UnionCF A f supf0 b) w
+                     cfcs0 : a ≡ px → odef (UnionCF A f ay supf0 b) w
                      cfcs0 a=px = ⟪  A∋fc {A} _ f mf fc , ? ⟫ where
                          spx<b : supf0 px o< b
                          spx<b = subst (λ k → supf0 k o< b) a=px sa<b
@@ -1129,7 +1129,7 @@
                               (subst (λ k → supf0 px o< k ) (sym (Oprev.oprev=x op)) (ordtrans<-≤ spx<b b≤x))))
                          fc1 : FClosure A f (supf0 (supf0 px)) w
                          fc1 = subst (λ k → FClosure A f k w) cs01 fc
-                         m : MinSUP A (UnionCF A f supf0 (supf0 px))
+                         m : MinSUP A (UnionCF A f ay supf0 (supf0 px))
                          m = ZChain.minsup zc (zc-b<x _ (ordtrans<-≤ spx<b b≤x))
                          m=sa : MinSUP.sup m ≡ supf0 (supf0 px)
                          m=sa = begin 
@@ -1137,12 +1137,12 @@
                                 supf0 (supf0 px)  ∎  where open ≡-Reasoning 
 
 
-                     cfcs1 : odef (UnionCF A f supf0 b) w
+                     cfcs1 : odef (UnionCF A f ay supf0 b) w
                      cfcs1 with trio< a px
                      ... | tri< a<px ¬b ¬c = cfcs2 where
                          sa<x : supf0 a o< x
                          sa<x = ordtrans<-≤ sa<b b≤x
-                         cfcs2 : odef (UnionCF A f supf0 b) w
+                         cfcs2 : odef (UnionCF A f ay supf0 b) w
                          cfcs2 with trio< (supf0 a) px
                          ... | tri< sa<x ¬b ¬c = chain-mono f mf ay (ZChain.supf zc) (ZChain.supf-mono zc) (o<→≤ px<b) 
                              ( ZChain.cfcs zc mf< a<px o≤-refl sa<x fc ) 
@@ -1153,7 +1153,7 @@
                               cs01 =  sym ( ZChain.supf-idem zc mf< (zc-b<x _ (ordtrans<-≤ a<b b≤x)) (zc-b<x _ (ordtrans<-≤ sa<b b≤x)))  
                               fc1 : FClosure A f (supf0 (supf0 a)) w
                               fc1 = subst (λ k → FClosure A f k w) cs01 fc
-                              m : MinSUP A (UnionCF A f supf0 (supf0 a))
+                              m : MinSUP A (UnionCF A f ay supf0 (supf0 a))
                               m = ZChain.minsup zc (o≤-refl0 sa=px)
                               m=sa : MinSUP.sup m ≡ supf0 (supf0 a)
                               m=sa = begin 
@@ -1172,12 +1172,12 @@
                       zc177 : supf0 z ≡ supf0 px
                       zc177 = ZChain.supfmax zc px<z  -- px o< z, px o< supf0 px
 
-                 zc11 : {z : Ordinal} → odef (UnionCF A f supf0 x) z → odef pchainpx z
+                 zc11 : {z : Ordinal} → odef (UnionCF A f ay supf0 x) z → odef pchainpx z
                  zc11 {z} ⟪ az , cp ⟫ = ? 
 
                  record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where
                      field
-                         tsup : MinSUP A (UnionCF A f supf0 z)
+                         tsup : MinSUP A (UnionCF A f ay supf0 z)
                          tsup=sup : supf0 z ≡ MinSUP.sup tsup
 
                  sup : {z : Ordinal} → (z≤x : z o≤ x ) → STMP z≤x
@@ -1190,7 +1190,7 @@
                      ... | case1 eq = eq
                      ... | case2 z<x = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ )
                      zc32 = ?
-                     zc34 : ¬ (supf0 px ≡ px) → {w : HOD} → UnionCF A f supf0 z ∋ w → (w ≡ SUP.sup zc32) ∨ (w < SUP.sup zc32)
+                     zc34 : ¬ (supf0 px ≡ px) → {w : HOD} → UnionCF A f ay supf0 z ∋ w → (w ≡ SUP.sup zc32) ∨ (w < SUP.sup zc32)
                      zc34 ne {w} lt = ?
                      zc33 : supf0 z ≡ & (SUP.sup zc32)
                      zc33 = ? -- trans (sym (supfx (o≤-refl0 (sym zc30)))) ( ZChain.supf-is-minsup zc o≤-refl  )
@@ -1201,10 +1201,10 @@
                      ... | tri< a ¬b ¬c = zc36 ¬b
                      ... | tri> ¬a ¬b c = zc36 ¬b
                      ... | tri≈ ¬a b ¬c = record { tsup = ? ; tsup=sup = ?  } where
-                          zc37 : MinSUP A (UnionCF A f supf0 z)
+                          zc37 : MinSUP A (UnionCF A f ay supf0 z)
                           zc37 = record { sup = ? ; asm = ? ; x≤sup = ? ; minsup = ? }
                  sup=u : {b : Ordinal} (ab : odef A b) →
-                    b o≤ x → IsMinSUP A (UnionCF A f supf0 b) b ∧ (¬ HasPrev A (UnionCF A f supf0 b) f b ) → supf0 b ≡ b
+                    b o≤ x → IsMinSUP A (UnionCF A f ay supf0 b) b ∧ (¬ HasPrev A (UnionCF A f ay supf0 b) f b ) → supf0 b ≡ b
                  sup=u {b} ab b≤x is-sup with trio< b px
                  ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) ⟪ record { x≤sup = λ lt → IsMinSUP.x≤sup (proj1 is-sup) lt } , ? ⟫
                  ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) ⟪ record { x≤sup = λ lt → IsMinSUP.x≤sup (proj1 is-sup) lt } , ? ⟫
@@ -1218,7 +1218,10 @@
                          zc32 : {w : Ordinal } → odef pchainpx w → (w ≡ b) ∨ (w << b) 
                          zc32 = ?
                      
-     ... | no lim = record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf-mono ; order = ?
+     ... | no lim with trio< x o∅
+     ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) 
+     ... | tri≈ ¬a b ¬c = record { supf = ? }
+     ... | tri> ¬a ¬b 0<x = record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf-mono ; order = ?
               ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; cfcs = cfcs    }  where
 
           pzc : {z : Ordinal} → z o< x → ZChain A f mf ay z
@@ -1279,7 +1282,7 @@
           ... | tri> ¬a ¬b c = spu
 
           pchain : HOD
-          pchain = UnionCF A f supf1 x
+          pchain = UnionCF A f ay supf1 x
 
           -- pchain ⊆ pchainx
 
@@ -1316,7 +1319,7 @@
           ... | tri> ¬a ¬b c = ?
 
           cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal } 
-                 → a o< b → b o≤ x →  supf1 a o< b → FClosure A f (supf1 a) w → odef (UnionCF A f supf1 b) w
+                 → a o< b → b o≤ x →  supf1 a o< b → FClosure A f (supf1 a) w → odef (UnionCF A f ay supf1 b) w
           cfcs mf< {a} {b} {w} a<b b≤x sa<b fc with osuc-≡< b≤x
           ... | case1 b=x with trio< a x 
           ... | tri< a<x ¬b ¬c = zc40 where
@@ -1340,9 +1343,9 @@
                sam<m = subst (λ k → k o< m ) (supf-unique A f mf ay zc42 (pzc (ob<x lim a<x)) (pzc (ob<x lim m<x)) (o<→≤ <-osuc)) ( omax-y _ _ )
                fcm : FClosure A f (ZChain.supf (pzc (ob<x lim m<x)) a) w
                fcm = subst (λ k → FClosure A f k w ) (zeq (ob<x lim a<x) (ob<x lim m<x) zc42 (o<→≤ <-osuc) ) fc
-               zcm : odef (UnionCF A f (ZChain.supf (pzc  (ob<x lim m<x))) (osuc (omax a sa))) w
+               zcm : odef (UnionCF A f ay (ZChain.supf (pzc  (ob<x lim m<x))) (osuc (omax a sa))) w
                zcm = ZChain.cfcs (pzc  (ob<x lim m<x)) mf< (o<→≤ (omax-x _ _)) o≤-refl (o<→≤ sam<m) fcm
-               zc40 : odef (UnionCF A f supf1 b) w
+               zc40 : odef (UnionCF A f ay supf1 b) w
                zc40 with ZChain.cfcs (pzc  (ob<x lim m<x)) mf< (o<→≤ (omax-x _ _)) o≤-refl (o<→≤ sam<m) fcm
                ... | ⟪ az , cp ⟫ = ⟪ az , ? ⟫  
           ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x))
@@ -1354,14 +1357,14 @@
                fcb : FClosure A f (supfb a) w
                fcb = subst (λ k → FClosure A f k w) (sb=sa a<b) fc 
                --  supfb a o< b assures it is in Union b
-               zcb : odef (UnionCF A f supfb b) w
+               zcb : odef (UnionCF A f ay supfb b) w
                zcb = ZChain.cfcs (pzc (ob<x lim b<x)) mf< a<b (o<→≤ <-osuc) (subst (λ k → k o< b) (sb=sa a<b) sa<b) fcb
-               zc40 : odef (UnionCF A f supf1 b) w
+               zc40 : odef (UnionCF A f ay supf1 b) w
                zc40 with zcb
                ... | ⟪ az , cp  ⟫ = ⟪ az , ? ⟫ 
 
           sup=u : {b : Ordinal} (ab : odef A b) →
-                b o≤ x → IsMinSUP A (UnionCF A f supf1 b) b ∧ (¬ HasPrev A (UnionCF A f supf1 b) f b ) → supf1 b ≡ b
+                b o≤ x → IsMinSUP A (UnionCF A f ay supf1 b) b ∧ (¬ HasPrev A (UnionCF A f ay supf1 b) f b ) → supf1 b ≡ b
           sup=u {b} ab b≤x is-sup with osuc-≡< b≤x
           ... | case1 b=x = ? where
                  zc31 : spu o≤ b
@@ -1378,8 +1381,8 @@
 
      msp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y)
          → (zc : ZChain A f mf ay x )
-         → MinSUP A (UnionCF A f (ZChain.supf zc) x)
-     msp0 f mf {x} ay zc = minsupP (UnionCF A f (ZChain.supf zc) x) (ZChain.chain⊆A zc) (ZChain.f-total zc)
+         → MinSUP A (UnionCF A f ay (ZChain.supf zc) x)
+     msp0 f mf {x} ay zc = minsupP (UnionCF A f ay (ZChain.supf zc) x) (ZChain.chain⊆A zc) (ZChain.f-total zc)
 
      fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (mf< : <-monotonic-f A f )  (zc : ZChain A f mf as0 (& A) )
             → (sp1 : MinSUP A (ZChain.chain zc))
@@ -1391,23 +1394,24 @@
            sp = MinSUP.sup sp1
            asp : odef A sp
            asp = MinSUP.as sp1
+           ay = as0
            z10 :  {a b : Ordinal } → (ca : odef chain a ) → b o< (& A) → (ab : odef A b )
-              →  HasPrev A chain f b  ∨  IsSUP A (UnionCF A f (ZChain.supf zc) b) b
+              →  HasPrev A chain f b  ∨  IsSUP A (UnionCF A f ay (ZChain.supf zc) b) b
               → * a < * b  → odef chain b
            z10 = ZChain1.is-max (SZ1 f mf mf< as0 zc (& A) o≤-refl )
            z22 : sp o< & A
            z22 = z09 asp
            z12 : odef chain sp
            z12 with o≡? (& s) sp
-           ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc )
-           ... | no ne = ZChain1.is-max (SZ1 f mf mf< as0 zc (& A) o≤-refl) {& s} {sp} ( ZChain.chain∋init zc ) (z09 asp) asp (case2 z19 ) z13 where
+           ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc ? )
+           ... | no ne = ZChain1.is-max (SZ1 f mf mf< as0 zc (& A) o≤-refl) {& s} {sp} ( ZChain.chain∋init zc ? ) (z09 asp) asp (case2 z19 ) z13 where
                z13 :  * (& s) < * sp
-               z13 with MinSUP.x≤sup sp1 ( ZChain.chain∋init zc )
+               z13 with MinSUP.x≤sup sp1 ( ZChain.chain∋init zc ? )
                ... | case1 eq = ⊥-elim ( ne eq )
                ... | case2 lt = lt
-               z19 : IsSUP A (UnionCF A f (ZChain.supf zc) sp) sp
+               z19 : IsSUP A (UnionCF A f ay (ZChain.supf zc) sp) sp
                z19 = record {   x≤sup = z20 }  where
-                   z20 : {y : Ordinal} → odef (UnionCF A f (ZChain.supf zc) sp) y → (y ≡ sp) ∨ (y << sp)
+                   z20 : {y : Ordinal} → odef (UnionCF A f ay (ZChain.supf zc) sp) y → (y ≡ sp) ∨ (y << sp)
                    z20 {y} zy with MinSUP.x≤sup sp1
                        (subst (λ k → odef chain k ) (sym &iso) (chain-mono f mf as0 supf (ZChain.supf-mono zc) (o<→≤ z22)  zy ))
                    ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso y=p )