--- a/src/zorn.agda	Fri Jul 22 19:18:05 2022 +0900
+++ b/src/zorn.agda	Sat Jul 23 17:19:18 2022 +0900
@@ -293,6 +293,7 @@
       initial : {y : Ordinal } → odef chain y → * init ≤ * y
       f-next : {a : Ordinal } → odef chain a → odef chain (f a)
       f-total : IsTotalOrderSet chain
+      chain∋supf : {z : Ordinal } → odef chain (supf z)
       sup=u : {b : Ordinal} → {ab : odef A b} → b o< z → IsSup A chain ab → supf b ≡ b 
       order : {b sup1 z1 : Ordinal} → b o< z → sup1 o< b → FClosure A f (supf sup1) z1 → z1 << supf b
 
@@ -449,7 +450,7 @@
                       (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u<x (ChainP-next A f mf ay _ 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 ; chain-mono2 = chain-mono2 x ; fcy<sup = fcy<sup ; sup=u = ? ; order = order } where
+        ... | yes op = record { is-max = is-max ; chain-mono2 = chain-mono2 x ; fcy<sup = fcy<sup ; sup=u = sup=u ; order = order } where
            px = Oprev.oprev op
            px<x : px o< x
            px<x = subst (λ k → px o< k ) (Oprev.oprev=x op) <-osuc
@@ -470,7 +471,7 @@
                 IsSup A (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) ab → ZChain.supf zc b ≡ b
            sup=u {b} {ab} b<x is-sup with trio< b px
            ... | tri< b<px ¬b ¬c = ZChain1.sup=u (prev px px<x) b<px is-sup
-           ... | tri≈ ¬a b=px ¬c = ZChain.sup=u zc ? is-sup
+           ... | tri≈ ¬a b=px ¬c = ZChain.sup=u zc ? ?
            ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ )
            is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
               b o< x → (ab : odef A b) →
@@ -658,29 +659,59 @@
           pcy : odef pchain y
           pcy = ⟪ ay , ch-init (init ay)    ⟫
 
-          supf0 = ZChain.supf (prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ))
+          supf0 : Ordinal → Ordinal
+          supf0 z with trio< z x
+          ... | tri< a ¬b ¬c = ZChain.supf zc z
+          ... | tri≈ ¬a b ¬c = ZChain.supf zc px
+          ... | tri> ¬a ¬b c = ZChain.supf zc px
+
+          spuf0eq : {z : Ordinal} → z o< x → supf0 z ≡ ZChain.supf zc z 
+          spuf0eq {z} z<x with trio< z x
+          ... | tri< a ¬b ¬c = refl
+          ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a z<x )
+          ... | tri> ¬a ¬b c = ⊥-elim ( ¬a z<x )
+
+          zc9 :  UnionCF A f mf ay (ZChain.supf zc) px ⊆'  UnionCF A f mf ay supf0 x 
+          zc9 ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
+          zc9 {z} ⟪ az , ch-is-sup u u<px is-sup fc ⟫ with trio< z x
+          ... | tri< a ¬b ¬c = ⟪ az , ch-is-sup u (ordtrans u<px px<x) ? ? ⟫ 
+          ... | tri≈ ¬a b ¬c = ?
+          ... | tri> ¬a ¬b c = ?
+
+          -- ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
+          --- zc9 {z} ⟪ az , ch-is-sup u u<px is-sup fc ⟫ with trio< z x
+          -- ... | tri< a ¬b ¬c = ⟪ az , ch-is-sup u (ordtrans u<px px<x) ? ? ⟫ 
+          -- ... | tri≈ ¬a b ¬c = ?
+          -- ... | tri> ¬a ¬b c = ?
+          -- = ⟪ az , ch-is-sup u (ordtrans u<px px<x) ? ? ⟫ 
 
           -- if previous chain satisfies maximality, we caan reuse it
           --
           no-extension : ZChain A f mf ay x
           no-extension = record { supf = supf0
-               ; initial = pinit ; chain∋init = pcy  ; sup=u = sup=u 
-              ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal ;  order = order } where
+               ; initial = ? ; chain∋init = ?  ; sup=u = sup=u  ; chain∋supf = ?
+              ;  chain⊆A = ?  ;  f-next = ? ;  f-total = ? ;  order = ? } where
+              cs : {z : Ordinal} → odef (UnionCF A f mf ay supf0 x) (supf0 z)
+              cs {z} with trio< z x
+              ... | tri< a ¬b ¬c = zc9 (ZChain.chain∋supf zc {z} )
+              ... | tri≈ ¬a b ¬c = ?
+              ... | tri> ¬a ¬b c = ?
+              --- = subst (λ k → odef (UnionCF A f mf ay supf0 k) (supf0 z)) ? (ZChain.chain∋supf zc {z} ) 
               sup=u :  {b : Ordinal} {ab : odef A b} → b o< x 
                     → IsSup A (UnionCF A f mf ay supf0 x) ab 
                     → supf0 b ≡ b
               sup=u {b} {ab} b<x is-sup with trio< b px
