# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1659424140 -32400
# Node ID c164f4f7cfd1e1fc34dd8c3884521b63db11cb42
# Parent  56df4675e15a218b90cf66941585e21a3d151f76
u<x in UChain again

diff -r 56df4675e15a -r c164f4f7cfd1 src/zorn.agda
--- a/src/zorn.agda	Tue Aug 02 11:34:28 2022 +0900
+++ b/src/zorn.agda	Tue Aug 02 16:09:00 2022 +0900
@@ -284,7 +284,7 @@
 data UChain  ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y )
        (supf : Ordinal → Ordinal) (x : Ordinal) : (z : Ordinal) → Set n where 
     ch-init : {z : Ordinal } (fc : FClosure A f y z) → UChain A f mf ay supf x z
-    ch-is-sup  : (u : Ordinal) {z : Ordinal }  ( is-sup : ChainP A f mf ay supf u ) 
+    ch-is-sup  : (u : Ordinal) {z : Ordinal }  (u<x : u o< x) ( is-sup : ChainP A f mf ay supf u ) 
         ( fc : FClosure A f (supf u) z ) → UChain A f mf ay supf x z
 
 ∈∧P→o< :  {A : HOD } {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A
@@ -322,22 +322,24 @@
    order {b} {s} {z1} b<z sf<sb fc = zc04 where
         zc01 : {z1 : Ordinal } → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1
         zc01  (init x refl ) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc03  where
-            s<z : s o< z
-            s<z with trio< s z
+            s<b : s o< b
+            s<b with trio< s b
             ... | tri< a ¬b ¬c = a
-            ... | tri≈ ¬a b ¬c = ⊥-elim ( o<¬≡ (cong supf b)  (ordtrans<-≤ sf<sb (supf-mono b<z)  ))
+            ... | tri≈ ¬a b ¬c = ⊥-elim ( o<¬≡ (cong supf b) sf<sb )
             ... | tri> ¬a ¬b c with osuc-≡< ( supf-mono c )
-            ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) (ordtrans<-≤ sf<sb (supf-mono b<z)  ))
-            ... | case2 lt = ⊥-elim ( o<> lt (ordtrans<-≤ sf<sb (supf-mono b<z)  ))
+            ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) sf<sb )
+            ... | case2 lt = ⊥-elim ( o<> lt  sf<sb   )
+            s<z : s o< z
+            s<z = ordtrans s<b b<z
             zc03 : odef (UnionCF A f mf ay supf b)  (supf s)
             zc03 with csupf (o<→≤ s<z) 
             ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc  ⟫ 
-            ... | ⟪ as , ch-is-sup u is-sup fc ⟫ = ⟪ as , ch-is-sup u is-sup fc ⟫ 
+            ... | ⟪ as , ch-is-sup u u<x is-sup fc ⟫ = ⟪ as , ch-is-sup u (ordtrans u<x s<b) is-sup fc ⟫ 
         zc01  (fsuc x fc) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc04  where
             zc04 : odef (UnionCF A f mf ay supf b) (f x)
             zc04 with subst (λ k → odef (UnionCF A f mf ay supf b) k ) &iso (zc01 fc  )
             ... | ⟪ as , ch-init fc ⟫ = ⟪ proj2 (mf _ as) , ch-init (fsuc _ fc) ⟫ 
-            ... | ⟪ as , ch-is-sup u is-sup fc ⟫ = ⟪ proj2 (mf _ as) , ch-is-sup u is-sup (fsuc _ fc) ⟫ 
+            ... | ⟪ as , ch-is-sup u u<x is-sup fc ⟫ = ⟪ proj2 (mf _ as) , ch-is-sup u u<x is-sup (fsuc _ fc) ⟫ 
         zc00 : ( * z1  ≡  SUP.sup (sup b<z )) ∨ ( * z1  < SUP.sup ( sup b<z ) )
         zc00 = SUP.x<sup (sup b<z) (zc01 fc )
         zc04 : (z1 ≡ supf b) ∨ (z1 << supf b)
@@ -366,7 +368,7 @@
 chain-total A f mf {y} ay supf {xa} {xb} {a} {b} ca cb = ct-ind xa xb ca cb where
      ct-ind : (xa xb : Ordinal) → {a b : Ordinal} → UChain A f mf ay supf xa a → UChain A f mf ay supf xb b → Tri (* a < * b) (* a ≡ * b) (* b < * a)
      ct-ind xa xb {a} {b} (ch-init fca) (ch-init fcb) = fcn-cmp y f mf fca fcb
