# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1668641763 -32400
# Node ID 04f4baee7b68323bfddf528fa7c2e1887e776d8b
# Parent  a15f1cddf4c6822ff8e9ad18cb76c935b9c2e1f2
UChain is now u o< x

diff -r a15f1cddf4c6 -r 04f4baee7b68 src/zorn.agda
--- a/src/zorn.agda	Thu Nov 17 03:33:19 2022 +0900
+++ b/src/zorn.agda	Thu Nov 17 08:36:03 2022 +0900
@@ -280,7 +280,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 : u o< 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
 
 --
@@ -422,7 +422,7 @@
 chain-mono f mf ay supf supf-mono {a} {b} {c} a≤b ⟪ ua , ch-init fc  ⟫ =
         ⟪ ua , ch-init fc  ⟫
 chain-mono f mf ay supf supf-mono {a} {b} {c} a≤b ⟪ uaa ,  ch-is-sup ua ua<x is-sup fc  ⟫ =
-        ⟪ uaa , ch-is-sup ua (ordtrans<-≤ ua<x (supf-mono a≤b ) ) is-sup fc  ⟫
+        ⟪ uaa , ch-is-sup ua (ordtrans<-≤ ua<x a≤b) is-sup fc  ⟫
 
 record ZChain ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
         {y : Ordinal} (ay : odef A y)  ( z : Ordinal ) : Set (Level.suc n) where
@@ -522,35 +522,33 @@
         → ( { 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⊆ 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} supf-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-inject0 supf-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 ) )
+UChain⊆ A f mf {z} {y} ay {supf} {supf1} supf-mono eq<x lex ⟪ az , ch-is-sup u {x} u<x is-sup fc ⟫ = ⟪ az , ch-is-sup u u<x cp1 fc1 ⟫  where
           fc1 : FClosure A f (supf1 u) x
-          fc1 = subst (λ k → FClosure A f k x ) (eq<x u<x0) fc
+          fc1 = subst (λ k → FClosure A f k x ) (eq<x u<x) fc
+          supf1-mono : {x y : Ordinal } →  x o≤  y  → supf1 x o≤ supf1 y 
+          supf1-mono = ?
           uc01 : {s : Ordinal } →  supf1 s o< supf1 u → s o< z
           uc01 {s} s<u with trio< s z
           ... | tri< a ¬b ¬c = a
           ... | tri≈ ¬a b ¬c = ⊥-elim ( o≤> uc02  s<u ) where -- (supf-mono (o<→≤ u<x0))
                uc02 :  supf1 u o≤ supf1 s
                uc02 = begin
-                 supf1 u  <⟨ u<x1 ⟩
+                 supf1 u  ≤⟨ supf1-mono (o<→≤ u<x) ⟩
                  supf1 z  ≡⟨ cong supf1 (sym b) ⟩
                  supf1 s ∎  where open o≤-Reasoning O
           ... | tri> ¬a ¬b c = ⊥-elim ( o≤> uc03 s<u ) where
                uc03 :  supf1 u o≤ supf1 s
                uc03 = begin
-                 supf1 u  ≡⟨ sym (eq<x u<x0) ⟩
-                 supf u  <⟨ u<x ⟩
+                 supf1 u  ≡⟨ sym (eq<x u<x) ⟩
+                 supf u  ≤⟨ supf-mono (o<→≤ u<x) ⟩
                  supf z  ≤⟨ lex (o<→≤ c) ⟩
                  supf1 s ∎  where open o≤-Reasoning O
           cp1 : ChainP A f mf ay supf1 u
-          cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (eq<x u<x0) (ChainP.fcy<sup is-sup fc )  
-               ; order =  λ {s} {z} s<u fc  → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (eq<x u<x0) 
-                  (ChainP.order is-sup (subst₂ (λ j k → j o< k ) (sym (eq<x (uc01 s<u) )) (sym (eq<x u<x0)) s<u)  
+          cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (eq<x u<x) (ChainP.fcy<sup is-sup fc )  
+               ; order =  λ {s} {z} s<u fc  → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (eq<x u<x) 
+                  (ChainP.order is-sup (subst₂ (λ j k → j o< k ) (sym (eq<x (uc01 s<u) )) (sym (eq<x u<x)) s<u)  
                     (subst (λ k → FClosure A f k z ) (sym (eq<x (uc01 s<u) )) fc ))
-               ; supu=u = trans (sym (eq<x u<x0)) (ChainP.supu=u is-sup)  }
+               ; supu=u = trans (sym (eq<x u<x)) (ChainP.supu=u is-sup)  }
 
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
         {y : Ordinal} (ay : odef A y)  (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
@@ -702,7 +700,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 (ZChain.supf-inject zc 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
@@ -735,7 +733,7 @@
                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 ab has-prev a<b
                is-max {a} {b} ua b<x ab P a<b | case2 is-sup with osuc-≡< (ZChain.supf-mono zc (o<→≤ b<x))
-               ... | case2 sb<sx = ⟪ ab , ch-is-sup b sb<sx  m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫   where
+               ... | case2 sb<sx = ⟪ ab , ch-is-sup b b<x  m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫   where
                   b<A : b o< & A
                   b<A = z09 ab
                   m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) f b
@@ -772,7 +770,7 @@
                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 with osuc-≡< (ZChain.supf-mono zc (o<→≤ b<x))
-               ... | case2 sb<sx = ⟪ ab , ch-is-sup b sb<sx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl))  ⟫ where
+               ... | case2 sb<sx = ⟪ ab , ch-is-sup b b<x m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl))  ⟫ where
                   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
