# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1661133780 -32400
# Node ID b91681b604d8e67a1ed10b6da89ef091950c4b12
# Parent  507f6582c31da4790879fb9918e039f79082f597
...

diff -r 507f6582c31d -r b91681b604d8 src/zorn.agda
--- a/src/zorn.agda	Mon Aug 22 07:39:18 2022 +0900
+++ b/src/zorn.agda	Mon Aug 22 11:03:00 2022 +0900
@@ -304,12 +304,35 @@
    ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso  (trans (cong (&) eq) (sym (supf-is-sup u<z ) ) ))
    ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup u<z ))) ) lt )
 
-   csupf-fc : {b s z1 : Ordinal} → b o≤ z → supf s o< supf b → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1
-   csupf-fc {b} {s} {z1} b≤<z ss<sb (init x refl ) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc05  where
+   csupf-fc : {b s z1 : Ordinal} → b o≤ z → supf s o≤ supf b → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1
+   csupf-fc {b} {s} {z1} b≤z ss≤sb (init x refl ) with osuc-≡< ss≤sb
+   ... | case1 eq = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc05  where
+            zc04 : odef (UnionCF A f mf ay supf (supf s))  (supf s)
+            zc04 = subst (λ k → odef (UnionCF A f mf ay supf k)  k) (sym eq) ( csupf b≤z  )
+            zc05 : odef (UnionCF A f mf ay supf b)  (supf s)
+            zc05 with zc04
+            ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc  ⟫ 
+            ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = zc09 u≤x where
+                zc06 : supf u ≡ u
+                zc06 = ChainP.supu=u is-sup
+                zc09 : u o≤ supf s  →  odef (UnionCF A f mf ay supf b)  (supf s)
+                zc09 u≤ss with osuc-≡< (subst (λ k → k o≤ supf s) (sym zc06) u≤ss)
+                ... | case1 su=ss = zc08 where
+                    zc07 : supf u o≤ supf b   
+                    zc07 = subst₂ (λ j k → j o≤ k) (sym zc06) eq u≤ss
+                    zc08 :  odef (UnionCF A f mf ay supf b)  (supf s)
+                    zc08 with osuc-≡< zc07
+                    ... | case2 lt =  ⟪ as , ch-is-sup u (o<→≤ (supf-inject lt )) is-sup fc ⟫ 
+                    ... | case1 su=sb with trio< u b
+                    ... | tri< u<b ¬b ¬c = ?
+                    ... | tri≈ ¬a u=b ¬c = ?
+                    ... | tri> ¬a ¬b b<u = ⟪ ? , ch-is-sup (supf b) ? ? ? ⟫
+                ... | case2 lt =  ⟪ as , ch-is-sup u (o<→≤ (supf-inject (subst (λ k → supf u o< k) eq lt ))) is-sup fc ⟫ 
+   ... | case2 ss<sb = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc05  where
             s<b : s o< b
             s<b = supf-inject ss<sb
             s≤<z : s o≤ z
-            s≤<z = ordtrans s<b b≤<z
+            s≤<z = ordtrans s<b b≤z
             zc04 : odef (UnionCF A f mf ay supf (supf s))  (supf s)
             zc04 = csupf s≤<z 
             zc05 : odef (UnionCF A f mf ay supf b)  (supf s)
@@ -328,15 +351,15 @@
                     ... | case1 su=sb = ⊥-elim ( o<¬≡ (trans (sym su=ss) su=sb ) ss<sb )
                     ... | case2 lt =  o<→≤ (supf-inject lt )
                 ... | case2 lt =  o<→≤ (ordtrans (supf-inject lt) s<b) 
-   csupf-fc {b} {s} {z1} b<z ss<sb (fsuc x fc) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc04  where
+   csupf-fc {b} {s} {z1} b<z ss≤sb (fsuc x fc) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc04  where
             zc04 : odef (UnionCF A f mf ay supf b) (f x)
-            zc04 with subst (λ k → odef (UnionCF A f mf ay supf b) k ) &iso (csupf-fc b<z ss<sb fc  )
+            zc04 with subst (λ k → odef (UnionCF A f mf ay supf b) k ) &iso (csupf-fc b<z ss≤sb fc  )
             ... | ⟪ as , ch-init fc ⟫ = ⟪ proj2 (mf _ as) , ch-init (fsuc _ fc) ⟫ 
             ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf _ as) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫ 
-   order : {b s z1 : Ordinal} → b o< z → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
-   order {b} {s} {z1} b<z ss<sb fc = zc04 where
+   order : {b s z1 : Ordinal} → b o< z → supf s o≤ supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
+   order {b} {s} {z1} b<z ss≤sb fc = zc04 where
       zc00 : ( * z1  ≡  SUP.sup (sup b<z )) ∨ ( * z1  < SUP.sup ( sup b<z ) )
-      zc00 = SUP.x<sup (sup  b<z) (csupf-fc (o<→≤ b<z) ss<sb fc )
+      zc00 = SUP.x<sup (sup  b<z) (csupf-fc (o<→≤ b<z) ss≤sb fc )
       zc04 : (z1 ≡ supf b) ∨ (z1 << supf b)
       zc04 with zc00
       ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso (sym (supf-is-sup  b<z)  ) (cong (&) eq) )
@@ -541,7 +564,7 @@
               m08 {z} fcz = ZChain.fcy<sup zc b<A fcz
               m09 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b 
                            → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b
-              m09 {s} {z} s<b fcz = ZChain.order zc b<A s<b fcz    
+              m09 {s} {z} s<b fcz = ZChain.order zc b<A (o<→≤ s<b) fcz    
               m06 : ChainP A f mf ay (ZChain.supf zc) b 
               m06 = record {  fcy<sup = m08  ; order = m09 ; supu=u = ZChain.sup=u zc ab (o<→≤ b<A )
                       record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono1 (o<→≤ b<x) uz ) } }  
@@ -561,7 +584,7 @@
               m07 {z} fc = ZChain.fcy<sup zc  m09 fc
               m08 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b 
                        → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b
-              m08 {s} {z1} s<b fc = ZChain.order zc m09 s<b fc
+              m08 {s} {z1} s<b fc = ZChain.order zc m09 (o<→≤ s<b) fc
               m05 : b ≡ ZChain.supf zc b
               m05 = sym (ZChain.sup=u zc ab (o<→≤  m09)
                       record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono1 (o<→≤ b<x) lt )} )   -- ZChain on x