-     ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub supb fcb) with ChainP.fcy<sup supb fca
+     ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub u<x supb fcb) with ChainP.fcy<sup supb fca
      ... | case1 eq with s≤fc (supf ub) f mf fcb
      ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
           ct00 : * a ≡ * b
@@ -374,14 +376,14 @@
      ... | case2 lt = tri< ct01  (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt)  where
           ct01 : * a < * b 
           ct01 = subst (λ k → * k < * b ) (sym eq) lt
-     ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub supb fcb) | case2 lt = tri< ct01  (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt)  where
+     ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub u<x supb fcb) | case2 lt = tri< ct01  (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt)  where
           ct00 : * a < * (supf ub)
           ct00 = lt
           ct01 : * a < * b 
           ct01 with s≤fc (supf ub) f mf fcb
           ... | case1 eq =  subst (λ k → * a < k ) eq ct00
           ... | case2 lt =  IsStrictPartialOrder.trans POO ct00 lt
-     ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-init fcb) with ChainP.fcy<sup supa fcb
+     ct-ind xa xb {a} {b} (ch-is-sup ua u<x supa fca) (ch-init fcb) with ChainP.fcy<sup supa fcb
      ... | case1 eq with s≤fc (supf ua) f mf fca
      ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
           ct00 : * a ≡ * b
@@ -389,14 +391,14 @@
      ... | case2 lt = tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01    where
           ct01 : * b < * a 
           ct01 = subst (λ k → * k < * a ) (sym eq) lt
-     ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-init fcb) | case2 lt = tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01    where
+     ct-ind xa xb {a} {b} (ch-is-sup ua u<x supa fca) (ch-init fcb) | case2 lt = tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01    where
           ct00 : * b < * (supf ua)
           ct00 = lt
           ct01 : * b < * a 
           ct01 with s≤fc (supf ua) f mf fca
           ... | case1 eq =  subst (λ k → * b < k ) eq ct00
           ... | case2 lt =  IsStrictPartialOrder.trans POO ct00 lt
-     ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-is-sup ub supb fcb) with trio< (supf ua) (supf ub)
+     ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x supb fcb) with trio< (supf ua) (supf ub)
      ... | tri< a₁ ¬b ¬c with ChainP.order supb  a₁ fca 
      ... | case1 eq with s≤fc (supf ub) f mf fcb 
      ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
@@ -405,16 +407,16 @@
      ... | case2 lt =  tri< ct02  (λ eq → <-irr (case1 (sym eq)) ct02) (λ lt → <-irr (case2 ct02) lt)  where
           ct02 : * a < * b 
           ct02 = subst (λ k → * k < * b ) (sym eq) lt
-     ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-is-sup ub supb fcb) | tri< a₁ ¬b ¬c | case2 lt = tri< ct02  (λ eq → <-irr (case1 (sym eq)) ct02) (λ lt → <-irr (case2 ct02) lt)  where
+     ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x supb fcb) | tri< a₁ ¬b ¬c | case2 lt = tri< ct02  (λ eq → <-irr (case1 (sym eq)) ct02) (λ lt → <-irr (case2 ct02) lt)  where
           ct03 : * a < * (supf ub)
           ct03 = lt
           ct02 : * a < * b 
           ct02 with s≤fc (supf ub) f mf fcb
           ... | case1 eq =  subst (λ k → * a < k ) eq ct03
           ... | case2 lt =  IsStrictPartialOrder.trans POO ct03 lt
-     ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-is-sup ub supb fcb) | tri≈ ¬a  eq ¬c 
+     ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x  supb fcb) | tri≈ ¬a  eq ¬c 
          = fcn-cmp (supf ua) f mf fca (subst (λ k → FClosure A f k b ) (sym eq) fcb )
-     ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-is-sup ub supb fcb) | tri> ¬a ¬b c with ChainP.order supa c fcb 
+     ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x supb fcb) | tri> ¬a ¬b c with ChainP.order supa c fcb 
      ... | case1 eq with s≤fc (supf ua) f mf fca 
      ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
           ct00 : * a ≡ * b
@@ -422,7 +424,7 @@
      ... | case2 lt =  tri> (λ lt → <-irr (case2 ct02) lt) (λ eq → <-irr (case1 eq) ct02) ct02    where
           ct02 : * b < * a 
           ct02 = subst (λ k → * k < * a ) (sym eq) lt
-     ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-is-sup ub supb fcb) | tri> ¬a ¬b c | case2 lt = tri> (λ lt → <-irr (case2 ct04) lt) (λ eq → <-irr (case1 (eq)) ct04) ct04    where
+     ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x supb fcb) | tri> ¬a ¬b c | case2 lt = tri> (λ lt → <-irr (case2 ct04) lt) (λ eq → <-irr (case1 (eq)) ct04) ct04    where
           ct05 : * b < * (supf ua)
           ct05 = lt
           ct04 : * b < * a 
@@ -441,8 +443,8 @@
 Zorn-lemma {A}  0<A supP = zorn00 where
      <-irr0 : {a b : HOD} → A ∋ a → A ∋ b  → (a ≡ b ) ∨ (a < b ) → b < a → ⊥
      <-irr0 {a} {b} A∋a A∋b = <-irr
-     z07 :   {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A
-     z07 {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p )))
+     z07 :   {y : Ordinal} {A : HOD } → {P : Set n} → odef A y ∧ P → y o< & A
+     z07 {y} {A} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p )))
      z09 : {b : Ordinal } { A : HOD } → odef A b → b o< & A
      z09 {b} {A} ab = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
      s : HOD
@@ -499,25 +501,29 @@
      SZ1 :( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
         {init : Ordinal} (ay : odef A init) (zc : ZChain A f mf ay (& A)) (x : Ordinal)   → ZChain1 A f mf ay zc x
      SZ1 A f mf {y} ay zc x = TransFinite { λ x →  ZChain1 A f mf ay zc x } zc1 x where
-        chain-mono1 : (x : Ordinal) {a b c : Ordinal} → 
-            odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c
-        chain-mono1 x {a} {b} {c} ⟪ ua , ch-init fc  ⟫ = 
+        chain-mono1 : (x : Ordinal) {a b c : Ordinal} → a o≤ b
+            → odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c
+        chain-mono1 x {a} {b} {c} a≤b ⟪ ua , ch-init fc  ⟫ = 
             ⟪ ua , ch-init fc  ⟫ 
-        chain-mono1 x {a} {b} {c} ⟪ uaa ,  ch-is-sup ua is-sup fc  ⟫ = 
-            ⟪ uaa , ch-is-sup ua  is-sup fc  ⟫ 
+        chain-mono1 x {a} {b} {c} a≤b ⟪ uaa ,  ch-is-sup ua ua<x is-sup fc  ⟫ = 
+            ⟪ uaa , ch-is-sup ua (ordtrans<-≤ ua<x a≤b ) is-sup fc  ⟫ 
         chain<ZA : {x : Ordinal } → UnionCF A f mf ay (ZChain.supf zc) x ⊆' UnionCF A f mf ay (ZChain.supf zc) (& A)
         chain<ZA {x} ux with proj2 ux
         ... | ch-init fc = ⟪ proj1 ux , ch-init fc ⟫
-        ... | ch-is-sup u is-sup fc = ⟪ proj1 ux , ch-is-sup u  is-sup fc ⟫ 
+        ... | ch-is-sup u pu<x is-sup fc = ⟪ proj1 ux , ch-is-sup u u<x is-sup fc ⟫  where
+            u<A : (& ( * ( ZChain.supf zc u)))  o< & A
+            u<A = c<→o< (subst (λ k → odef A k ) (sym &iso) (A∋fcs _ f mf fc) )
+            u<x :  u o< & A
+            u<x = subst (λ k → k o< & A ) (trans &iso ?) u<A
         is-max-hp : (x : Ordinal) {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
             b o< x → (ab : odef A b) →
             HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) ab f → 
             * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b
         is-max-hp x {a} {b} ua b<x ab has-prev a<b with HasPrev.ay has-prev
         ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫ 
-        ... | ⟪ ab0 , ch-is-sup u is-sup fc ⟫ = ⟪ ab , 
+        ... | ⟪ ab0 , ch-is-sup u u<x is-sup fc ⟫ = ⟪ ab , 
                  subst (λ k → UChain A f mf ay (ZChain.supf zc) x k )
-                      (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u is-sup (fsuc _ fc))  ⟫ 
+                      (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u<x is-sup (fsuc _ fc))  ⟫ 
         zc1 :  (x : Ordinal) →  ((y₁ : Ordinal) → y₁ o< x → ZChain1 A f mf ay zc y₁) → ZChain1 A f mf ay zc x
         zc1 x prev with Oprev-p x
         ... | yes op = record { is-max = is-max } where
@@ -537,20 +543,23 @@
                  m01 : odef (UnionCF A f mf ay (ZChain.supf zc) x) b
                  m01 with trio< b px    --- px  < b < x
                  ... | tri> ¬a ¬b c = ⊥-elim (¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x  ⟫)
-                 ... | tri< b<px ¬b ¬c = chain-mono1 x m04 where
+                 ... | tri< b<px ¬b ¬c = chain-mono1 x (ordtrans px<x ? ) m04 where
                     m03 :  odef (UnionCF A f mf ay (ZChain.supf zc) px) a -- if a ∈ chain of px, is-max of px can be used
                     m03 with proj2 ua
                     ... | ch-init fc = ⟪ proj1 ua ,  ch-init fc ⟫
-                    ... | ch-is-sup u is-sup-a fc = ⟪ proj1 ua , ch-is-sup u  is-sup-a fc ⟫
+                    ... | ch-is-sup u u<x is-sup fc with trio< u px
+                    ... | tri< a ¬b ¬c = ⟪ proj1 ua , ch-is-sup u a is-sup fc ⟫
+                    ... | tri≈ ¬a u=px ¬c = ?   ---    supf u < a < b , 
+                    ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x ⟫ )
                     m04 : odef (UnionCF A f mf ay (ZChain.supf zc) px) b
                     m04 = ZChain1.is-max (prev px px<x) m03 b<px ab 
