# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1665319883 -32400
# Node ID 5b6034ad8b9868abf3e15e5fc90adae570a77918
# Parent  49594badc9b42bd47a74e9d8eb0d2ec427caab4e
...

diff -r 49594badc9b4 -r 5b6034ad8b98 src/zorn.agda
--- a/src/zorn.agda	Sun Oct 09 19:30:41 2022 +0900
+++ b/src/zorn.agda	Sun Oct 09 21:51:23 2022 +0900
@@ -839,14 +839,14 @@
 
                  zc02 : { a b : Ordinal } → odef A a ∧ UChain A f mf ay supf0 px a → FClosure A f (supf0 px) b → a <= b
                  zc02 {a} {b} ca fb = zc05 fb where
-                    zc06 : MinSUP.sup (ZChain.minsup zc o≤-refl) ≡ px
-                    zc06 = trans (sym ( ZChain.supf-is-minsup zc o≤-refl )) ?
+                    zc06 : MinSUP.sup (ZChain.minsup zc o≤-refl) ≡ supf0 px
+                    zc06 = trans (sym ( ZChain.supf-is-minsup zc o≤-refl )) refl
                     zc05 : {b : Ordinal } → FClosure A f (supf0 px) b → a <= b
                     zc05 (fsuc b1 fb ) with proj1 ( mf b1 (A∋fc (supf0 px) f mf fb ))
                     ... | case1 eq = subst (λ k → a <= k ) (subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) eq)) (zc05 fb)
                     ... | case2 lt = <-ftrans (zc05 fb) (case2 lt) 
-                    zc05 (init b1 refl) with MinSUP.x<sup (ZChain.minsup zc o≤-refl) ? --
-                       -- (subst (λ k → odef A k ∧ UChain A f mf ay supf0 (supf0 px) k) (sym &iso) ca )
+                    zc05 (init b1 refl) with MinSUP.x<sup (ZChain.minsup zc o≤-refl) 
+                       (subst (λ k → odef A k ∧ UChain A f mf ay supf0 px k) (sym &iso) ca )
                     ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso zc06 eq )
                     ... | case2 lt = case2 (subst₂ (λ j k → j < k ) *iso (cong (*) zc06) lt ) 
 
@@ -867,7 +867,7 @@
                  ... | case2 lt = tri> (<-irr (case2 lt1)) (λ eq → <-irr (case1 eq) lt1) lt1  where
                       lt1 : a0 < b0
                       lt1 = subst₂ (λ j k → j < k ) *iso *iso lt
-                 ptotal (case2 a) (case2 b) = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso (fcn-cmp px f mf a b)
+                 ptotal (case2 a) (case2 b) = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso (fcn-cmp (supf0 px) f mf a b)
 
                  pcha : pchainpx ⊆' A
                  pcha (case1 lt) = proj1 lt
@@ -895,6 +895,12 @@
                  ... | tri≈ ¬a b ¬c = ⊥-elim ( o<¬≡ (sym b) px<z )
                  ... | tri> ¬a ¬b c = refl
 
+                 asupf1 : {z : Ordinal } → odef A (supf1 z)
+                 asupf1 {z} with trio< z px
+                 ... | tri< a ¬b ¬c = ZChain.asupf zc 
+                 ... | tri≈ ¬a b ¬c = ZChain.asupf zc 
+                 ... | tri> ¬a ¬b c = MinSUP.asm sup1
+
                  supf1-mono : {a b : Ordinal } → a o≤ b → supf1 a o≤ supf1 b 
                  supf1-mono {a} {b} a≤b with trio< b px 
                  ... | tri< a ¬b ¬c =  subst₂ (λ j k → j o≤ k ) (sym (sf1=sf0 (o<→≤ (ordtrans≤-< a≤b a)))) refl ( supf-mono a≤b )
@@ -918,6 +924,106 @@
                        zc18 = subst (λ k → k o≤ sp1) zc20( MinSUP.minsup zc21 (MinSUP.asm sup1) zc24 )
                  ... | tri> ¬a ¬b c = o≤-refl
 
