--- a/src/zorn.agda	Wed Aug 31 22:08:33 2022 +0900
+++ b/src/zorn.agda	Sat Sep 03 09:43:19 2022 +0900
@@ -311,13 +311,6 @@
    supf∈A : {b : Ordinal} → b o≤ z → odef A (supf b)
    supf∈A {b} b≤z = subst (λ k → odef A k ) (sym (supf-is-sup b≤z)) ( SUP.as ( sup b≤z ) )
 
-   csupf0 :  {b : Ordinal} → b o≤ z → odef (UnionCF A f mf ay supf (supf b)) (supf b)
-   csupf0 {b} b≤z = ⟪ supf∈A b≤z  , ch-is-sup (supf b) o≤-refl  ? (init zc10 zc11 ) ⟫ where
-       zc11 : supf (supf b) ≡ supf b
-       zc11 = ?
-       zc10 : odef A (supf (supf b))
-       zc10 = subst (λ k → odef A k ) (sym zc11) (  supf∈A b≤z )
-
    fcy<sup  : {u w : Ordinal } → u o< z  → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf 
    fcy<sup  {u} {w} u<z fc with SUP.x<sup (sup (o<→≤ 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 ) ⟫ 
@@ -781,6 +774,9 @@
           ... | tri≈ ¬a b ¬c = refl
           ... | tri> ¬a ¬b c = ⊥-elim ( o≤> z≤px c )
 
+          supf∈A : {b : Ordinal} → b o≤ x → odef A (supf1 b)
+          supf∈A {b} b≤z = ?
+
           supf1≤sp1 : {a : Ordinal } → supf1 a o≤ sp1
           supf1≤sp1 = ?
 
@@ -967,7 +963,37 @@
                      ... | refl = record { ax = ab ; is-sup = record { x<sup = λ {w} lt → 
                         IsSup.x<sup is-sup (subst (λ k → odef k w) pchain0=1 lt)  } }
                  csupf :  {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 (supf1 b)) (supf1 b)
-                 csupf {b} b≤x = ?
+                 csupf {b} b≤x with osuc-≡< b≤x
+                 ... | case2 b<x = csupf1 where
+                     b≤px : b o≤ px
+                     b≤px = zc-b<x _ b<x
+                     csupf0 : odef (UnionCF A f mf ay supf0 (supf1 b)) (supf1 b)
+                     csupf0 = subst (λ k → odef (UnionCF A f mf ay supf0 k) k ) (supf0=1 b≤px) ( ZChain.csupf zc b≤px )
+                     csupf1 : odef (UnionCF A f mf ay supf1 (supf1 b)) (supf1 b)
+                     csupf1 with csupf0
+                     ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ 
+                     ... | ⟪ as , ch-is-sup u u≤x record { fcy<sup = fcy<sup ; order = order ; supu=u = supu=u } fc  ⟫ 
+                        =  ⟪ as  , ch-is-sup u u≤x record { fcy<sup = fcy<sup1 ; order = order1 ; supu=u = ? }  ? ⟫  where
+                         u≤x1 : u o≤ supf1 b 
+                         u≤x1 = u≤x
+                         supu=u1 : supf1 u ≡ u
+                         supu=u1 = ?
+                         fcy<sup1 : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u) ∨ (z << supf1 u)
+                         fcy<sup1 = ? 
+                         order1 : {s z1 : Ordinal} → supf1 s o< supf1 u → FClosure A f (supf1 s) z1 
+                             → (z1 ≡ supf1 u) ∨ (z1 << supf1 u)
+                         order1 = ?
+                 ... | case1 refl = ⟪ supf∈A o≤-refl  , ch-is-sup (supf1 x) o≤-refl 
+                          record { fcy<sup = fcy<sup ; order = order ; supu=u = zc11 }  (init zc10 zc11 ) ⟫ where
+                     zc11 : supf1 (supf1 x) ≡ supf1 x
+                     zc11 = ?
+                     zc10 : odef A (supf1 (supf1 x))
+                     zc10 = subst (λ k → odef A k ) (sym zc11) (  supf∈A o≤-refl )
+                     fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 (supf1 x)) ∨ (z << supf1 (supf1 x))
+                     fcy<sup = ? 
+                     order : {s z1 : Ordinal} → supf1 s o< supf1 (supf1 b) → FClosure A f (supf1 s) z1 
+                         → (z1 ≡ supf1 (supf1 b)) ∨ (z1 << supf1 (supf1 b))
+                     order = ?
                  sis : {z : Ordinal} (z≤x : z o≤ x) → supf1 z ≡ & (SUP.sup (sup z≤x))
                  sis {z} z≤x  = zc40 where
                       zc40 : supf1 z ≡ & (SUP.sup (sup z≤x))  -- direct with statment causes error