--- a/src/zorn.agda	Thu Dec 08 07:55:31 2022 +0900
+++ b/src/zorn.agda	Fri Dec 09 11:10:41 2022 +0900
@@ -1108,28 +1108,6 @@
                                 u≤px : u o≤ px
                                 u≤px = ordtrans u<x z≤px
 
-                 order : {a b : Ordinal} {w : Ordinal} →
-                    b o≤ x → supf1 a o< supf1 b → FClosure A f (supf1 a) w → w ≤ supf1 b
-                 order {a} {b} {w} b≤x sa<sb fc = z20 where
-                     a<b : a o< b
-                     a<b = supf-inject0 supf1-mono sa<sb
-                     z20 : w ≤ supf1 b
-                     z20 with trio< b px
-                     ... | tri< b<px ¬b ¬c = ZChain.order zc (o<→≤ b<px) (subst (λ k → k o< supf0 b) (sf1=sf0 (o<→≤ (ordtrans a<b b<px))) sa<sb) 
-                          (fcup fc (o<→≤ (ordtrans a<b b<px))) 
-                     ... | tri≈ ¬a b=px ¬c = IsMinSUP.x≤sup (ZChain.is-minsup zc (o≤-refl0 b=px)) z26  where 
-                          sa<b : supf1 a o< b  -- px
-                          sa<b = ?
-                          z26 : odef ( UnionCF A f ay supf0 b ) w 
-                          z26 =  ?
-                          z27 : odef ( UnionCF A f ay supf1 b ) w 
-                          z27 =  cfcs a<b b≤x sa<b fc  
-                     ... | tri> ¬a ¬b px<b = MinSUP.x≤sup sup1 (zc11 ( chain-mono f mf ay supf1 supf1-mono b≤x (cfcs a<b b≤x sa<b fc))) where
-                          sa<b : supf1 a o< b   --  b ≡ x
-                          sa<b = ?
-
-                 --  
-                 -- 
                  sup=u : {b : Ordinal} (ab : odef A b) →
                     b o≤ x → IsSUP A (UnionCF A f ay supf1 b) b ∧ (¬ HasPrev A (UnionCF A f ay supf1 b) f b ) → supf1 b ≡ b
                  sup=u {b} ab b≤x is-sup with trio< b px
@@ -1200,6 +1178,59 @@
                         zc40 = subst (λ k → f (supf0 px) ≤ k ) (sym zc39) 
                            ( MinSUP.x≤sup sup1 (case2 ⟪ fsuc _ (init (ZChain.asupf zc) refl) , subst (λ k → k o< x) (sym zc37) px<x ⟫  ))
 
+                 order : {a b : Ordinal} {w : Ordinal} →
+                    b o≤ x → supf1 a o< supf1 b → FClosure A f (supf1 a) w → w ≤ supf1 b
+                 order {a} {b} {w} b≤x sa<sb fc = z20 where
+                     a<b : a o< b
+                     a<b = supf-inject0 supf1-mono sa<sb
+                     a≤px : a o≤ px
+                     a≤px with trio< a px
+                     ... | tri< a ¬b ¬c = o<→≤ a
+                     ... | tri≈ ¬a b ¬c = o≤-refl0 b
+                     ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → a o< k) (sym (Oprev.oprev=x op)) 
+                        ( ordtrans<-≤ a<b b≤x) ⟫ ) -- px o< a o< b o≤ x
+                     spx<x : supf0 px o< x
+                     spx<x = ?
+                     spx<=sb : supf0 px ≤ sp1
+                     spx<=sb = MinSUP.x≤sup sup1 (case2 ⟪ init (ZChain.asupf zc) refl , ? ⟫ )
+                     sa<<sb : supf1 a << supf1 b
+                     sa<<sb with osuc-≡< b≤x
+                     ... | case2 b<x = subst₂ (λ j k → j << k ) (sym (sf1=sf0 ?)) (sym (sf1=sf0 ?)) ( ZChain.supf-mono< zc (zc-b<x _ b<x) 
+                         (subst₂ (λ j k → j o< k) (sf1=sf0 ?) (sf1=sf0 ?)  sa<sb ))
+                     ... | case1 b=x with osuc-≡< ( supf1-mono a≤px )   --   supf1 a ≤ supf1 px << sp1
+                     ... | case2 sa<spx = subst₂ (λ j k → j << k ) (sym (sf1=sf0 ?)) (sym (sf1=sp1 ?))
+                        ( ftrans<-≤ ( ZChain.supf-mono< zc o≤-refl (subst₂ (λ j k → j o< k) (sf1=sf0 ?) (sf1=sf0 ?) sa<spx)) spx<=sb )
+                     ... | case1 sa=spx with spx<=sb
+                     ... | case2 lt = subst₂ (λ j k → j << k ) ? ? lt
+                     ... | case1 eq = ?
+                     -- supf1 a o≤ x
+                     --    x o< supf1 a o< supf1 b -> UnionCF px ⊆ UnionCF a → supf0 px ≡ supf0 a → ⊥
+                     --    a o≤ supf1 a
+                     sa<x : supf1 a o< x    -- supf1 a o< supf1 x ≡ sp1 ( supf of fc (supf0 px) ∧ (supf0 px o< x)
+                     sa<x with x<y∨y≤x (supf1 a) x
+                     ... | case1 lt = lt
+                     ... | case2 x≤sa = ⊥-elim ( <<-irr z27 sa<<sb ) where
+                          z27 : supf1 b ≤ supf1 a
+                          z27 = subst (λ k → supf1 b ≤ k ) ? (IsMinSUP.x≤sup (is-minsup ? ) ? )
+                     ssa=sa : supf1 a ≡ supf1 (supf1 a)   -- supf0 a o≤ px
+                     ssa=sa = sym ( sup=u ? ? ? )
+                     sa<b : supf1 a o< b  -- supf1 (supf1 a) ≡ supf1 a o< supf1 b  → inject supf1 a o< b
+                     sa<b = supf-inject0 supf1-mono (subst (λ k → k o< supf1 b ) ? sa<sb )
+                     z20 : w ≤ supf1 b
+                     z20 with trio< b px
+                     ... | tri< b<px ¬b ¬c = ZChain.order zc (o<→≤ b<px) (subst (λ k → k o< supf0 b) (sf1=sf0 (o<→≤ (ordtrans a<b b<px))) sa<sb) 
+                          (fcup fc (o<→≤ (ordtrans a<b b<px))) 
+                     ... | tri≈ ¬a b=px ¬c = IsMinSUP.x≤sup (ZChain.is-minsup zc (o≤-refl0 b=px)) z26  where 
+                          -- sa<b : supf1 a o< b  -- px
+                          -- sa<b = ?
+                          z26 : odef ( UnionCF A f ay supf0 b ) w 
+                          z26 with cfcs a<b b≤x sa<b fc  
+                          ... | ⟪ ua , ch-init fc ⟫ = ⟪ ua , ch-init fc ⟫ 
+                          ... | ⟪ ua , ch-is-sup u u<x su=u fc ⟫ = ⟪ ua , ch-is-sup u ? ? ? ⟫ 
+                     ... | tri> ¬a ¬b px<b = MinSUP.x≤sup sup1 (zc11 ( chain-mono f mf ay supf1 supf1-mono b≤x (cfcs a<b b≤x sa<b fc))) 
+                          -- sa<b : supf1 a o< b   --  b ≡ x
+                          -- sa<b = ?
+
      ... | no lim with trio< x o∅
      ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
      ... | tri≈ ¬a b ¬c = record { supf = ? ; sup=u = ? ; asupf = ? ; supf-mono = ? ; order = ?