# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1663050379 -32400
# Node ID 1ca338c3f09c2b69c3cefd2126ca7e07db9dde93
# Parent  35a884f2bfde8eda432e72a0776a21fce3b665ca
...

diff -r 35a884f2bfde -r 1ca338c3f09c src/zorn.agda
--- a/src/zorn.agda	Tue Sep 13 02:49:49 2022 +0900
+++ b/src/zorn.agda	Tue Sep 13 15:26:19 2022 +0900
@@ -447,7 +447,8 @@
            → IsSup A (UnionCF A f mf ay supf b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf b) b f) → supf b ≡ b 
       supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (sup x≤z) )
       supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
-      order : {b s z1 : Ordinal} → b o< z → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
+      csupf : {b : Ordinal } → supf b o< z → odef (UnionCF A f mf ay supf z) (supf b) 
+
 
    chain∋init : odef chain y
    chain∋init = ⟪ ay , ch-init (init ay refl)    ⟫
@@ -487,10 +488,12 @@
 
 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
+   supf = ZChain.supf zc
    field
-      is-max :  {a b : Ordinal } → (ca : odef (UnionCF A f mf ay (ZChain.supf zc) z) a ) →  b o< z  → (ab : odef A b) 
-          → HasPrev A (UnionCF A f mf ay (ZChain.supf zc) z) b f ∨  IsSup A (UnionCF A f mf ay (ZChain.supf zc) z) ab  
-          → * a < * b  → odef ((UnionCF A f mf ay (ZChain.supf zc) z)) b
+      order : {b s z1 : Ordinal} → b o< z → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
+      is-max :  {a b : Ordinal } → (ca : odef (UnionCF A f mf ay supf z) a ) →  b o< z  → (ab : odef A b) 
+          → HasPrev A (UnionCF A f mf ay supf z) b f ∨  IsSup A (UnionCF A f mf ay supf z) ab  
+          → * a < * b  → odef ((UnionCF A f mf ay supf z)) b
 
 initial-segment : ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
         {a b y : Ordinal} (ay : odef A y)  (za : ZChain A f mf ay a ) (zb : ZChain A f mf ay b ) 
@@ -622,7 +625,39 @@
                  subst (λ k → UChain A f mf ay (ZChain.supf zc) x k )
                       (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u≤x is-sup (fsuc _ fc))  ⟫ 
 
-        supf1 = ZChain.supf zc
+        supf = ZChain.supf zc
+
+        csupf-fc : {b s z1 : Ordinal} → b o≤ & A → supf s o< supf b → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1
+        csupf-fc {b} {s} {z1} b≤z ss<sb (init x refl ) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc05  where
+                s<b : s o< b
+                s<b = ZChain.supf-inject zc ss<sb
+                s≤<z : s o≤ & A
+                s≤<z = ordtrans s<b b≤z
+                zc04 : odef (UnionCF A f mf ay supf (supf s))  (supf s)
+                zc04 = ? ZChain.csupf zc ? 
+                zc03 : odef (UnionCF A f mf ay supf (& A))  (supf s)
+                zc03 = ZChain.csupf zc ? 
+                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 (zc09 u<x ) is-sup fc ⟫ where
+                    zc06 : supf u ≡ u
+                    zc06 = ChainP.supu=u is-sup
+                    zc09 : u o< supf s  →  u o< b 
+                    zc09 u<s = ordtrans (ZChain.supf-inject zc (subst (λ k → k o< supf s) (sym zc06) u<s)) s<b
+        csupf-fc {b} {s} {z1} b<z ss≤sb (fsuc x fc) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc04  where
+                zc04 : odef (UnionCF A f mf ay supf b) (f x)
+                zc04 with subst (λ k → odef (UnionCF A f mf ay supf b) k ) &iso (csupf-fc b<z ss≤sb fc  )
+                ... | ⟪ as , ch-init fc ⟫ = ⟪ proj2 (mf _ as) , ch-init (fsuc _ fc) ⟫ 
+                ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf _ as) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫ 
+        order : {b s z1 : Ordinal} → b o< & A → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
+        order {b} {s} {z1} b<z ss<sb fc = zc04 where
+          zc00 : ( * z1  ≡  SUP.sup (ZChain.sup zc (o<→≤ b<z) )) ∨ ( * z1  < SUP.sup ( ZChain.sup zc (o<→≤ b<z) ) )
+          zc00 = SUP.x<sup (ZChain.sup zc (o<→≤  b<z) ) (csupf-fc (o<→≤ b<z) ss<sb fc )
+          zc04 : (z1 ≡ supf b) ∨ (z1 << supf b)
+          zc04 with zc00
+          ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso (sym (ZChain.supf-is-sup zc (o<→≤ b<z))  ) (cong (&) eq) )
+          ... | case2 lt = case2 (subst₂ (λ j k → j < k ) refl (subst₂ (λ j k → j ≡ k ) *iso refl (cong (*) (sym (ZChain.supf-is-sup zc (o<→≤ b<z) ) )))  lt )
 
         zc1 :  (x : Ordinal) →  ((y₁ : Ordinal) → y₁ o< x → ZChain1 A f mf ay zc y₁) → ZChain1 A f mf ay zc x
         zc1 x prev with Oprev-p x