+
+                 fcup : {u z : Ordinal } → FClosure A f (supf1 u) z → u o≤ px → FClosure A f (supf0 u) z 
+                 fcup {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sf1=sf0 u≤px) fc
+                 fcpu : {u z : Ordinal } → FClosure A f (supf0 u) z → u o≤ px →  FClosure A f (supf1 u) z 
+                 fcpu {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sym (sf1=sf0 u≤px)) fc
+                 zc11 : {z : Ordinal} → odef (UnionCF A f mf ay supf1 x) z → odef pchainpx z
+                 zc11 {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫ 
+                 zc11 {z} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ = zc21 fc where
+                    zc21 : {z1 : Ordinal } → FClosure A f (supf1 u) z1 → odef pchainpx z1
+                    zc21 {z1} (fsuc z2 fc ) with zc21 fc
+                    ... | case1 ⟪ ua1 , ch-init fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫ 
+                    ... | case1 ⟪ ua1 , ch-is-sup u u<x u1-is-sup fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u<x u1-is-sup (fsuc _ fc₁) ⟫ 
+                    ... | case2 fc = case2 (fsuc _ fc) 
+                    zc21 (init asp refl ) with trio< u px | inspect supf1 u
+                    ... | tri< a ¬b ¬c | _ = case1 ⟪ asp , ch-is-sup u a record {fcy<sup = zc13 ; order = zc17
+                         ; supu=u = trans (sym (sf1=sf0 (o<→≤ a))) (ChainP.supu=u is-sup) } (init asp refl) ⟫ where
+                        zc17 :  {s : Ordinal} {z1 : Ordinal} → supf0 s o< supf0 u →
+                            FClosure A f (supf0 s) z1 → (z1 ≡ supf0 u) ∨ (z1 << supf0 u)
+                        zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) ((sf1=sf0 zc19)) ( ChainP.order is-sup 
+                         (subst₂ (λ j k → j o< k ) (sym (sf1=sf0 zc18)) (sym (sf1=sf0 zc19)) ss<spx) (fcpu fc zc18) ) where
+                            zc19 : u o≤ px
+                            zc19 = o<→≤ a
+                            zc18 : s o≤ px
+                            zc18 = ordtrans (ZChain.supf-inject zc ss<spx) zc19
+                        zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf0 u) ∨ ( z << supf0 u )
+                        zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sf1=sf0 (o<→≤ a)) ( ChainP.fcy<sup is-sup fc )
+                    ... | tri≈ ¬a b ¬c | _ = case2 (init (subst (λ k → odef A k) (cong supf0 b) asp ) (cong supf0 (sym b)) )
+                    ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x  ⟫ )
+                 zc12 : {z : Ordinal} → odef pchainpx z → odef (UnionCF A f mf ay supf1 x) z
+                 zc12 {z} (case1 ⟪ az , ch-init fc ⟫ ) = ⟪ az , ch-init fc ⟫
+                 zc12 {z} (case1 ⟪ az , ch-is-sup u u<x is-sup fc ⟫ ) = zc21 fc where
+                        zc21 : {z1 : Ordinal } → FClosure A f (supf0 u) z1 → odef (UnionCF A f mf ay supf1 x) z1
+                        zc21 {z1} (fsuc z2 fc ) with zc21 fc
+                        ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫ 
+                        ... | ⟪ ua1 , ch-is-sup u u≤x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u≤x u1-is-sup (fsuc _ fc₁) ⟫ 
+                        zc21 (init asp refl ) with trio< u px | inspect supf1 u
+                        ... | tri< a ¬b ¬c | _ = ⟪ asp , ch-is-sup u 
+                             (subst (λ k → u o< k) (Oprev.oprev=x op) (ordtrans u<x <-osuc)) 
+                                record {fcy<sup = zc13 ; order = zc17 ; supu=u = trans (sf1=sf0 (o<→≤ u<x)) (ChainP.supu=u is-sup) } zc14 ⟫  where
+                            zc17 :  {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 u →
+                                  FClosure A f (supf1 s) z1 → (z1 ≡ supf1 u) ∨ (z1 << supf1 u)
+                            zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) (sym (sf1=sf0 (o<→≤ u<x))) ( ChainP.order is-sup 
+                               (subst₂ (λ j k → j o< k ) (sf1=sf0 s≤px) (sf1=sf0 (o<→≤ u<x)) ss<spx) (fcup fc s≤px) ) where
+                                  s≤px : s o≤ px
+                                  s≤px = ordtrans ( supf-inject0 supf1-mono ss<spx ) (o<→≤ u<x)
+                            zc14 : FClosure A f (supf1 u) (supf0 u)
+                            zc14 = init (subst (λ k → odef A k ) (sym (sf1=sf0 (o<→≤ u<x))) asp) (sf1=sf0 (o<→≤ u<x))
+                            zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 u) ∨ ( z << supf1 u )
+                            zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 (o<→≤ u<x))) ( ChainP.fcy<sup is-sup fc )
+                        ... | tri≈ ¬a b ¬c | _ = ⟪ asp , ch-is-sup px (pxo<x op) record { fcy<sup = zc13 
+                              ; order = zc17 ; supu=u = zc18   } (init asupf1 (trans (sf1=sf0 o≤-refl ) (cong supf0 (sym b)))  ) ⟫ where
+                            zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 px) ∨ ( z << supf1 px )
+                            zc13 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (trans (cong supf0 b) (sym (sf1=sf0 o≤-refl))) (ChainP.fcy<sup is-sup fc )
+                            zc18 : supf1 px ≡ px
+                            zc18 = begin
+                                supf1 px ≡⟨ sf1=sf0 o≤-refl ⟩
+                                supf0 px ≡⟨ cong supf0 (sym b) ⟩
+                                supf0 u ≡⟨ ChainP.supu=u is-sup ⟩
+                                u ≡⟨ b ⟩
+                                px ∎ where open ≡-Reasoning
+                            zc17 :  {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 px →
+                                  FClosure A f (supf1 s) z1 → (z1 ≡ supf1 px) ∨ (z1 << supf1 px)
+                            zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) (trans (cong supf0 b) (sym (sf1=sf0 o≤-refl)))
+                              ( ChainP.order is-sup (subst₂ (λ j k → j o< k) (sf1=sf0 s≤px) zc19 ss<spx) (fcup fc s≤px) ) where
+                                zc19 : supf1 px ≡ supf0 u
+                                zc19 = trans (sf1=sf0 o≤-refl) (cong supf0 (sym b))
+                                s≤px : s o≤ px
+                                s≤px = o<→≤ (supf-inject0 supf1-mono ss<spx)
+                        ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , o<→≤ u<x  ⟫ )
+                 zc12 {z} (case2 fc) = zc21 fc where
+                        zc21 : {z1 : Ordinal } → FClosure A f (supf0 px) z1 → odef (UnionCF A f mf ay supf1 x) z1
+                        zc21 {z1} (fsuc z2 fc ) with zc21 fc
+                        ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫ 
+                        ... | ⟪ ua1 , ch-is-sup u u≤x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u≤x u1-is-sup (fsuc _ fc₁) ⟫ 
+                        zc21 (init asp refl ) = ⟪ asp , ch-is-sup (supf0 px) ?
+                                   record {fcy<sup = ? ; order = ? ; supu=u = ? } ? ⟫ where
+                            zc15 : supf1 px ≡ px
+                            zc15 = trans (sf1=sf0 o≤-refl ) ?
+                            zc14 : FClosure A f (supf1 px) px
+                            zc14 = init (subst (λ k → odef A k) ? asp) zc15
+                            zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 px ) ∨ ( z << supf1 px )
+                            zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 o≤-refl)) ( ZChain.fcy<sup zc o≤-refl fc )
+                            zc17 :  {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 px →
+                                  FClosure A f (supf1 s) z1 → (z1 ≡ supf1 px) ∨ (z1 << supf1 px)
+                            zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k )) mins-is-spx 
+                                   (MinSUP.x<sup mins (csupf17 (fcup fc (o<→≤ s<px) )) ) where
+                                mins : MinSUP A (UnionCF A f mf ay supf0 px)
+                                mins = ZChain.minsup zc o≤-refl
+                                mins-is-spx : MinSUP.sup mins ≡ supf1 px 
+                                mins-is-spx = trans (sym ( ZChain.supf-is-minsup zc o≤-refl ) ) (sym (sf1=sf0 o≤-refl ))
+                                s<px : s o< px
+                                s<px = supf-inject0 supf1-mono ss<spx
+                                sf<px : supf0 s o< px
+                                sf<px = subst₂ (λ j k → j o< k ) (sf1=sf0 (o<→≤ s<px)) (trans (sf1=sf0 o≤-refl) ?) ss<spx
+                                -- (sf1=sf0 ?) (trans ? sfpx=px ) ss<spx
+                                csupf17 : {z1 : Ordinal } → FClosure A f (supf0 s) z1 → odef (UnionCF A f mf ay supf0 px) z1
+                                csupf17 (init as refl ) = ZChain.csupf zc sf<px 
+                                csupf17 (fsuc x fc) = ZChain.f-next zc (csupf17 fc)
+
+
                  record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where
                      field
                          tsup : MinSUP A (UnionCF A f mf ay supf0 z)