# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1665098929 -32400
# Node ID 37a09244cebd748b94ae4f867cbcf8b37684e015
# Parent  37ddab37e189bb1238d4f47550fb106265941a07
UChain u<x to u≤x again

diff -r 37ddab37e189 -r 37a09244cebd src/zorn.agda
--- a/src/zorn.agda	Thu Oct 06 18:59:44 2022 +0900
+++ b/src/zorn.agda	Fri Oct 07 08:28:49 2022 +0900
@@ -262,7 +262,7 @@
 data UChain  ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y )
        (supf : Ordinal → Ordinal) (x : Ordinal) : (z : Ordinal) → Set n where 
     ch-init : {z : Ordinal } (fc : FClosure A f y z) → UChain A f mf ay supf x z
-    ch-is-sup  : (u : Ordinal) {z : Ordinal }  (u<x : supf u o< supf x) ( is-sup : ChainP A f mf ay supf u ) 
+    ch-is-sup  : (u : Ordinal) {z : Ordinal }  (u≤x : supf u o≤ supf x) ( is-sup : ChainP A f mf ay supf u ) 
         ( fc : FClosure A f (supf u) z ) → UChain A f mf ay supf x z
 
 --
@@ -576,7 +576,7 @@
      chain-mono f mf ay supf {a} {b} {c} a≤b ⟪ ua , ch-init fc  ⟫ = 
             ⟪ ua , ch-init fc  ⟫ 
      chain-mono f mf ay supf {a} {b} {c} a≤b ⟪ uaa ,  ch-is-sup ua ua<x is-sup fc  ⟫ = 
-            ⟪ uaa , ch-is-sup ua (ordtrans<-≤ ua<x a≤b ) is-sup fc  ⟫ 
+            ⟪ uaa , ch-is-sup ua (OrdTrans ua<x a≤b ) is-sup fc  ⟫ 
 
      sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y)  
          (zc : ZChain A f mf ay x ) → SUP A (ZChain.chain zc)
@@ -619,7 +619,7 @@
                 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 ⟫ = ⟪ as , ch-is-sup u zc08 is-sup fc ⟫ where
+                ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ as , ch-is-sup u (o<→≤ zc08) is-sup fc ⟫ where
                     zc07 : FClosure A f (supf u) (supf s)   -- supf u ≤ supf s  → supf u o≤ supf s
                     zc07 = fc
                     zc06 : supf u ≡ u
@@ -654,16 +654,18 @@
            is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P
            is-max {a} {b} ua b<x ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua b<x ab has-prev a<b 
            is-max {a} {b} ua b<x ab P a<b | case2 is-sup 
-             = ⟪ ab , ch-is-sup b sb<sx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫   where
+             = ⟪ ab , ch-is-sup b sb≤sx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫   where
               b<A : b o< & A
               b<A = z09 ab
+              sb≤sx : supf b o≤ supf x
+              sb≤sx = ZChain.supf-mono zc (o<→≤ b<x ) 
               m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) b f
               m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = 
-                    chain-mono1 ?  (HasPrev.ay  nhp) 
+                    chain-mono1 sb≤sx  (HasPrev.ay  nhp) 
                  ; x=fy = HasPrev.x=fy nhp } )
               m05 : ZChain.supf zc b ≡ b
               m05 =  ZChain.sup=u zc ab (o<→≤ (z09 ab) )
-                      ⟪ record { x<sup = λ {z} uz → IsSup.x<sup (proj2 is-sup) (chain-mono1 ? uz) }  , m04 ⟫
+                      ⟪ record { x<sup = λ {z} uz → IsSup.x<sup (proj2 is-sup) (chain-mono1 sb≤sx uz) }  , m04 ⟫
               m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b
               m08 {z} fcz = ZChain.fcy<sup zc (o<→≤ b<A) fcz
               m09 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b 
@@ -671,22 +673,6 @@
               m09 {s} {z} s<b fcz = order b<A s<b fcz    
               m06 : ChainP A f mf ay supf b 
               m06 = record {  fcy<sup = m08  ; order = m09 ; supu=u = m05 }
-              sb<sx : supf b o< supf x
-              sb<sx with osuc-≡< ( ZChain.supf-mono zc (o<→≤ b<x ) )
-              ... | case2 lt = lt
-              ... | case1 eq = ⊥-elim ( <-irr (case1 (sym m11)) m12 ) where 
-                    ---    supf b ≡ supf x     * ( supf x ) ≤ * a < * b , * (supf x) ≡ * (supf b) ≡ * b
-                    ---    xchain = UnionCF A f mf ay supf x
-                    ---       {y : Ordinal} → odef xchain y → (y ≡ b ) ∨ (y < * b )
-                    ---     supf x ∈ xchian → ok
-                    ---   ¬ supf x ∈ xchian → ⊥ 
-                    m10 : {a : Ordinal} → odef  (UnionCF A f mf ay supf x) a  → * ( supf x ) ≤ * a
-                    m10 {a} ⟪ ua , ch-init fc ⟫ = ?
-                    m10 {a} ⟪ ua , ch-is-sup u u<x is-sup fc ⟫ = ?
-                    m12 : * ( supf x ) < * b
-                    m12 = ?
-                    m11 : * ( supf x ) ≡ * b
-                    m11 = ?
         ... | no lim = record { is-max = is-max }  where
            is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
               b o< x → (ab : odef A b) →
