--- a/src/zorn.agda	Tue Aug 16 16:29:57 2022 +0900
+++ b/src/zorn.agda	Tue Aug 16 21:54:03 2022 +0900
@@ -803,19 +803,32 @@
                       zc60 (fsuc w1 fc) with zc60 fc
                       ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫ 
                       ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫ 
+                 chp10 : {u : Ordinal } → u o< x → ChainP A f mf ay supf1 u → ChainP A f mf ay supf0 u
+                 chp10 = ?
+                 fc10 : {w : Ordinal } → u o< x → FClosure A f supf1 w → FClosure A f supf0 w 
+                 fc10 = ?
                  sup : {z : Ordinal} → z o< x → SUP A (UnionCF A f mf ay supf1 z)
                  sup {z} z<x with trio< z px
-                 ... | tri< a ¬b ¬c = SUP⊆ (UnionCFR⊆ o≤-refl ? (o<→≤ a)) ( ZChain.sup zc  a )
-                 ... | tri≈ ¬a b ¬c = record { sup = SUP.sup sup1 ; as = SUP.as sup1 ; x<sup = zc61 } where
-                     zc61 : {w : HOD} → UnionCF A f mf ay supf1 z ∋ w → (w ≡ SUP.sup sup1) ∨ (w < SUP.sup sup1)
-                     zc61 {w} lt = ?
+                 ... | tri< a ¬b ¬c = SUP⊆ (UnionCFR⊆ o≤-refl (ordtrans z<x <-osuc) (o<→≤ a)) ( ZChain.sup zc  a ) 
+                 ... | tri≈ ¬a b ¬c = record { sup = SUP.sup sup1 ; as = SUP.as sup1 ; x<sup = λ {w} lt → zc61 (subst (λ k → UnionCF A f mf ay supf1 k ∋ w) b lt) } where
+                     zc61 : {w : HOD} → UnionCF A f mf ay supf1 px ∋ w → (w ≡ SUP.sup sup1) ∨ (w < SUP.sup sup1)
+                     zc61 {w} ⟪ au , ch-init fc ⟫  with SUP.x<sup sup1 ⟪ au , ch-init fc ⟫ 
+                     ... | case1 eq = case1 eq
+                     ... | case2 lt = case2 lt
+                     zc61 {w} ⟪ au , ch-is-sup u u≤px is-sup fc ⟫ with SUP.x<sup sup1 ⟪ au , ch-is-sup u (subst (λ k → u o≤ k) (Oprev.oprev=x op) (ordtrans u≤px <-osuc))  ? ? ⟫ 
+                     ... | case1 eq = case1 eq
+                     ... | case2 lt = case2 lt
                  ... | tri> ¬a ¬b px<z = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ )
                  sup=u : {b : Ordinal} (ab : odef A b) →
                     b o≤ x → IsSup A (UnionCF A f mf ay supf1 (osuc b)) ab → supf1 b ≡ b
                  sup=u {b} ab b≤x is-sup with trio< b px
                  ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) record { x<sup = {!!} }
-                 ... | tri≈ ¬a b ¬c = ?
-                 ... | tri> ¬a ¬b px<b = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) ? ⟫ )
+                 ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab {!!} record { x<sup = {!!} }
+                 ... | tri> ¬a ¬b px<b = {!!} where
+                     zc30 : x ≡ b
+                     zc30 with osuc-≡< b≤x
+                     ... | case1 eq = sym (eq)
+                     ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ )
                  csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 b) (supf1 b)
                  csupf {b} b≤x with trio< b px | inspect supf1 b
                  ... | tri< a ¬b ¬c | _ = UnionCF⊆ o≤-refl (o<→≤ a) b≤x ( ZChain.csupf zc (o<→≤ a) )
@@ -960,18 +973,18 @@
                  sup : {z : Ordinal} → z o< x → SUP A (UnionCF A f mf ay supf1 z)
                  sup {z} z≤x with trio< z x
                  ... | tri< a ¬b ¬c = SUP⊆ (UnionCF⊆ a) (ZChain.sup (pzc (osuc z) {!!}) {!!} )
-                 ... | tri≈ ¬a b ¬c = ?
-                 ... | tri> ¬a ¬b c = ?
-                 sis : {z : Ordinal} (x≤z : z o< x) → supf1 z ≡ & (SUP.sup (sup ?))
+                 ... | tri≈ ¬a b ¬c = {!!}
+                 ... | tri> ¬a ¬b c = {!!}
+                 sis : {z : Ordinal} (x≤z : z o< x) → supf1 z ≡ & (SUP.sup (sup {!!}))
                  sis {z} z<x with trio< z x
                  ... | tri< a ¬b ¬c = {!!} where
-                     zc8 = ZChain.supf-is-sup (pzc z a) ?
-                 ... | tri≈ ¬a b ¬c = ?
-                 ... | tri> ¬a ¬b c = ?
+                     zc8 = ZChain.supf-is-sup (pzc z a) {!!}
+                 ... | tri≈ ¬a b ¬c = {!!}
+                 ... | tri> ¬a ¬b c = {!!}
                  sup=u : {b : Ordinal} (ab : odef A b) → b o≤ x → IsSup A (UnionCF A f mf ay supf1 (osuc b)) ab → supf1 b ≡ b
                  sup=u {b} ab b<x is-sup with trio< b x
                  ... | tri< a ¬b ¬c = ZChain.sup=u (pzc (osuc b)  (ob<x lim a))  ab {!!} record { x<sup = {!!} }
-                 ... | tri≈ ¬a b ¬c = {!!}
+                 ... | tri≈ ¬a b ¬c = {!!} -- ZChain.sup=u (pzc (osuc ?)  ?)  ab {!!} record { x<sup = {!!} }
                  ... | tri> ¬a ¬b c = {!!}
                  csupf : {z : Ordinal} → z o≤ x → odef (UnionCF A f mf ay supf1 z) (supf1 z)
                  csupf {z} z≤x with trio< z x