--- a/src/zorn.agda	Sun Oct 02 19:30:19 2022 +0900
+++ b/src/zorn.agda	Mon Oct 03 01:43:00 2022 +0900
@@ -1042,9 +1042,11 @@
                               zc17 :  {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 px →
                                     FClosure A f (supf1 s) z1 → (z1 ≡ supf1 px) ∨ (z1 << supf1 px)
                               zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) (trans (cong supf0 b) (sym (sf1=sf0 o≤-refl)))
-                                ( ChainP.order is-sup (subst₂ (λ j k → j o< k) (sf1=sf0 s≤px) ? ss<spx) (fcup fc s≤px) ) where
+                                ( ChainP.order is-sup (subst₂ (λ j k → j o< k) (sf1=sf0 s≤px) zc19 ss<spx) (fcup fc s≤px) ) where
+                                  zc19 : supf1 px ≡ supf0 u
+                                  zc19 = trans (sf1=sf0 o≤-refl) (cong supf0 (sym b))
                                   s≤px : s o≤ px
-                                  s≤px = ?
+                                  s≤px = o<→≤ (supf-inject0 supf-mono1 ss<spx)
                           ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , (ordtrans u<x <-osuc )   ⟫ )
                       zc12 {z} (case2 fc) = zc21 fc where
                           zc21 : {z1 : Ordinal } → FClosure A f px z1 → odef (UnionCF A f mf ay supf1 x) z1
@@ -1061,7 +1063,21 @@
                               zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 o≤-refl)) ( ZChain.fcy<sup zc o≤-refl fc )
                               zc17 :  {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 px →
                                     FClosure A f (supf1 s) z1 → (z1 ≡ supf1 px) ∨ (z1 << supf1 px)
-                              zc17 {s} {z1} ss<spx fc = ?
+                              zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k )) mins-is-spx 
+                                     (MinSUP.x<sup mins (csupf17 (fcup fc (o<→≤ s<px) )) ) where
+                                  mins : MinSUP A (UnionCF A f mf ay supf0 px)
+                                  mins = ZChain.minsup zc o≤-refl
+                                  mins-is-spx : MinSUP.sup mins ≡ supf1 px 
+                                  mins-is-spx = trans (sym ( ZChain.supf-is-minsup zc o≤-refl ) ) (sym (sf1=sf0 o≤-refl ))
+                                  s<px : s o< px
+                                  s<px = supf-inject0 supf-mono1 ss<spx
+                                  sf<px : supf0 s o< px
+                                  sf<px = subst₂ (λ j k → j o< k ) (sf1=sf0 (o<→≤ s<px)) (trans (sf1=sf0 o≤-refl) (sym sfpx=px)) ss<spx
+                                  -- (sf1=sf0 ?) (trans ? sfpx=px ) ss<spx
+                                  csupf17 : {z1 : Ordinal } → FClosure A f (supf0 s) z1 → odef (UnionCF A f mf ay supf0 px) z1
+                                  csupf17 (init as refl ) = ZChain.csupf zc sf<px 
+                                  csupf17 (fsuc x fc) = ZChain.f-next zc (csupf17 fc)
+
 
                  record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where
                      field
@@ -1080,23 +1096,24 @@
                          ; x<sup = ? ; minsup = ? } ; tsup=sup = ? } 
 
 
-                 csupf1 : {b : Ordinal } → supf1 b o< x → odef (UnionCF A f mf ay supf1 x) (supf1 b) 
-                 csupf1 {b} sb<z = ⟪ asb , ch-is-sup (supf1 b) sb<z 
-                     record { fcy<sup = ?  ; order = order ; supu=u = ? }  
-                        (init ? ? ) ⟫ where
-                    b<x : b o< x
-                    b<x = ZChain.supf-inject zc ?
-                    asb : odef A (supf1 b)
-                    asb = ? --  ZChain.supf∈A zc ? -- (o<→≤ b<x)
-                    supb : SUP A (UnionCF A f mf ay supf1 (supf1 b))
-                    supb = ? -- ZChain.sup zc (o<→≤ sb<z)
-                    supb-is-b : supf1 (supf1 b) ≡ & (SUP.sup supb)
-                    supb-is-b = ? -- ZChain.supf-is-sup zc ? -- (o<→≤ sb<z)
-                    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 {s} {z1} ss<ssb fs with SUP.x<sup supb ?
-                    ... | case1 eq = ?
-                    ... | case2 lt = ?
+                 csupf1 : {z1 : Ordinal } → supf1 z1 o< x → odef (UnionCF A f mf ay supf1 x) (supf1 z1) 
+                 csupf1 {z1} sz1<x with trio< (supf0 z1) px
+                 ... | tri< a ¬b ¬c = subst₂ (λ j k → odef j k ) (sym ch1x=pchainpx) (sym (sf1=sf0 z1≤px)) (case1 (ZChain.csupf zc a )) where
+                        z1≤px : z1 o≤ px
+                        z1≤px = o<→≤ ( ZChain.supf-inject zc (subst (λ k → supf0 z1 o< k ) sfpx=px a ))
+                 ... | tri≈ ¬a b ¬c = subst₂ (λ j k → odef j k ) (sym ch1x=pchainpx) zc20 (case2 (init apx sfpx=px )) where
+                      z1≤px : z1 o≤ px
+                      z1≤px with trio< z1 px
+                      ... | tri< a ¬b ¬c = o<→≤ a
+                      ... | tri≈ ¬a b ¬c = o≤-refl0 b
+                      ... | tri> ¬a ¬b c = ⊥-elim ( o<> c ( supf-inject0 supf-mono1 (subst (λ k → supf1 z1 o< k ) refl ?) ) )
+                      zc20 : supf0 px ≡ supf1 z1 
+                      zc20 = begin
+                        supf0 px  ≡⟨ ? ⟩
+                        px  ≡⟨ ? ⟩
+                        supf0 z1  ≡⟨ ? ⟩
+                        supf1 z1 ∎ where open ≡-Reasoning
+                 ... | tri> ¬a ¬b c = ⊥-elim ( ? )
 
           ... | case2 px<spfx = ? where