# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1667764928 -32400
# Node ID ec7f3473ff551fd3fea66a731ea30438c509dfd3
# Parent  9a8041a7f3c92254adcd9698bd806d896491e57e
...

diff -r 9a8041a7f3c9 -r ec7f3473ff55 src/zorn.agda
--- a/src/zorn.agda	Sun Nov 06 13:39:45 2022 +0900
+++ b/src/zorn.agda	Mon Nov 07 05:02:08 2022 +0900
@@ -483,14 +483,16 @@
        fsp≤sp : f sp <=  sp
        fsp≤sp = subst (λ k → f k <= sp ) (sym (HasPrev.x=fy hp)) im00
 
-   UChain⊆ : { supf1 : Ordinal → Ordinal }
+UChain⊆ : ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
+        {z y : Ordinal} (ay : odef A y)  { supf supf1 : Ordinal → Ordinal }
+        → (supf-mono : {x y : Ordinal } →  x o≤  y  → supf x o≤ supf y )
         → ( { x : Ordinal } → x o< z → supf x ≡ supf1 x)
         → ( { x : Ordinal } → z o≤ x → supf z o≤ supf1 x)
         → UnionCF A f mf ay supf z ⊆' UnionCF A f mf ay supf1 z
-   UChain⊆ {supf1} eq<x lex ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
-   UChain⊆ {supf1} eq<x lex ⟪ az , ch-is-sup u {x} u<x is-sup fc ⟫ = ⟪ az , ch-is-sup u u<x1 cp1 fc1 ⟫  where
+UChain⊆ A f mf {z} {y} ay {supf} {supf1} supf-mono eq<x lex ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
+UChain⊆ A f mf {z} {y} ay {supf} {supf1} spuf-mono eq<x lex ⟪ az , ch-is-sup u {x} u<x is-sup fc ⟫ = ⟪ az , ch-is-sup u u<x1 cp1 fc1 ⟫  where
           u<x0 : u o< z
-          u<x0 = supf-inject u<x
+          u<x0 = supf-inject0 spuf-mono u<x
           u<x1 : supf1 u o< supf1 z
           u<x1 = subst (λ k → k o< supf1 z ) (eq<x u<x0) (ordtrans<-≤ u<x (lex o≤-refl ) )
           fc1 : FClosure A f (supf1 u) x
@@ -887,8 +889,9 @@
           zc41 with zc43
           zc41 | (case2 sp≤x ) =  record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono ; supf-< = ?
               ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = csupf1    }  where
-                 --  supf0 px is included by the chain of sp1
-                 --  ( UnionCF A f mf ay supf0 px ∪ FClosure (supf0 px) ) ≡ UnionCF supf1 x
+                 --  supf0 px is included in the chain of sp1
+                 --  supf0 px ≡ px ∧ supf0 px o< sp1 → ( UnionCF A f mf ay supf0 px ∪ FClosure (supf0 px) ) ≡ UnionCF supf1 x
+                 --     else                             UnionCF A f mf ay supf0 px  ≡ UnionCF supf1 x
                  --  supf1 x ≡ sp1, which is not included now
 
                  supf1 : Ordinal → Ordinal
@@ -984,9 +987,77 @@
                     ... | tri≈ ¬a b ¬c | _ = case2 (init (subst (λ k → odef A k) b (ZChain.asupf zc) ) (sym (trans (sf1=sf0 u≤px) b )))
                     ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ ZChain.supf-inject zc c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x  ⟫ )
 