@@ -1032,16 +1030,21 @@
                  fcpu {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sym (sf1=sf0 u≤px)) fc
 
                  fcs<sup : {a b w : Ordinal } → a o< b → b o≤ x → FClosure A f (supf1 a) w → odef (UnionCF A f mf ay supf1 b) w
-                 fcs<sup with trio< a px
-                 ... | tri< a ¬b ¬c = ? -- chain-mono ZChain.fcs<sup a
-                 ... | tri≈ ¬a b ¬c = ? -- a ≡ px , b ≡ x, sp o≤ x → supf px o≤ supf x 
+                 fcs<sup {a} {b} {w} a<b b≤x fc with trio< a px
+                 ... | tri< a<px ¬b ¬c = ? -- chain-mono ZChain.fcs<sup a
+                 ... | tri≈ ¬a a=px ¬c = ⟪ A∋fc _ f mf fc , ch-is-sup px px<b ? ? ⟫ where -- a ≡ px , b ≡ x, sp o≤ x → supf px o≤ supf x 
+                      px<b : px o< b
+                      px<b = subst₂ (λ j k → j o< k) a=px refl a<b
+                      b=x : b ≡ x
+                      b=x with trio< b x
+                      ... | tri< a ¬b ¬c = ?
+                      ... | tri≈ ¬a b ¬c = b
+                      ... | tri> ¬a ¬b c = ⊥-elim ( o<> c ? ) -- subst₂ (λ j k → j o≤ k ) ? ? a<b 
                  ... | tri> ¬a ¬b c = ? --  px o< a o< b o≤ x
 
                  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 su<sx is-sup fc ⟫ = zc21 fc where
-                    u<x :  u o< x
-                    u<x =  supf-inject0 supf1-mono su<sx
+                 zc11 {z} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ = zc21 fc where
                     u≤px : u o≤ px
                     u≤px = zc-b<x _ u<x
                     zc21 : {z1 : Ordinal } → FClosure A f (supf1 u) z1 → odef pchainpx z1
@@ -1050,7 +1053,7 @@
                     ... | 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< (supf0 u) (supf0 px) | inspect supf1 u
-                    ... | tri< a ¬b ¬c | _ = case1 ⟪ asp , ch-is-sup u a record {fcy<sup = zc13 ; order = zc17
+                    ... | tri< a ¬b ¬c | _ = case1 ⟪ asp , ch-is-sup u u<px record {fcy<sup = zc13 ; order = zc17
                          ; supu=u = trans (sym (sf1=sf0 (o<→≤ u<px))) (ChainP.supu=u is-sup) } (init asp0 (sym (sf1=sf0 (o<→≤ u<px))) ) ⟫ where
                         u<px :  u o< px
                         u<px =  ZChain.supf-inject zc a
@@ -1141,7 +1144,12 @@
                  ... | 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
+                 zc17 {z} with trio< z px
+                 ... | tri< a ¬b ¬c = ZChain.supf-mono zc (o<→≤ a)
+                 ... | tri≈ ¬a b ¬c = o≤-refl0 (cong supf0 b)
+                 ... | tri> ¬a ¬b px<z = o≤-refl0 zc177 where
+                      zc177 : supf0 z ≡ supf0 px
+                      zc177 = ZChain.supfmax zc px<z  -- px o< z, px o< supf0 px
 
                  supf-mono1 : {z w : Ordinal } → z o≤ w → supf1 z o≤ supf1 w
                  supf-mono1 {z} {w} z≤w with trio< w px
@@ -1150,9 +1158,9 @@
                  ... | tri< a ¬b ¬c = zc17
                  ... | tri≈ ¬a refl ¬c = o≤-refl
                  ... | tri> ¬a ¬b c = o≤-refl
-                 supf-mono1 {z} {w} z≤w | tri> ¬a ¬b c with trio< z px
+                 supf-mono1 {z} {w} z≤w | tri> ¬a ¬b px<w with trio< z px
                  ... | tri< a ¬b ¬c = zc17
-                 ... | tri≈ ¬a b ¬c = o≤-refl0 ?
+                 ... | tri≈ ¬a b ¬c = o≤-refl0 (cong supf0 b)  -- z=px   supf1 z = supf0 z, supf1 w = supf0 px
                  ... | tri> ¬a ¬b c = o≤-refl
 
                  pchain1 : HOD