# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1661237270 -32400
# Node ID d72bcf8552bbcebbbf71ac2f68a5673293d6356f
# Parent  106492766e36cb851e46af80018d9a05aa915b0c
...

diff -r 106492766e36 -r d72bcf8552bb src/zorn.agda
--- a/src/zorn.agda	Tue Aug 23 15:16:06 2022 +0900
+++ b/src/zorn.agda	Tue Aug 23 15:47:50 2022 +0900
@@ -225,8 +225,9 @@
 -- tree structure
 --
 
-record HasPrev (A B : HOD) {x : Ordinal } (xa : odef A x)  ( f : Ordinal → Ordinal )  : Set n where
+record HasPrev (A B : HOD) (x : Ordinal ) ( f : Ordinal → Ordinal )  : Set n where
    field
+      ax : odef A x
       y : Ordinal
       ay : odef B y
       x=fy :  x ≡ f y 
@@ -346,7 +347,7 @@
         {y : Ordinal} (ay : odef A y)  (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
    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) ab f ∨  IsSup A (UnionCF A f mf ay (ZChain.supf zc) z) ab  
+          → 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
 
 record Maximal ( A : HOD )  : Set (Level.suc n) where
@@ -512,7 +513,7 @@
         chain-mono1  {a} {b} {c} a≤b = chain-mono f mf ay (ZChain.supf zc) a≤b
         is-max-hp : (x : Ordinal) {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) ab f → 
+            HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) b f → 
             * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b
         is-max-hp x {a} {b} ua b<x ab has-prev a<b with HasPrev.ay has-prev
         ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫ 
@@ -527,7 +528,7 @@
            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) ab f ∨ IsSup A (UnionCF A f mf ay (ZChain.supf zc) x) ab →
+              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
            is-max {a} {b} ua b<x ab (case1 has-prev) a<b = is-max-hp x {a} {b} ua b<x ab has-prev a<b 
            is-max {a} {b} ua b<x ab (case2 is-sup) a<b 
@@ -548,7 +549,7 @@
         ... | 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 →
               b o< x → (ab : odef A b) →
-              HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) ab f ∨ IsSup A (UnionCF A f mf ay (ZChain.supf zc) x) ab →
+              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
            is-max {a} {b} ua b<x ab (case1 has-prev) a<b = is-max-hp x {a} {b} ua b<x ab has-prev a<b 
            is-max {a} {b} ua b<x ab (case2 is-sup) a<b with IsSup.x<sup is-sup (init-uchain A f mf ay )
@@ -579,7 +580,7 @@
            chain = ZChain.chain zc
            sp1 = sp0 f mf zc total
            z10 :  {a b : Ordinal } → (ca : odef chain a ) → b o< & A → (ab : odef A b ) 
-              →  HasPrev A chain ab f ∨  IsSup A chain {b} ab -- (supO  chain  (ZChain.chain⊆A zc) (ZChain.f-total zc) ≡ b )
+              →  HasPrev A chain b f ∨  IsSup A chain {b} ab -- (supO  chain  (ZChain.chain⊆A zc) (ZChain.f-total zc) ≡ b )
               → * a < * b  → odef chain b
            z10 = ZChain1.is-max (SZ1 f mf as0 zc (& A) )
            z11 : & (SUP.sup sp1) o< & A
@@ -707,13 +708,12 @@
           pchain1 : HOD
           pchain1  = UnionCF A f mf ay supf1 x
 
-
           -- if previous chain satisfies maximality, we caan reuse it
           --
           --  supf0 px is sup of UnionCF px , supf0 x is sup of UnionCF x 
 
-          no-extension : (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨ HasPrev A pchain ? f → ZChain A f mf ay x
-          no-extension ¬sp=x = record { supf = supf0 ;  sup = ? ; supf-mono = {!!}
+          no-extension : (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨ HasPrev A pchain x f → ZChain A f mf ay x
+          no-extension ¬sp=x = record { supf = supf1 ;  sup = ? ; supf-mono = {!!}
                ; initial = ? ; chain∋init = ? ; sup=u = ? ; supf-is-sup = ? ; csupf = {!!}
               ;  chain⊆A = λ lt → proj1 lt ;  f-next = ? ;  f-total = ? }  where
                  pchain0=1 : ?
@@ -752,7 +752,7 @@
           zc4 : ZChain A f mf ay x 
           zc4 with ODC.∋-p O A (* x)
           ... | no noax = no-extension {!!} -- ¬ A ∋ p, just skip
-          ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) ax f )   
+          ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) x f )   
                -- we have to check adding x preserve is-max ZChain A y f mf x
           ... | case1 pr = no-extension {!!} -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) ax )