-                 zc12 : {z : Ordinal} → supf0 px ≡ px → odef pchainpx z → odef (UnionCF A f mf ay supf1 x) z
-                 zc12 {z} sfpx=px (case1 ⟪ az , ch-init fc ⟫ ) = ⟪ az , ch-init fc ⟫
-                 zc12 {z} sfpx=px (case1 ⟪ az , ch-is-sup u su<sx is-sup fc ⟫ ) = zc21 fc where
+                 zc35 : {z : Ordinal} → ¬ (supf0 px ≡ px) → odef (UnionCF A f mf ay supf1 x) z  → odef (UnionCF A f mf ay supf0 x) z
+                 zc35 {z} ne with trio< (supf0 px) px
+                 ... | tri< sf0px<px ¬b ¬c = zc34 where
+                     zc34 :  odef (UnionCF A f mf ay supf1 x) z  → odef (UnionCF A f mf ay supf0 x) z
+                     zc34 ⟪ ua1 , ch-init fc ⟫ = ⟪ ua1 , ch-init fc ⟫ 
+                     zc34 ⟪ ua1 , ch-is-sup u u<x is-sup fc ⟫ with osuc-≡< ( ZChain.supf-mono zc (o<→≤ (supf-inject0 supf1-mono u<x)) )
+                     ... | case1 eq = cp3 ( subst ( λ k → FClosure A f k z) (trans (trans (sf1=sf0 u<x0) eq) (ZChain.supfmax zc px<x) ) fc) where 
+                          u<x0 : u o≤ px
+                          u<x0 = subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) (supf-inject0 supf1-mono u<x )
+                          cp3 : {z : Ordinal } → FClosure A f (supf0 px) z → odef (UnionCF A f mf ay supf0 x) z
+                          cp3 (init uz refl) = chain-mono f mf ay supf0 (ZChain.supf-mono zc) (o<→≤ px<x) (ZChain.csupf zc sf0px<px)
+                          cp3 (fsuc uz fc) = ZChain.f-next zc (cp3 fc)
+                     ... | case2 u<x1 = ⟪ ua1 , ch-is-sup u u<x1 cp1 fc1 ⟫ where
+                          u<x0 : u o< x
+                          u<x0 = supf-inject0 supf1-mono u<x -- supf0 u o≤  px ≡ supf0 px → supf0 u ≡ supf0 px ∨ u o< px
+                          sf0u=sf1u : supf0 u ≡ supf1 u
+                          sf0u=sf1u = sym (sf1=sf0 (subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x0 ))
+                          cp2 : {s : Ordinal } → supf0 s o< supf0 u → supf0 s ≡ supf1 s
+                          cp2 {s} ss<su = sym ( sf1=sf0 ( begin
+                                 s  <⟨ ZChain.supf-inject zc ss<su ⟩
+                                 u  ≤⟨ subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x0  ⟩
+                                 px ∎ )) where open o≤-Reasoning O
+                          fc1 : FClosure A f (supf0 u) z
+                          fc1 = subst (λ k → FClosure A f k z ) (sym sf0u=sf1u) fc
+                          cp1 : ChainP A f mf ay supf0 u
+                          cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sym sf0u=sf1u) (ChainP.fcy<sup is-sup fc )  
+                               ; order =  λ {s} {z} s<u fc  → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sym sf0u=sf1u)
+                                  (ChainP.order is-sup (subst₂ (λ j k → j o< k ) (cp2 s<u) sf0u=sf1u s<u)  
+                                    (subst (λ k → FClosure A f k z ) (cp2 s<u) fc ))
+                               ; supu=u = trans (sym (sf1=sf0 (subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x0 ))) (ChainP.supu=u is-sup)  }
+                 ... | tri≈ ¬a b ¬c = ⊥-elim (ne b)
+                 ... | tri> ¬a ¬b c = ?  where
+                     zc34 :  odef (UnionCF A f mf ay supf1 x) z  → odef (UnionCF A f mf ay supf0 x) z
+                     zc34 ⟪ ua1 , ch-init fc ⟫ = ⟪ ua1 , ch-init fc ⟫ 
+                     zc34 ⟪ ua1 , ch-is-sup u u<x is-sup fc ⟫ with osuc-≡< ( ZChain.supf-mono zc (o<→≤ (supf-inject0 supf1-mono u<x)) )
+                     ... | case1 eq = ?
+                     ... | case2 u<x1 = ⟪ ua1 , ch-is-sup u u<x1 cp1 fc1 ⟫ where
+                          u<x0 : u o< x
+                          u<x0 = supf-inject0 supf1-mono u<x -- supf0 u o≤  px ≡ supf0 px → supf0 u ≡ supf0 px ∨ u o< px
+                          sf0u=sf1u : supf0 u ≡ supf1 u
+                          sf0u=sf1u = sym (sf1=sf0 (subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x0 ))
+                          cp2 : {s : Ordinal } → supf0 s o< supf0 u → supf0 s ≡ supf1 s
+                          cp2 {s} ss<su = sym ( sf1=sf0 ( begin
+                                 s  <⟨ ZChain.supf-inject zc ss<su ⟩
+                                 u  ≤⟨ subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x0  ⟩
+                                 px ∎ )) where open o≤-Reasoning O
+                          fc1 : FClosure A f (supf0 u) z
+                          fc1 = subst (λ k → FClosure A f k z ) (sym sf0u=sf1u) fc
+                          cp1 : ChainP A f mf ay supf0 u
+                          cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sym sf0u=sf1u) (ChainP.fcy<sup is-sup fc )  
+                               ; order =  λ {s} {z} s<u fc  → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sym sf0u=sf1u)
+                                  (ChainP.order is-sup (subst₂ (λ j k → j o< k ) (cp2 s<u) sf0u=sf1u s<u)  
+                                    (subst (λ k → FClosure A f k z ) (cp2 s<u) fc ))
+                               ; supu=u = trans (sym (sf1=sf0 (subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x0 ))) (ChainP.supu=u is-sup)  }
+
+                 zc33 : {z : Ordinal} → ¬ (supf0 px o< sp1) → odef (UnionCF A f mf ay supf1 x) z  → odef (UnionCF A f mf ay supf0 x) z
+                 zc33 {z} lt = UChain⊆ A f mf ay supf1-mono (λ lt → sym (sf=eq lt)) sf≤0  where
+                     sf≤0 :  { z : Ordinal } → x o≤ z → supf1 x o≤ supf0 z
+                     sf≤0 {z} x≤z with trio< z px
+                     ... | tri< a ¬b ¬c = ⊥-elim ( o<> (osucc a) (subst (λ k → k o≤ z) (sym (Oprev.oprev=x op)) x≤z ) )
+                     ... | tri≈ ¬a b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → k o< x ) (sym b) px<x ))
+                     ... | tri> ¬a ¬b px<z with trio< sp1 (supf0 x) -- = ?   --- sp1 o≤ supf0 x
+                     ... | tri< a ¬b ¬c = subst₂ ( λ j k → j o≤ k) (sym (sf1=sp1 px<x)) 
+                           (trans (ZChain.supfmax zc px<x) (sym (ZChain.supfmax zc px<z))) ( o<→≤ a  )
+                     ... | tri≈ ¬a b ¬c = subst₂ ( λ j k → j o≤ k) (sym (sf1=sp1 px<x)) 
+                           (trans (ZChain.supfmax zc px<x) (sym (ZChain.supfmax zc px<z)))  (o≤-refl0 b)
+                     ... | tri> ¬a ¬b sf0<sp1 = ⊥-elim ( lt ( ordtrans≤-< (ZChain.supf-mono zc (o<→≤ px<x)) sf0<sp1 ))
+
+                 zc12 : {z : Ordinal} → supf0 px ≡ px → supf0 px o< sp1 → odef pchainpx z → odef (UnionCF A f mf ay supf1 x) z
+                 zc12 {z} sfpx=px sfpx<sp (case1 ⟪ az , ch-init fc ⟫ ) = ⟪ az , ch-init fc ⟫
+                 zc12 {z} sfpx=px sfpx<sp (case1 ⟪ az , ch-is-sup u su<sx is-sup fc ⟫ ) = zc21 fc where
                         u<px :  u o< px
                         u<px = ZChain.supf-inject zc su<sx
                         u<x : u o< x