-                         (case2 record {x<sup = λ {z} lt → IsSup.x<sup is-sup (chain-mono1 x lt)  } ) a<b
-                 ... | tri≈ ¬a b=px ¬c = ⟪ ab , ch-is-sup b  m06 (subst (λ k → FClosure A f k b) m05 (init ab refl)) ⟫   where
+                         (case2 record {x<sup = λ {z} lt → IsSup.x<sup is-sup (chain-mono1 x ? lt)  } ) a<b
+                 ... | tri≈ ¬a b=px ¬c = ⟪ ab , ch-is-sup b b<x m06 (subst (λ k → FClosure A f k b) m05 (init ab refl)) ⟫   where
                     b<A : b o< & A
                     b<A = z09 ab
                     m05 : b ≡ ZChain.supf zc b
                     m05 = sym ( ZChain.sup=u zc ab (z09 ab) 
-                      record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono1 x uz )  }  )
+                      record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono1 x ? uz )  }  )
                     m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b
                     m08 {z} fcz = ZChain.fcy<sup zc b<A fcz
                     m09 : {sup1 z1 : Ordinal} → (ZChain.supf zc sup1) o< (ZChain.supf zc b) 
@@ -565,9 +574,9 @@
               * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b
            is-max {a} {b} ua b<x ab (case1 has-prev) a<b = is-max-hp x {a} {b} ua b<x ab has-prev a<b 
            is-max {a} {b} ua b<x ab (case2 is-sup) a<b with IsSup.x<sup is-sup (init-uchain A f mf ay )
-           ... | case1 b=y = ⊥-elim ( <-irr ( ZChain.initial zc (chain<ZA {x} (chain-mono1 (osuc x) ua )) )
+           ... | case1 b=y = ⊥-elim ( <-irr ( ZChain.initial zc (chain<ZA {x} (chain-mono1 (osuc x) ? ua )) )
                        (subst (λ k → * a < * k ) (sym b=y) a<b ) )
-           ... | case2 y<b = chain-mono1 x m04 where
+           ... | case2 y<b = chain-mono1 x ? m04 where
                  m09 : b o< & A
                  m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
                  m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b
@@ -577,11 +586,11 @@
                  m08 {sup1} {z1} s<b fc = ZChain.order zc m09 s<b fc
                  m05 : b ≡ ZChain.supf zc b
                  m05 = sym (ZChain.sup=u zc ab m09
-                      record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono1 x lt )} )   -- ZChain on x
+                      record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono1 x ? lt )} )   -- ZChain on x
                  m06 : ChainP A f mf ay (ZChain.supf zc) b 
                  m06 = record { fcy<sup = m07 ;  order = m08 }
                  m04 : odef (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) b
-                 m04 = ⟪ ab , ch-is-sup b  m06 (subst (λ k → FClosure A f k b) m05 (init ab refl))  ⟫
+                 m04 = ⟪ ab , ch-is-sup b ?  m06 (subst (λ k → FClosure A f k b) m05 (init ab refl))  ⟫
 
      ---
      --- the maximum chain  has fix point of any ≤-monotonic function
