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

diff -r 56a150965988 -r f1f779930fbf src/zorn.agda
--- a/src/zorn.agda	Sun Sep 04 08:50:53 2022 +0900
+++ b/src/zorn.agda	Sun Sep 04 14:25:01 2022 +0900
@@ -774,6 +774,12 @@
           ... | tri≈ ¬a b ¬c = refl
           ... | tri> ¬a ¬b c = ⊥-elim ( o≤> z≤px c )
 
+          supf1=sp : {z : Ordinal } → x o≤ z  → supf1 z ≡ sp1
+          supf1=sp {z} x≤z with trio< z px
+          ... | tri< a ¬b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → z o< k ) (Oprev.oprev=x op) (ordtrans a <-osuc )))
+          ... | tri≈ ¬a refl ¬c = ⊥-elim ( o≤> x≤z (pxo<x op))
+          ... | tri> ¬a ¬b c = refl
+
           supf∈A : {b : Ordinal} → b o≤ x → odef A (supf1 b)
           supf∈A {b} b≤z = ?
 
@@ -963,58 +969,44 @@
                      ... | refl = record { ax = ab ; is-sup = record { x<sup = λ {w} lt → 
                         IsSup.x<sup is-sup (subst (λ k → odef k w) pchain0=1 lt)  } }
                  csupf :  {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 (supf1 b)) (supf1 b)
-                 csupf {b} b≤x with osuc-≡< b≤x
-                 ... | case2 b<x = csupf1 where
-                     b≤px : b o≤ px
-                     b≤px = zc-b<x _ b<x
-                     csupf0 : odef (UnionCF A f mf ay supf0 (supf1 b)) (supf1 b)
-                     csupf0 = subst (λ k → odef (UnionCF A f mf ay supf0 k) k ) (supf0=1 b≤px) ( ZChain.csupf zc b≤px )
-                     csupf1 : odef (UnionCF A f mf ay supf1 (supf1 b)) (supf1 b)
-                     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  ⟫ 
-                         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 → ⊥ 
-                         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 
+                 csupf {b} b≤x = ⟪ zc01 , ch-is-sup u o≤-refl 
+                          record { fcy<sup = fcy<sup ; order = order ; supu=u = supu=u } fc  ⟫  where
+                     csupf0 : b o≤ px → odef (UnionCF A f mf ay supf0 (supf1 b)) (supf1 b)
+                     csupf0 b≤px = subst (λ k → odef (UnionCF A f mf ay supf0 k) k ) (supf0=1 b≤px) ( ZChain.csupf zc b≤px )
+                     zc04 : (b o≤ px ) ∨ (b ≡ x )
+                     zc04 with trio< b px 
+                     ... | tri< a ¬b ¬c = case1 (o<→≤ a)
+                     ... | tri≈ ¬a b ¬c = case1 (o≤-refl0 b)
+                     ... | tri> ¬a ¬b px<b with osuc-≡< b≤x
+                     ... | case1 eq = case2 eq
+                     ... | case2 b<x = ⊥-elim ( ¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x  ⟫ ) 
+                     zc01 : odef A (supf1 b)
+                     zc01 with zc04
+                     ... | case1 le = proj1 ( csupf0 le )
+                     ... | case2 eq = subst (λ k → odef A k ) (sym (supf1=sp (o≤-refl0 (sym eq)))) (SUP.as sup1)
+                     u = supf1 b
+                     supu=u : supf1 u ≡ u
+                     supu=u with zc04
+                     ... | case2 eq = begin
+                        supf1 u ≡⟨ cong supf1 (supf1=sp ? ) ⟩
+                        supf1 sp1 ≡⟨ supf1=sp ?  ⟩
+                        sp1 ≡⟨ sym (supf1=sp ?)  ⟩
+                        u ∎ where open ≡-Reasoning
+                     ... | case1 le = subst (λ k → k ≡ u ) (supf0=1 zc05 ) ( ZChain.sup=u zc zc01 zc05 ? )  where
+                         zc06 : b o≤ px
+                         zc06 = le
+                         zc05 : supf1 b o≤ px
+                         zc05 = ?
+                     zc02 : odef A (supf1 u)
+                     zc02 = subst (λ k → odef A k ) (sym supu=u) zc01
+                     zc03 : supf1 u ≡ supf1 b
+                     zc03 = ?
+                     fc : FClosure A f (supf1 u) (supf1 b)
+                     fc = init zc02 zc03 
+                     fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u) ∨ (z << supf1 u)
+                     fcy<sup = ? 
+                     order : {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))
-                     zc10 = subst (λ k → odef A k ) (sym zc11) (  supf∈A o≤-refl )
-                     fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 (supf1 x)) ∨ (z << supf1 (supf1 x))
-                     fcy<sup = ? 
-                     order : {s z1 : Ordinal} → supf1 s o< supf1 (supf1 b) → FClosure A f (supf1 s) z1 
-                         → (z1 ≡ supf1 (supf1 b)) ∨ (z1 << supf1 (supf1 b))
                      order = ?
                  sis : {z : Ordinal} (z≤x : z o≤ x) → supf1 z ≡ & (SUP.sup (sup z≤x))
                  sis {z} z≤x  = zc40 where