@@ -790,18 +790,14 @@
           ysp =  & (SUP.sup (ysup f mf ay))
 
           initial-segment : {a b z : Ordinal } → (a<x : a o< x) ( b<x : b o< x)  → a o< b  → z o≤ a 
-             → ZChain.supf (pzc (osuc a) (ob<x lim a<x )) z ≡ ZChain.(umax z)) (ob<x lim b<x )) z
+             → ZChain.supf (pzc (osuc a) (ob<x lim a<x )) z ≡ ZChain.supf (pzc (osuc b) (ob<x lim b<x )) z
           initial-segment = ?
 
-          initial-segment1 : {a b z : Ordinal } → (a<x : a o< x) ( b<x : b o< x)  → a o< b  → 
-             → ZChain.supf (pzc (osuc a) (ob<x lim a<x )) x ≡ ZChain.(umax z)) (ob<x lim b<x )) x
-          initial-segment1 = ?
-
           supf0 : Ordinal → Ordinal
           supf0 z with trio< z x
           ... | tri< a ¬b ¬c = ZChain.supf (pzc (osuc z) (ob<x lim a)) z
-          ... | tri≈ ¬a b ¬c = {!!}
-          ... | tri> ¬a ¬b c = {!!}
+          ... | tri≈ ¬a b ¬c = ysp
+          ... | tri> ¬a ¬b c = ysp
 
           pchain0 : HOD
           pchain0 = UnionCF A f mf ay supf0 x
@@ -818,8 +814,8 @@
           supf1 : Ordinal → Ordinal
           supf1 z with trio< z x
           ... | tri< a ¬b ¬c = ZChain.supf (pzc (osuc z) (ob<x lim a)) z
-          ... | tri≈ ¬a b ¬c = {!!}
-          ... | tri> ¬a ¬b c = {!!}
+          ... | tri≈ ¬a b ¬c = spu
+          ... | tri> ¬a ¬b c = spu
 
           pchain : HOD
           pchain = UnionCF A f mf ay supf1 x
@@ -844,7 +840,7 @@
 
           is-max-hp : (supf : Ordinal → Ordinal) (x : Ordinal) {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 supf x) ab f → 
+                HasPrev A (UnionCF A f mf ay supf x) b f → 
                 * a < * b → odef (UnionCF A f mf ay supf x) b
           is-max-hp supf x {a} {b} ua b<x ab has-prev a<b with HasPrev.ay has-prev
           ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫ 
@@ -852,7 +848,7 @@
                      subst (λ k → UChain A f mf ay supf x k )
                           (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u≤x is-sup (fsuc _ fc))  ⟫ 
 
-          no-extension : ¬ ( xSUP (UnionCF A f mf ay supf1 x) x ) ∨ HasPrev A pchain ? f → ZChain A f mf ay x
+          no-extension : ¬ ( xSUP (UnionCF A f mf ay supf0 x) x ) ∨ HasPrev A pchain x f → ZChain A f mf ay x
           no-extension ¬sp=x  = record { initial = pinit ; chain∋init = pcy  ; supf = supf1  ; sup=u = sup=u
                ; sup = sup ; supf-is-sup = sis ; supf-mono = {!!}
                ; csupf = {!!} ; chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal } where
@@ -901,7 +897,7 @@
           zc5 : ZChain A f mf ay x 
           zc5 with ODC.∋-p O A (* x)
           ... | no noax = no-extension {!!} -- ¬ A ∋ p, just skip
-          ... | yes ax with ODC.p∨¬p O ( HasPrev A pchain ax f )   
+          ... | yes ax with ODC.p∨¬p O ( HasPrev A pchain x f )   
                -- we have to check adding x preserve is-max ZChain A y f mf x
           ... | case1 pr = no-extension {!!} 
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax )