--- a/src/zorn.agda	Fri Jul 22 16:08:31 2022 +0900
+++ b/src/zorn.agda	Fri Jul 22 16:52:17 2022 +0900
@@ -472,13 +472,13 @@
                     ... | ch-init fc = ⟪ proj1 ua ,  ch-init 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 b ¬c = ?
+                    ... | 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 ⟫ )
                     -- = ⟪ proj1 ua , ? ⟫
                     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-mono2 x ( o<→≤  (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ))  o≤-refl lt)  } ) a<b
-                 ... | tri≈ ¬a b=px ¬c = ? -- b = px case
+                 ... | tri≈ ¬a b=px ¬c = ? -- b = px case,  u = px  u<x 
         ... | no lim = record { is-max = is-max ; chain-mono2 = chain-mono2 x ; fcy<sup = fcy<sup ; sup=u = sup=u ; order = order  }  where
            fcy<sup : {u w : Ordinal} → u o< x → FClosure A f y w → w << ZChain.supf zc u
            fcy<sup {u} {w} u<x fc = ZChain1.fcy<sup (prev (osuc u) (ob<x lim u<x)) <-osuc fc
@@ -511,7 +511,7 @@
                  m06 = record { fcy<sup = m07 ; csupz = subst (λ k →  FClosure A f k b ) m05 (init ab) ; order = m08 ; y<s = y<s 
                        ; supfu=u = sym m05 }
                  m04 : odef (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) b
-                 m04 = ⟪ ab , ch-is-sup ? ? m06 (subst (λ k → FClosure A f k b) m05 (init ab))  ⟫
+                 m04 = ⟪ ab , ch-is-sup b <-osuc m06 (subst (λ k → FClosure A f k b) m05 (init ab))  ⟫
 
      ---
      --- the maximum chain  has fix point of any ≤-monotonic function
@@ -582,7 +582,7 @@
           isupf : Ordinal → Ordinal
           isupf z = y
           cy : odef (UnionCF A f mf ay isupf o∅) y
-          cy = ⟪ ay , ch-init ?  ⟫
+          cy = ⟪ ay , ch-init (init ay)  ⟫
           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 
@@ -675,8 +675,13 @@
           ... | case1 pr = no-extension -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) apx )
           ... | case1 is-sup = -- x is a sup of zc 
-                record {  supf = {!!} ; chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal
-                     ; initial = pinit ; chain∋init  = pcy ; sup=u = ? ; order = ? } 
+                record {  supf = psupf1 ; chain⊆A = ? ; f-next = ? ; f-total = ?
+                     ; initial = ? ; chain∋init  = ? ; sup=u = ? ; order = ? }  where
+             psupf1 : Ordinal → Ordinal
+             psupf1 z with trio< z x 
+             ... | tri< a ¬b ¬c = ZChain.supf zc z
+             ... | tri≈ ¬a b ¬c = x
+             ... | tri> ¬a ¬b c = x
           ... | case2 ¬x=sup =  no-extension -- px is not f y' nor sup of former ZChain from y -- no extention
      ... | no lim = zc5 where
 
@@ -707,13 +712,8 @@
           pchain⊆A : {y : Ordinal} → odef pchain y →  odef A y
           pchain⊆A {y} ny = proj1 ny
           pnext : {a : Ordinal} → odef pchain a → odef pchain (f a)
-          pnext {a} ⟪ aa , ua ⟫ = ⟪ afa , fua  ⟫ where
-               afa : odef A ( f a )
-               afa = proj2 ( mf a aa )
-               fua : UChain A f mf ay psupf0 ? (f a)
-               fua = ? -- with  ua
-               -- ... | ch-init fc = ch-init  ( fsuc _ fc )
-               --- ... | ch-is-sup u is-sup fc = ch-is-sup u (ChainP-next A f mf ay _ is-sup ) (fsuc _ fc )
+          pnext {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf a aa ) , ch-init (fsuc _ fc) ⟫
+          pnext {a} ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ = ⟪  proj2 ( mf a aa ) , ch-is-sup u u<x (ChainP-next A f mf ay _ 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