@@ -1033,7 +1104,7 @@
                                 s≤px : s o≤ px
                                 s≤px = o<→≤ (supf-inject0 supf1-mono ss<spx)
                         ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , u≤px  ⟫ )
-                 zc12 {z} sfpx=px (case2 fc) = zc21 fc where
+                 zc12 {z} sfpx=px sfpx<sp (case2 fc) = zc21 fc where
                         --- supf0 px o< sp1
                         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
@@ -1043,8 +1114,8 @@
                                      record {fcy<sup = zc13 ; order = zc17 ; supu=u = zc15 } zc14 ⟫ where
                               zc15 : supf1 px ≡ px
                               zc15 = trans (sf1=sf0 o≤-refl ) (sfpx=px)
-                              zc18 : supf1 px o< supf1 x
-                              zc18 = ?
+                              zc18 : supf1 px o< supf1 x  
+                              zc18 = subst₂ ( λ j k → j o< k ) (sym (sf1=sf0 o≤-refl)) (sym (sf1=sp1 px<x)) sfpx<sp
                               zc14 : FClosure A f (supf1 px) (supf0 px)
                               zc14 = init (subst (λ k → odef A k) (sym (sf1=sf0 o≤-refl)) asp) (sf1=sf0 o≤-refl)
                               zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 px ) ∨ ( z << supf1 px )