-              ... | tri< a ¬b ¬c = ZChain.sup=u zc {b} {ab} a record { x<sup = pc20 } where
+              ... | tri< a ¬b ¬c = ? where --  ZChain.sup=u zc {b} {ab} a record { x<sup = pc20 } where
                      pc20 : {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op)) z → (z ≡ b) ∨ (z << b)
                      pc20 {z} ⟪ az , ch-init fc  ⟫ = 
                          IsSup.x<sup is-sup ⟪ az ,  ch-init fc  ⟫ 
                      pc20 {z} ⟪ az , ch-is-sup u u<x is-sup-c fc  ⟫ = IsSup.x<sup is-sup 
-                         ⟪ az , ch-is-sup u (subst (λ k → u o< k) (Oprev.oprev=x op) (ordtrans u<x <-osuc)) is-sup-c fc  ⟫ 
+                         ⟪ az , ch-is-sup u (subst (λ k → u o< k) (Oprev.oprev=x op) (ordtrans u<x <-osuc)) ? ?  ⟫ 
               ... | tri≈ ¬a refl ¬c = ?
               ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op))  b<x  ⟫ )
               order : {b sup1 z1 : Ordinal} → b o< x → sup1 o< b → FClosure A f (supf0 sup1) z1 → z1 << supf0 b
               order {b} {s} {z1} b<x s<b fc with trio< b px 
-              ... | tri< a ¬b ¬c = ZChain.order zc a s<b fc
+              ... | tri< a ¬b ¬c = ? -- ZChain.order zc a s<b ?
               ... | tri≈ ¬a refl ¬c = ?
               ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op))  b<x  ⟫ )
 
@@ -692,13 +723,19 @@
           ... | 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 = psupf1 ; chain⊆A = ? ; f-next = ? ; f-total = ?
+                record {  supf = psupf1 ; chain⊆A = ? ; f-next = ? ; f-total = ? ; chain∋supf = ?
                      ; 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
+             cA : UnionCF A f mf ay psupf1 x ⊆' A
+             cA {z} uz with trio< z x
+             ... | tri< a ¬b ¬c = ZChain.chain⊆A zc ⟪ proj1 uz , ? ⟫ 
+             ... | tri≈ ¬a b ¬c = ?
+             ... | tri> ¬a ¬b c = ?
+
           ... | case2 ¬x=sup =  no-extension -- px is not f y' nor sup of former ZChain from y -- no extention
      ... | no lim = zc5 where
 
@@ -741,7 +778,7 @@
           pcy = ⟪ ay , ch-init (init ay)    ⟫
 
           no-extension : ZChain A f mf ay x
-          no-extension  = record { initial = pinit ; chain∋init = pcy  ; supf = psupf0 
+          no-extension  = record { initial = pinit ; chain∋init = pcy  ; supf = psupf0  ; chain∋supf = ?
               ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal ; sup=u = ? ; order = ? }
 
           usup : SUP A pchain
@@ -760,7 +797,7 @@
                -- we have to check adding x preserve is-max ZChain A y f mf x
           ... | case1 pr = no-extension  
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax )
-          ... | case1 is-sup = record { initial = {!!} ; chain∋init = {!!}  ; supf = psupf1  ; sup=u = ? ; order = ?
+          ... | case1 is-sup = record { initial = {!!} ; chain∋init = {!!}  ; supf = psupf1  ; sup=u = ? ; order = ? ; chain∋supf = ?
               ;  chain⊆A = {!!} ;  f-next = {!!} ;  f-total = ? } where -- x is a sup of (zc ?) 
              psupf1 : Ordinal → Ordinal
              psupf1 z with trio< z x