@@ -632,15 +667,15 @@
            zc-b<x {b} lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt 
            is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
               b o< x → (ab : odef A b) →
-              HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) b f ∨ IsSup A (UnionCF A f mf ay (ZChain.supf zc) x) ab →
-              * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b
+              HasPrev A (UnionCF A f mf ay supf x) b f ∨ IsSup A (UnionCF A f mf ay supf x) ab →
+              * a < * b → odef (UnionCF A f mf ay supf x) b
            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 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 (ZChain.supf zc) b) b f
+              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 (o<→≤ b<x) (HasPrev.ay  nhp) 
                  ; x=fy = HasPrev.x=fy nhp } )
               m05 : ZChain.supf zc b ≡ b
@@ -650,14 +685,14 @@
               m08 {z} fcz = ZChain.fcy<sup zc b<A fcz
               m09 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b 
                            → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b
-              m09 {s} {z} s<b fcz = ZChain.order zc b<A s<b fcz    
-              m06 : ChainP A f mf ay (ZChain.supf zc) b 
+              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 }
         ... | no lim = record { is-max = is-max }  where
-           is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
+           is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
               b o< x → (ab : odef A b) →
-              HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) b f ∨ IsSup A (UnionCF A f mf ay (ZChain.supf zc) x) ab →
-              * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b
+              HasPrev A (UnionCF A f mf ay supf x) b f ∨ IsSup A (UnionCF A f mf ay supf x) ab →
+              * a < * b → odef (UnionCF A f mf ay supf x) b
            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 with IsSup.x<sup (proj2 is-sup) (init-uchain A f mf ay )
@@ -670,14 +705,14 @@
               m07 {z} fc = ZChain.fcy<sup zc  m09 fc
               m08 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b 
                        → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b
-              m08 {s} {z1} s<b fc = ZChain.order zc m09 s<b fc
-              m04 : ¬ HasPrev A (UnionCF A f mf ay (ZChain.supf zc) b) b f
+              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 (o<→≤ b<x) (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 (o<→≤ b<x) lt )} , m04 ⟫    -- ZChain on x
-              m06 : ChainP A f mf ay (ZChain.supf zc) b 
+              m06 : ChainP A f mf ay supf b 
               m06 = record { fcy<sup = m07 ;  order = m08 ; supu=u = m05 }
 
      ---
@@ -784,11 +819,9 @@
           zc-b<x : (b : Ordinal ) → b o< x → b o< osuc px
           zc-b<x b lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt 
 
-          pchain : HOD
-          pchain  = UnionCF A f mf ay (ZChain.supf zc) px
-
           supf0 = ZChain.supf zc
-
+          pchain  : HOD
+          pchain   = UnionCF A f mf ay supf0 px
           pchain1 : HOD
           pchain1  = UnionCF A f mf ay supf0 x
 
@@ -824,7 +857,7 @@
           --           supf0 px ≡ supf0 x 
 
           no-extension : ( (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨  HasPrev A pchain x f) → ZChain A f mf ay x
-          no-extension P = record { supf = supf0 ;  asupf = ? ; sup = λ lt → STMP.tsup (sup lt ) ; supf-mono = supf-mono 
+          no-extension P = record { supf = supf0 ;  asupf = ZChain.asupf zc ; sup = λ lt → STMP.tsup (sup lt ) ; supf-mono = supf-mono 
               ; order = ? ; sup=u = sup=u ; supf-is-sup = λ lt → STMP.tsup=sup (sup lt) }  where
                  zc10 :  {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z
                  zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