# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1670378796 -32400
# Node ID aebab71cc386a6954a5f87ef4cf8240da5d9df42
# Parent  e99e2bcb885cee00a3eb3d4b241481c969e509e8
...

diff -r e99e2bcb885c -r aebab71cc386 src/zorn.agda
--- a/src/zorn.agda	Mon Dec 05 15:09:41 2022 +0900
+++ b/src/zorn.agda	Wed Dec 07 11:06:36 2022 +0900
@@ -1094,50 +1094,94 @@
 
                  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 with osuc-≡< b≤x
-                 ... | case2 b<x = 
-                    subst ( λ k → w ≤ k ) (sym (sf1=sf0 ?)) ( ZChain.order zc (zc-b<x _ b<x) 
-                       (subst₂ (λ j k → j o< k ) (sf1=sf0 ?) (sf1=sf0 ?) sa<sb) (fcup fc ?)  )
-                 ... | case1 eq with zc43 (supf1 a) b
-                 ... | case1 sa<b = subst (λ k → w ≤ k ) (sym (sf1=sp1 ? )) ( MinSUP.x≤sup sup1 ?)  where
-                     z26 : odef pchainpx w 
-                     z26 =  zc11 (chain-mono f mf ay supf1 supf1-mono ? (cfcs ? b≤x ? fc))
-                 ... | case2 b≤sa = ⊥-elim ( o≤> z27 sa<sb ) where
-                     z28 : supf1 (supf0 a) ≡ supf1 a -- x o≤ supf1 a  → 
-                     z28 with zc43 (supf0 a) x
-                     ... | case1 sa<x = subst₂ (λ j k → j ≡ k) ? ? ( ZChain.supf-idem zc ? ? )
-                     ... | case2 x≤sa with osuc-≡< ( supf1-mono x≤sa )   -- = ?  --  sp1 ≡ supf0 a   --- sp1 o≤ supf0 a
-                     ... | case1 eq = sym (trans z29 eq ) where
-                          z30 : supf1 (supf0 a) ≡ supf1 (supf0 a) 
-                          z30 = ?
-                          z29 : supf1 a ≡ supf1 x
-                          z29 = ?
-                          z32 : supf1 x ≡ supf1 (supf0 a) -- supf1 (supf0 a) ≡ supf1 a
-                          z32 = eq 
-                     ... | case2 lt = ? where
-                          z31 : supf1 x o< supf1 (supf0 a)
-                          z31 = lt
+                 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 = ?
 
-                     z27 : supf1 b o≤ supf1 a
-                     z27 = begin 
-                       supf1 b ≤⟨ ? ⟩
-                       supf1 (supf1 a) ≡⟨ ? ⟩
-                       supf1 a ∎ where open o≤-Reasoning O
-
+                 --  
+                 -- 
                  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
                  ... | tri< a ¬b ¬c = ? -- ZChain.sup=u zc ab (o<→≤ a) is-sup
                  ... | tri≈ ¬a b ¬c = ? -- ZChain.sup=u zc ab (o≤-refl0 b) is-sup
-                 ... | tri> ¬a ¬b px<b = ? where
-                     zc30 : x ≡ b
-                     zc30 with osuc-≡< b≤x
+                 ... | tri> ¬a ¬b px<b = trans zc36 x=b where
+                     x=b : x ≡ b
+                     x=b 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 ⟫ )
                      zc31 : sp1 o≤ b
                      zc31 = MinSUP.minsup sup1 ab zc32 where
                          zc32 : {w : Ordinal } → odef pchainpx w → (w ≡ b) ∨ (w << b)
