# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1662249053 -32400
# Node ID 56a150965988f73441c1adf78bbb027ad4b5c84b
# Parent  bf1b6c4768d2ecce58830032499b4bf100e03ac2
...

diff -r bf1b6c4768d2 -r 56a150965988 src/zorn.agda
--- a/src/zorn.agda	Sat Sep 03 13:28:10 2022 +0900
+++ b/src/zorn.agda	Sun Sep 04 08:50:53 2022 +0900
@@ -973,29 +973,40 @@
                      csupf1 with csupf0
                      ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ 
                      ... | ⟪ as , ch-is-sup u u≤x record { fcy<sup = fcy<sup ; order = order ; supu=u = supu=u } fc  ⟫ 
-                        =  ⟪ as  , ch-is-sup u u≤x record { fcy<sup = fcy<sup1 ; order = order1 ; supu=u = supu=u1 }  ? ⟫  where
-                         zc13 : supf0 u o< supf0 b
-                         zc13 = ?
-                         zc12 :  odef (UnionCF A f mf ay supf0 b) (supf1 b)
-                         zc12 = subst (λ k → odef (UnionCF A f mf ay supf0 b) k) &iso ( ZChain.csupf-fc zc b≤px zc13 fc  )
-                         u≤x1 : u o≤ supf1 b 
-                         u≤x1 = u≤x
-                         supu=u0 : supf0 u ≡ u
-                         supu=u0 = supu=u
+                         with osuc-≡< (subst₂ (λ j k → j o≤ k ) (sym supu=u ) (sym (supf0=1 b≤px)) u≤x)
+                     ... | case1 eq = ⟪ as  , ch-is-sup u u≤x record { fcy<sup = fcy<sup1 ; order = order1 ; supu=u = supu=u1 } fc1 ⟫  
+                       where
+                         s0b=s0u  : supf0 u ≡ supf0 b   -- u ≡ supf0 b 
+                         s0b=s0u  = eq
+                         u≤sb : u o≤ supf1 b
+                         u≤sb = u≤x
                          supu=u1 : supf1 u ≡ u
                          supu=u1 with trio< u px
                          ... | tri< a ¬b ¬c = supu=u 
                          ... | tri≈ ¬a b ¬c = supu=u 
                          ... | tri> ¬a ¬b c = ? -- supf1 b ≡ sp1 , u o≤ sp1, x o≤ u o≤ supf1 b -- u ≡ x → xsup x → ⊥ 
-                                                                     --    u > x → supf1 u ≡ sp1 → supf1 b o≤ supf1 u
-                          -- px o< u o≤ sp1 , spuf1 u o≤  spuf1 sp1
+                         fc0 : FClosure A f (supf0 u) (supf1 b)
+                         fc0 = fc
+                         fc1 : FClosure A f (supf1 u) (supf1 b)
+                         fc1 = ?
+                         --    u > x → supf1 u ≡ sp1 → supf1 b o≤ supf1 u
+                         -- px o< u o≤ sp1 , spuf1 u o≤  spuf1 sp1
                          fcy<sup1 : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u) ∨ (z << supf1 u)
                          fcy<sup1 = ? 
                          order1 : {s z1 : Ordinal} → supf1 s o< supf1 u → FClosure A f (supf1 s) z1 
                              → (z1 ≡ supf1 u) ∨ (z1 << supf1 u)
                          order1 = ?
+                     ... | case2 lt = chain-mono f mf ay supf1 b≤sb  (UnionCF0⊆1 b≤px zc12 ) where
+                         b≤sb :  b o≤ supf1 b -- ≡ supf0 b
+                         b≤sb = ?
+                         lt1 : supf0 u o<  supf0 b
+                         lt1 = lt
+                         zc12 :  odef (UnionCF A f mf ay supf0 b) (supf1 b)
+                         zc12 = subst (λ k → odef (UnionCF A f mf ay supf0 b) k) &iso ( ZChain.csupf-fc zc b≤px lt fc  )
                  ... | case1 refl = ⟪ supf∈A o≤-refl  , ch-is-sup (supf1 x) o≤-refl 
                           record { fcy<sup = fcy<sup ; order = order ; supu=u = zc11 }  (init zc10 zc11 ) ⟫ where
+                     zc12 : supf1 x ≡ sp1
+                     zc12 = ?
                      zc11 : supf1 (supf1 x) ≡ supf1 x
                      zc11 = ?
                      zc10 : odef A (supf1 (supf1 x))