@@ -677,11 +686,11 @@
           isy : {z : Ordinal } → odef (UnionCF A f mf ay isupf o∅) z → * y ≤ * z
           isy {z} ⟪ az , uz ⟫ with uz 
           ... | ch-init fc = s≤fc y f mf fc 
-          ... | ch-is-sup u is-sup fc = ≤-ftrans (subst (λ k → * y ≤ k) (sym *iso) y<sup)  (s≤fc (& (SUP.sup (ysup f mf ay))) f mf fc )
+          ... | ch-is-sup u u<x is-sup fc = ≤-ftrans (subst (λ k → * y ≤ k) (sym *iso) y<sup)  (s≤fc (& (SUP.sup (ysup f mf ay))) f mf fc )
           inext : {a : Ordinal} → odef (UnionCF A f mf ay isupf o∅) a → odef (UnionCF A f mf ay isupf o∅) (f a)
           inext {a} ua with (proj2 ua)
           ... | ch-init fc = ⟪ proj2 (mf _ (proj1 ua))  , ch-init (fsuc _ fc )  ⟫
-          ... | ch-is-sup u is-sup fc = ⟪ proj2 (mf _ (proj1 ua)) ,  ch-is-sup u is-sup (fsuc _ fc) ⟫
+          ... | ch-is-sup u u<x is-sup fc = ⟪ proj2 (mf _ (proj1 ua)) ,  ch-is-sup u u<x is-sup (fsuc _ fc) ⟫
           itotal : IsTotalOrderSet (UnionCF A f mf ay isupf o∅) 
           itotal {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) )
@@ -689,7 +698,7 @@
           mono : {x : Ordinal} {z : Ordinal} → x o< z → isupf x o≤ isupf z 
           mono {x} {z} x<z = o≤-refl
           csupf : {z : Ordinal} → z o≤ o∅ → odef (UnionCF A f mf ay isupf z ) (isupf z)