-                         zc32 = ?
+                         zc32 {w} (case1 uw) = IsSUP.x≤sup (proj1 is-sup) ?
+                         zc32 {w} (case2 fc) = IsSUP.x≤sup (proj1 is-sup) ⟪ A∋fc _ f mf (proj1 fc) , ch-is-sup (supf0 px) sa<x su=u fc1 ⟫ where
+                             su=u : supf1 (supf0 px) ≡ supf0 px
+                             su=u = trans (sf1=sf0 (zc-b<x _ (proj2 fc))) ( ZChain.supf-idem zc o≤-refl (zc-b<x _ (proj2 fc)) )
+                             fc1 : FClosure A f (supf1 (supf0 px)) w
+                             fc1 = subst (λ k → FClosure A f k w ) (sym su=u) (proj1 fc)
+                             sa<x : supf0 px o< b
+                             sa<x = subst (λ k → supf0 px o< k ) x=b ( proj2 fc)
+                     zc36 : sp1 ≡ x   -- this cannot heppen because px o< supf0 px ( px o≤ spuf0 px o< supf1 x ≡ x → ⊥ )
+                     zc36 with osuc-≡< zc31
+                     ... | case1 eq = trans eq (sym x=b)
+                     ... | case2 sp1<b with osuc-≡< ( zc-b<x _ (subst (λ k → sp1 o< k ) ? sp1<b))
+                     ... | case1 sp1=px = ⊥-elim ( <<-irr ?  z42 ) where 
+                          z40 : odef pchainpx (f (supf1 sp1))
+                          z40 = case2 ⟪ fsuc _ (init ? ?) , ? ⟫
+                          z41 : f (supf1 sp1) ≤ sp1
+                          z41 = MinSUP.x≤sup sup1 z40
+                          z44 : sp1 ≤ supf1 sp1
+                          z44 = ?
+                          z43 : px o≤ supf0 px 
+                          z43 with zc43 (supf0 px) px
+                          ... | case2 le = le
+                          ... | case1 spx<px = ⊥-elim ( <<-irr z45 (proj1 ( mf< (supf0 px) (ZChain.asupf zc)))) where 
+                             z46 : odef (UnionCF A f ay supf1 px) (f (supf1 px))
+                             z46 = ⟪ proj2 ( mf (supf1 px) ?) , ch-is-sup (supf0 px) spx<px z48 (fsuc _ (init ? z47 )) ⟫ where
+                                 z47 : supf1 (supf0 px) ≡ supf1 px
+                                 z47 = subst₂ (λ j k → j ≡ k ) (sym (sf1=sf0 ?)) (sym (sf1=sf0 ?)) ( ZChain.supf-idem zc o≤-refl (o<→≤ spx<px) )
+                                 z48 : supf1 (supf0 px) ≡ supf0 px
+                                 z48 = subst (λ k → k ≡ supf0 px ) (sym (sf1=sf0 ?)) ( ZChain.supf-idem zc o≤-refl (o<→≤ spx<px) )
+                             z45 : f (supf0 px) ≤ supf0 px
+                             z45 = subst (λ k → f k ≤ k ) ? ( IsMinSUP.x≤sup (is-minsup ?  ) z46 )
+                          z42 : (supf1 sp1) << f (supf1 sp1)
+                          z42 = proj1 ( mf< (supf1 sp1) ? )
+                     ... | case2 sp1<px = ⊥-elim ( o≤> z39 z44 ) where  
+                          z39 : supf1 px o≤ supf1 x   -- supf0 px o≤ px 
+                          z39 = supf1-mono (o<→≤ px<x) 
+                          z43 : px o≤ supf0 px 
+                          z43 with zc43 (supf0 px) px
+                          ... | case2 le = le
+                          ... | case1 spx<px = ⊥-elim ( <<-irr z45 (proj1 ( mf< (supf0 px) (ZChain.asupf zc)))) where 
+                             z46 : odef (UnionCF A f ay supf1 px) (f (supf1 px))
+                             z46 = ⟪ proj2 ( mf (supf1 px) ?) , ch-is-sup (supf0 px) spx<px z48 (fsuc _ (init ? z47 )) ⟫ where
+                                 z47 : supf1 (supf0 px) ≡ supf1 px
+                                 z47 = subst₂ (λ j k → j ≡ k ) (sym (sf1=sf0 ?)) (sym (sf1=sf0 ?)) ( ZChain.supf-idem zc o≤-refl (o<→≤ spx<px) )
+                                 z48 : supf1 (supf0 px) ≡ supf0 px
+                                 z48 = subst (λ k → k ≡ supf0 px ) (sym (sf1=sf0 ?)) ( ZChain.supf-idem zc o≤-refl (o<→≤ spx<px) )
+                             z45 : f (supf0 px) ≤ supf0 px
+                             z45 = subst (λ k → f k ≤ k ) ? ( IsMinSUP.x≤sup (is-minsup ?  ) z46 )
+                          z44 : supf1 x o< supf1 px
+                          z44 = osucprev ( begin
+                             osuc (supf1 x) ≡⟨ cong osuc (sf1=sp1 px<x) ⟩
+                             osuc sp1 ≤⟨ osucc sp1<px ⟩
+                             px ≤⟨ z43 ⟩
+                             supf0 px ≡⟨ sym (sf1=sf0 o≤-refl )  ⟩
+                             supf1 px ∎ ) where open o≤-Reasoning O
 
      ... | no lim with trio< x o∅
      ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )