# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1671177644 -32400
# Node ID c2546206c891fc6f161fb7181562f16d4f4be130
# Parent  2624f8a9f6edae2756b55d0dd01ec6b617a14673
order done

diff -r 2624f8a9f6ed -r c2546206c891 src/zorn.agda
--- a/src/zorn.agda	Fri Dec 16 12:25:17 2022 +0900
+++ b/src/zorn.agda	Fri Dec 16 17:00:44 2022 +0900
@@ -1588,6 +1588,9 @@
                    zc44 : FClosure A f (supf1 u) w
                    zc44 = subst (λ k → FClosure A f k w ) (sym zc45) fc
 
+          zo≤sz : {z : Ordinal} →  z o≤ x → z o≤ supf1 z
+          zo≤sz = ?
+
           order : {a b 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 (trans (sf1=sf b<x) (sym (zeq _ _ (o<→≤ <-osuc) o≤-refl ))))  (
@@ -1604,9 +1607,22 @@
                a<x : a o< x
                a<x = supf-inject0 supf-mono sa<sb
                zc40 : ZChain.supf (pzc  (ob<x lim a<x )) a o< spu → FClosure A f (ZChain.supf (pzc  (ob<x lim a<x )) a) w → w ≤ spu
-               zc40 sa<sp fc = MinSUP.x≤sup usup ⟪ A∋fc _ f mf fc , ic-isup a a<x zc44 fc ⟫ where
-                     zc44 : supfz a<x o≤ a
-                     zc44 = ?
+               zc40 sa<sp fc with x<y∨y≤x (supfz a<x) x
+               ... | case1 sa<x = z29 where
+                      z28 : odef (UnionCF A f ay supf1 b) w
+                      z28 = cfcs a<x o≤-refl (subst (λ k → k o< x) (sym (sf1=sf a<x)) sa<x) (subst (λ k → FClosure A f k w ) (sym (sf1=sf a<x)) fc )
+                      z29 : w ≤ spu
+                      z29 with z28
+                      ... | ⟪ aw , ch-init fc ⟫ = MinSUP.x≤sup usup ⟪ aw , ic-init fc ⟫
+                      ... | ⟪ aw , ch-is-sup u u<b su=u fc ⟫ = MinSUP.x≤sup usup ⟪ aw , ic-isup u u<b z30
+                                    (subst (λ k → FClosure A f k w) (sf1=sf u<b) fc) ⟫ where
+                          z30 : supfz u<b o≤ u
+                          z30 = o≤-refl0 ( trans (sym (sf1=sf u<b)) su=u )
+               ... | case2 x≤sa = ⊥-elim ( o<¬≡ z27 sa<sb ) where
+                      z27 : supf1 a ≡ supf1 b
+                      z27 = begin
+                         supf1 a  ≡⟨ ( supfeq1 (o<→≤ a<x) o≤-refl ( union-max1 (subst (λ k → x o≤ k ) (sym (sf1=sf a<x)) x≤sa ) b≤x sa<sb) ) ⟩
+                         supf1 x  ∎ where open ≡-Reasoning
 
      ---
      --- the maximum chain  has fix point of any ≤-monotonic function