-          csupf {z} z≤0 = ⟪ asi , ch-is-sup spi uz02 (init asi refl) ⟫ where
+          csupf {z} z≤0 = ⟪ asi , ch-is-sup spi ? uz02 (init asi refl) ⟫ where
                uz03 : {z : Ordinal } →  FClosure A f y z → (z ≡ isupf spi) ∨ (z << isupf spi)
                uz03 {z} fc with SUP.x<sup sp (subst (λ k → FClosure A f y k ) (sym &iso) fc )
                ... | case1 eq = case1 ( begin
@@ -732,11 +741,11 @@
           pchain⊆A {y} ny = proj1 ny
           pnext : {a : Ordinal} → odef pchain a → odef pchain (f a)
           pnext {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 (mf a aa) , ch-init (fsuc _ fc)  ⟫
-          pnext {a} ⟪ aa , ch-is-sup u is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u is-sup (fsuc _ fc ) ⟫
+          pnext {a} ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u ? is-sup (fsuc _ fc ) ⟫
           pinit :  {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁
           pinit {a} ⟪ aa , ua ⟫  with  ua
           ... | ch-init fc = s≤fc y f mf fc
-          ... | ch-is-sup u is-sup fc = ≤-ftrans (<=to≤ zc7) (s≤fc _ f mf fc)  where
+          ... | ch-is-sup u u<x is-sup fc = ≤-ftrans (<=to≤ zc7) (s≤fc _ f mf fc)  where
                zc7 : y <= (ZChain.supf zc) u 
                zc7 = ChainP.fcy<sup is-sup (init ay refl)
           pcy : odef pchain y
@@ -754,13 +763,14 @@
                  sup {z} z<x with trio< z px
                  ... | tri< a ¬b ¬c = ZChain.sup zc a
                  ... | tri> ¬a ¬b c = ⊥-elim (¬p<x<op ⟪ c , subst (λ k → z o< k) (sym (Oprev.oprev=x op)) z<x ⟫ )  --   px < z < x
-                 ... | tri≈ ¬a b ¬c = record { sup = * (supf0 px) ; A∋maximal = subst (λ k → odef A k) (sym &iso) (proj1 (ZChain.csupf zc o≤-refl ))
-                     ; x<sup = x<sup } where
+                 ... | tri≈ ¬a b ¬c = record { sup = * (supf0 px) ; A∋maximal = subst (λ k → odef A k ) (sym &iso) (proj1 zc8) ; x<sup = x<sup } where
+                     zc9 : SUP A (UnionCF A f mf ay supf0 x)
+                     zc9 = supP pchain  pchain⊆A ptotal
                      zc8 : odef (UnionCF A f mf ay supf0 z) (supf0 px)
                      zc8 = subst (λ k → odef (UnionCF A f mf ay supf0 z) k ) (cong supf0 b)  (ZChain.csupf zc (subst (λ k → z o≤ k) b o≤-refl ))
-                     x<sup :  {w : HOD} → UnionCF A f mf ay supf0 z ∋ w → (w ≡ * (supf0 px)) ∨ (w < * (supf0 px))
+                     x<sup :  {w : HOD} → UnionCF A f mf ay supf0 z ∋ w → (w ≡ * (supf0 px) ) ∨ (w < * (supf0 px) )
                      x<sup {w} ⟪ aw , ch-init fc ⟫ = ?
-                     x<sup {w} ⟪ aw , ch-is-sup u is-sup fc ⟫ = ?
+                     x<sup {w} ⟪ aw , ch-is-sup u u<x is-sup fc ⟫ = ?
 
           zc4 : ZChain A f mf ay x 
           zc4 with ODC.∋-p O A (* px)
@@ -831,7 +841,7 @@
                 zc12 : odef A (ZChain.supf ozc z) ∧ UChain A f mf ay (ZChain.supf ozc) (osuc z) (ZChain.supf ozc z)
                 zc12  = ?
                 zc11 : odef A (ZChain.supf ozc z) ∧ UChain A f mf ay psupf x (ZChain.supf ozc z)
-                zc11 = ⟪ az , ch-is-sup z cp1 (subst (λ k → FClosure A f k _) (sym eq1) (init az refl) ) ⟫ where
+                zc11 = ⟪ az , ch-is-sup z z<x cp1 (subst (λ k → FClosure A f k _) (sym eq1) (init az refl) ) ⟫ where
                       az : odef A ( ZChain.supf ozc z )
                       az = proj1 zc12
                       zc20 : {z1  : Ordinal} → FClosure A f y z1 → (z1 ≡ psupf z) ∨ (z1 << psupf z)
@@ -841,7 +851,7 @@
                       cp1 : ChainP A f mf ay psupf z 
                       cp1 = record {  fcy<sup = zc20   ; order = ? } 
                      ---  u = supf u = supf z 
-          ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ sa , ch-is-sup {!!} {!!} {!!} ⟫ where
+          ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ sa , ch-is-sup ? {!!} {!!} {!!} ⟫ where
                 sa = SUP.A∋maximal usup
           ... | tri> ¬a ¬b c | record { eq = eq1 } = {!!}
 
@@ -859,11 +869,11 @@
           pchain⊆A {y} ny = proj1 ny
           pnext : {a : Ordinal} → odef pchain a → odef pchain (f a)
           pnext {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf a aa ) , ch-init (fsuc _ fc) ⟫
-          pnext {a} ⟪ aa , ch-is-sup u is-sup fc ⟫ = ⟪  proj2 ( mf a aa ) , ch-is-sup u is-sup (fsuc _ fc) ⟫
+          pnext {a} ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ = ⟪  proj2 ( mf a aa ) , ch-is-sup u ? is-sup (fsuc _ fc) ⟫
           pinit :  {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁
           pinit {a} ⟪ aa , ua ⟫  with  ua
           ... | ch-init fc = s≤fc y f mf fc
-          ... | ch-is-sup u is-sup fc = ≤-ftrans (<=to≤ zc7) (s≤fc _ f mf fc)  where
+          ... | ch-is-sup u u<x is-sup fc = ≤-ftrans (<=to≤ zc7) (s≤fc _ f mf fc)  where
                zc7 : y <= psupf _
                zc7 = ChainP.fcy<sup is-sup (init ay refl)
           pcy : odef pchain y
@@ -879,9 +889,9 @@
                 * a < * b → odef (UnionCF A f mf ay supf x) b
           is-max-hp supf x {a} {b} ua b<x ab has-prev a<b with HasPrev.ay has-prev
           ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫ 
-          ... | ⟪ ab0 , ch-is-sup u is-sup fc ⟫ = ⟪ ab , 
+          ... | ⟪ ab0 , ch-is-sup u u<x is-sup fc ⟫ = ⟪ ab , 
                      subst (λ k → UChain A f mf ay supf x k )
-                          (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u is-sup (fsuc _ fc))  ⟫ 
+                          (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u ? is-sup (fsuc _ fc))  ⟫ 
 
           no-extension : ZChain A f mf ay x
           no-extension  = record { initial = pinit ; chain∋init = pcy  ; supf = psupf  ; sup=u = {!!}