@@ -1105,14 +1176,16 @@
                      --  z1 ≡ px , supf0 px ≡  px
                      psz1≤px :  supf1 z1 o≤ px
                      psz1≤px =  subst (λ k → supf1 z1 o< k ) (sym opx=x) sz1<x
+                     sf0px<sp1 : supf0 px o< sp1  -- px o< sp1 o≤ x .. sp1 ≡ x
+                     sf0px<sp1 = ?
                      csupf2 :  odef (UnionCF A f mf ay supf1 x) (supf1 z1)
                      csupf2 with  trio< z1 px | inspect supf1 z1
                      csupf2 | tri< a ¬b ¬c | record { eq = eq1 } with osuc-≡< psz1≤px
-                     ... | case2 lt  = zc12 ? (case1 cs03)  where
+                     ... | case2 lt  = zc12 ? ? (case1 cs03)  where
                            cs03 : odef (UnionCF A f mf ay supf0 px) (supf0 z1)
                            cs03 = ZChain.csupf zc (subst (λ k → k o< px) (sf1=sf0 (o<→≤ a)) lt )
                      ... | case1 sfz=px with osuc-≡< ( supf1-mono (o<→≤ a) )
-                     ... | case1 sfz=sfpx =  zc12 ? (case2 (init (ZChain.asupf zc) cs04 )) where
+                     ... | case1 sfz=sfpx =  zc12 ? ? (case2 (init (ZChain.asupf zc) cs04 )) where
                            supu=u : supf1 (supf1 z1) ≡ supf1 z1
                            supu=u = trans (cong supf1 sfz=px) (sym sfz=sfpx)
                            cs04 : supf0 px ≡ supf0 z1
@@ -1127,7 +1200,7 @@
                            cs05 = subst₂ ( λ j k → j o< k ) sfz=px (sf1=sf0 o≤-refl ) sfz<sfpx
                            cs06 : supf0 px o< osuc px
                            cs06 = subst (λ k → supf0 px o< k ) (sym opx=x) ?
-                     csupf2 | tri≈ ¬a b ¬c | record { eq = eq1 } =  zc12 ? (case2 (init (ZChain.asupf zc) (cong supf0 (sym b))))
+                     csupf2 | tri≈ ¬a b ¬c | record { eq = eq1 } =  zc12 ? ? (case2 (init (ZChain.asupf zc) (cong supf0 (sym b))))
                      csupf2 | tri> ¬a ¬b px<z1 | record { eq = eq1 } = ?
                      -- ⊥-elim ( ¬p<x<op ⟪ px<z1 , subst (λ k → z1 o< k) (sym opx=x) z1<x ⟫ )
 
@@ -1161,6 +1234,17 @@
                  ... | tri≈ ¬a b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → k o< x ) (sym b) px<x ))
                  ... | tri> ¬a ¬b c = o≤-refl0 ( ZChain.supfmax zc px<x )
 
+                 sf=eq0 :  { z : Ordinal } → z o< x → supf1 z ≡ supf0 z
+                 sf=eq0 {z} z<x with trio< z px
+                 ... | tri< a ¬b ¬c = refl
+                 ... | tri≈ ¬a b ¬c = refl 
+                 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → z o< k) (sym (Oprev.oprev=x op))  z<x ⟫ )
+                 sf≤0 :  { z : Ordinal } → x o≤ z → supf1 x o≤ supf0 z
+                 sf≤0 {z} x≤z with trio< z px
+                 ... | tri< a ¬b ¬c = ⊥-elim ( o<> (osucc a) (subst (λ k → k o≤ z) (sym (Oprev.oprev=x op)) x≤z ) )
+                 ... | tri≈ ¬a b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → k o< x ) (sym b) px<x ))
+                 ... | tri> ¬a ¬b c = o≤-refl0 ? -- (sym ( ZChain.supfmax zc px<x ))
+
                  zc17 : {z : Ordinal } → supf0 z o≤ supf0 px
                  zc17 = ? -- px o< z, px o< supf0 px