--- a/src/zorn.agda	Fri Aug 05 11:09:04 2022 +0900
+++ b/src/zorn.agda	Fri Aug 05 16:21:46 2022 +0900
@@ -310,15 +310,27 @@
       f-total : IsTotalOrderSet chain
 
       sup : {x : Ordinal } → x o≤ z  → SUP A (UnionCF A f mf ay supf x)
-      supf-is-sup : {x : Ordinal } → (x<z : x o≤ z) → supf x ≡ & (SUP.sup (sup x<z) )
       sup=u : {b : Ordinal} → (ab : odef A b) → b o< z  → IsSup A (UnionCF A f mf ay supf (osuc b)) ab → supf b ≡ b 
-      csupf : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf b) (supf b) 
-      supf-mono : {x y : Ordinal } → x o< y → supf x o≤ supf y
+      supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (sup x≤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 ) ⟫ 
    ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso  (trans (cong (&) eq) (sym (supf-is-sup (o<→≤ u<z) ) ) ))
    ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup (o<→≤ u<z) ))) ) lt )
+
+   csupf : {b : Ordinal } → b o< z → odef (UnionCF A f mf ay supf b) (supf b) 
+   csupf {b} b<z = ⟪ asb , ch-is-sup b o≤-refl is-sup (init asb refl)  ⟫ where
+       asb : odef A (supf b)
+       asb = subst (λ k → odef A k ) (sym (supf-is-sup ? )) (SUP.A∋maximal (sup ? ))
+       is-sup : ChainP A f mf ay supf b
+       is-sup = record { fcy<sup = fcy<sup b<z ; order = ? ; supu=u = ? }
+   supf-mono : {x y : Ordinal } → x o< y → supf x o≤ supf y
+   supf-mono = ?
+   -- supf-is-sup {x} x≤z  = ? where
+   --   zc51 : * (supf x) ≡ SUP.sup (sup x≤z )  
+   --   zc51 = ==→o≡ record { eq→  ? ; eq← = ? }
+   --   zc50 : supf x ≡ & (SUP.sup (sup x<z) )
+   --   zc50 = ?
    order : {b s z1 : Ordinal} → b o< z → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
    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
@@ -333,7 +345,7 @@
             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) 
+            zc03 with csupf s<z 
             ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc  ⟫ 
             ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ as , ch-is-sup u (ordtrans u≤x (osucc s<b)) is-sup fc ⟫ 
         zc01  (fsuc x fc) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc04  where
@@ -882,10 +894,12 @@
 
           no-extension : ¬ spu ≡ x → ZChain A f mf ay x
           no-extension ¬sp=x  = record { initial = pinit ; chain∋init = pcy  ; supf = supf1  ; sup=u = {!!} 
-               ; supf-is-sup = ?
+               ; sup = ? ; supf-is-sup = ?
                ; csupf = ? ; chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal ; supf-mono = ? } where
-                 UnionCF⊆ : UnionCF A f mf ay supf1 x ⊆' UnionCF A f mf ay ? x 
-
+                 supfu : {u : Ordinal } → ( a : u o< x ) → (z : Ordinal) → Ordinal
+                 supfu {u} a z = ZChain.supf (pzc (osuc u) (ob<x lim a)) z
+                 UnionCF⊆ : {u : Ordinal} → (a : u o< x ) → UnionCF A f mf ay supf1 x ⊆' UnionCF A f mf ay (supfu a) x 
+                 UnionCF⊆ = ?
           zc5 : ZChain A f mf ay x 
           zc5 with ODC.∋-p O A (* x)
           ... | no noax = no-extension ? -- ¬ A ∋ p, just skip
@@ -894,7 +908,7 @@
           ... | case1 pr = no-extension ? 
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax )
           ... | case1 is-sup = record { initial = {!!} ; chain∋init = {!!}  ; supf = supf1  ; sup=u = {!!} 
-               ; supf-is-sup = ?
+               ; sup = ? ; supf-is-sup = ?
                ;  chain⊆A = {!!} ;  f-next = {!!} ;  f-total = {!!} ; csupf = ? ; supf-mono = ? } where -- x is a sup of (zc ?) 
           ... | case2 ¬x=sup =  no-extension ? -- x is not f y' nor sup of former ZChain from y -- no extention