@@ -696,7 +682,9 @@
            is-max {a} {b} ua b<x ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua b<x ab has-prev a<b 
            is-max {a} {b} ua b<x ab P a<b | case2 is-sup with IsSup.x<sup (proj2 is-sup) (init-uchain A f mf ay )
            ... | case1 b=y = ⟪ subst (λ k → odef A k ) b=y ay , ch-init (subst (λ k → FClosure A f y k ) b=y (init ay refl ))  ⟫
-           ... | case2 y<b = ⟪ ab , ch-is-sup b ? m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl))  ⟫ where
+           ... | case2 y<b = ⟪ ab , ch-is-sup b sb≤sx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl))  ⟫ where
+              sb≤sx : supf b o≤ supf x
+              sb≤sx = ZChain.supf-mono zc (o<→≤ b<x ) 
               m09 : b o< & A
               m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
               m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b
@@ -706,11 +694,11 @@
               m08 {s} {z1} s<b fc = order m09 s<b fc
               m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) b f
               m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay =  
-                      chain-mono1 ? (HasPrev.ay  nhp) 
+                      chain-mono1 sb≤sx (HasPrev.ay  nhp) 
                  ; x=fy = HasPrev.x=fy nhp } )
               m05 : ZChain.supf zc b ≡ b
               m05 = ZChain.sup=u zc ab (o<→≤  m09)
-                      ⟪ record { x<sup = λ lt → IsSup.x<sup (proj2 is-sup) (chain-mono1 ? lt )} , m04 ⟫    -- ZChain on x
+                      ⟪ record { x<sup = λ lt → IsSup.x<sup (proj2 is-sup) (chain-mono1 sb≤sx lt )} , m04 ⟫    -- ZChain on x
               m06 : ChainP A f mf ay supf b 
               m06 = record { fcy<sup = m07 ;  order = m08 ; supu=u = m05 }
 
@@ -1003,11 +991,11 @@
                       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
+                      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₁) ⟫ 
+                          ... | 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 ? record {fcy<sup = zc13 ; order = zc17
@@ -1026,7 +1014,7 @@
                           ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) ?  ⟫ )
                       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
+                      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₁)  ⟫ 
@@ -1040,7 +1028,7 @@
                               zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) (sym (sf1=sf0 ?)) ( ChainP.order is-sup 
                                  (subst₂ (λ j k → j o< k ) (sf1=sf0 s≤px) (sf1=sf0 ?) ss<spx) (fcup fc s≤px) ) where
                                     s≤px : s o≤ px
-                                    s≤px = ? -- ordtrans ( supf-inject0 supf-mono1 ss<spx ) (o<→≤ u<x)
+                                    s≤px = ? -- ordtrans ( supf-inject0 supf-mono1 ss<spx ) (o<→≤ u≤x)
                               zc14 : FClosure A f (supf1 u) (supf0 u)
                               zc14 = init (subst (λ k → odef A k ) (sym (sf1=sf0 ?)) asp) (sf1=sf0 ?)
                               zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 u) ∨ ( z << supf1 u )
@@ -1199,7 +1187,7 @@
                         zc13 = o≤-refl0 ( trans (Oprev.oprev=x op) (sym eq ) ) 
                         x<sup : {w : Ordinal} → odef (UnionCF A f mf ay supf0 px) w → (w ≡ x) ∨ (w << x)
                         x<sup {w} ⟪ az , ch-init {w} fc ⟫ = subst (λ k → (w ≡ k) ∨ (w << k)) s1u=x ?
-                        x<sup {w} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ with osuc-≡< ( supf-mono (ordtrans (o<→≤ u<x) ? ))
+                        x<sup {w} ⟪ az , ch-is-sup u u≤x is-sup fc ⟫ with osuc-≡< ( supf-mono (ordtrans (o<→≤ u≤x) ? ))
                         ... | case1 eq1 = ⊥-elim ( o<¬≡ zc14 ? ) where
                                  zc14 : u ≡ osuc px
                                  zc14 = begin
@@ -1347,15 +1335,15 @@
                           zc12 (init asu su=z ) = ⟪ subst (λ k → odef A k) su=z asu , ch-is-sup u ? ? (init ? ? ) ⟫ 
                      zc11 :  {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z
                      zc11 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
-                     zc11 {z} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ = zc13 fc where
+                     zc11 {z} ⟪ az , ch-is-sup u u≤x is-sup fc ⟫ = zc13 fc where
                           zc13 : {z : Ordinal} →  FClosure A f (supf1 u) z → odef pchain z
                           zc13 (fsuc x fc) with zc13 fc
                           ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫ 
-                          ... | ⟪ ua1 , ch-is-sup u u<x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u<x is-sup (fsuc _ fc₁) ⟫ 
+                          ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫ 
                           zc13 (init asu su=z ) with trio< u x
                           ... | tri< a ¬b ¬c = ⟪ ? , ch-is-sup u ? ? (init ? ? ) ⟫ 
                           ... | tri≈ ¬a b ¬c = ?
-                          ... | tri> ¬a ¬b c = ? -- ⊥-elim ( o≤> u<x c )
+                          ... | tri> ¬a ¬b c = ? -- ⊥-elim ( o≤> u≤x c )
                  sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z)
                  sup {z} z≤x with trio< z x
                  ... | tri< a ¬b ¬c = SUP⊆ ? (ZChain.sup (pzc (osuc z) {!!}) {!!} )