# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1657838690 -32400
# Node ID 92275389e6234d288917c65ae49784807140727e
# Parent  b1d468186e68bd8185f2c98ebf166f0441945749
fix is-max

diff -r b1d468186e68 -r 92275389e623 src/OrdUtil.agda
--- a/src/OrdUtil.agda	Fri Jul 15 05:52:23 2022 +0900
+++ b/src/OrdUtil.agda	Fri Jul 15 07:44:50 2022 +0900
@@ -40,6 +40,13 @@
 osuc-< {x} {y} y<ox x<y | case1 refl = o<¬≡ refl x<y
 osuc-< {x} {y} y<ox x<y | case2 y<x = o<> x<y y<x
 
+open _∧_
+
+¬p<x<op : { p b : Ordinal } → ¬ ( (p o< b ) ∧ (b o< osuc p ) )
+¬p<x<op {p} {b} P with osuc-≡< (proj2 P)
+... | case1 eq = o<¬≡ (sym eq) (proj1 P) 
+... | case2 lt = o<> lt (proj1 P) 
+
 osucc :  {ox oy : Ordinal } → oy o< ox  → osuc oy o< osuc ox  
 osucc {ox} {oy} oy<ox with trio< (osuc oy) ox
 osucc {ox} {oy} oy<ox | tri< a ¬b ¬c = ordtrans a <-osuc
diff -r b1d468186e68 -r 92275389e623 src/zorn.agda
--- a/src/zorn.agda	Fri Jul 15 05:52:23 2022 +0900
+++ b/src/zorn.agda	Fri Jul 15 07:44:50 2022 +0900
@@ -42,12 +42,10 @@
 
 import ODC
 
-
 open _∧_
 open _∨_
 open Bool
 
-
 open HOD
 
 --
@@ -290,7 +288,7 @@
       initial : {y : Ordinal } → odef chain y → * init ≤ * y
       f-next : {a : Ordinal } → odef chain a → odef chain (f a)
       f-total : IsTotalOrderSet chain
-      is-max :  {a b : Ordinal } → (ca : odef chain a ) →  b o< osuc z  → (ab : odef A b) 
+      is-max :  {a b : Ordinal } → (ca : odef chain a ) →  b o< z  → (ab : odef A b) 
           → HasPrev A chain ab f ∨  IsSup A chain ab  
           → * a < * b  → odef chain b
 
@@ -414,7 +412,7 @@
      fixpoint f mf zc total = z14 where
            chain = ZChain.chain zc
            sp1 = sp0 f mf zc total
-           z10 :  {a b : Ordinal } → (ca : odef chain a ) → b o< osuc (& A) → (ab : odef A b ) 
+           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 )
               → * a < * b  → odef chain b
            z10 = ZChain.is-max zc
@@ -423,7 +421,7 @@
            z12 : odef chain (& (SUP.sup sp1))
            z12 with o≡? (& s) (& (SUP.sup sp1))
            ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc )
-           ... | no ne = z10 {& s} {& (SUP.sup sp1)} ( ZChain.chain∋init zc ) (ordtrans z11 <-osuc ) (SUP.A∋maximal sp1)
+           ... | no ne = z10 {& s} {& (SUP.sup sp1)} ( ZChain.chain∋init zc ) z11 (SUP.A∋maximal sp1)
                 (case2 z19 ) z13 where
                z13 :  * (& s) < * (& (SUP.sup sp1))
                z13 with SUP.x<sup sp1 ( ZChain.chain∋init zc )
@@ -488,7 +486,7 @@
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
                uz01 = chain-total A f mf ay isupf (UChain.uchain (proj2 ca)) (UChain.uchain (proj2 cb)) 
           imax : {a b : Ordinal} → odef (UnionCF A f mf ay isupf o∅) a →
-            b o< osuc o∅ → (ab : odef A b) →
+            b o< o∅ → (ab : odef A b) →
             HasPrev A (UnionCF A f mf ay isupf o∅) ab f ∨ IsSup A (UnionCF A f mf ay isupf o∅) ab →
             * a < * b → odef (UnionCF A f mf ay isupf o∅) b
           imax {a} {b} ua b<ox ab (case1 hasp) a<b = subst (λ k → odef  (UnionCF A f mf ay isupf o∅) k ) (sym (HasPrev.x=fy hasp)) ( inext (HasPrev.ay hasp) )
@@ -544,7 +542,7 @@
 
           -- if previous chain satisfies maximality, we caan reuse it
           --
-          no-extenion : ( {a b : Ordinal} → odef pchain a → b o< osuc x → (ab : odef A b) →
+          no-extenion : ( {a b : Ordinal} → odef pchain a → b o< x → (ab : odef A b) →
                     HasPrev A pchain ab f ∨  IsSup A pchain ab →
                             * a < * b → odef pchain b ) → ZChain A f mf ay x
           no-extenion is-max  = record { initial = pinit ; chain∋init = pcy 
@@ -552,11 +550,11 @@
 
           zcp : {a b : Ordinal} → odef pchain a 
               → pchain ≡ UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op )
-              → b o< x → (ab : odef A b) 
+              → b o< px → (ab : odef A b) 
               → HasPrev A pchain ab f ∨  IsSup A pchain ab 
               → * a < * b → odef pchain b
           zcp {a} {b} za cheq b<x ab P a<b = subst (λ k → odef k b ) (sym cheq) ( 
-                   ZChain.is-max zc (subst (λ k → odef k a) cheq za) (subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x) ab 
+                   ZChain.is-max zc (subst (λ k → odef k a) cheq za) b<x ab 
                        (subst (λ k → HasPrev A k ab f ∨  IsSup A k ab ) cheq P)  a<b )
 
           chain-mono : UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op ) ⊆' pchain
@@ -573,12 +571,12 @@
           zc4 : ZChain A f mf ay x 
           zc4 with ODC.∋-p O A (* x)
           ... | no noax = no-extenion zc1 where -- ¬ A ∋ p, just skip
-                zc1 : {a b : Ordinal} → odef pchain a → b o< osuc x → (ab : odef A b) →
+                zc1 : {a b : Ordinal} → odef pchain a → b o< x → (ab : odef A b) →
                     HasPrev A pchain ab f ∨  IsSup A pchain ab →
                             * a < * b → odef pchain b
-                zc1 {a} {b} za b<ox ab P a<b with osuc-≡< b<ox
+                zc1 {a} {b} za b<ox ab P a<b with osuc-≡< ?
                 ... | case1 eq = ⊥-elim ( noax (subst (λ k → odef A k) (trans eq (sym &iso)) ab ) )
-                ... | case2 lt = zcp za (chain-≡ zc10) lt ab P a<b where
+                ... | case2 lt = zcp za (chain-≡ zc10) ? ab P a<b where
                      zc10 : pchain ⊆' UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op)
                      zc10 {z} ⟪ az , record { u = u ; u<x = case2 u=y ; uchain = uc } ⟫ = 
                                    ⟪ az , record { u = u ; u<x = case2 u=y ; uchain = uc } ⟫ 
@@ -589,11 +587,11 @@
           ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) ax f )   
                -- we have to check adding x preserve is-max ZChain A y f mf x
           ... | case1 pr = no-extenion ? where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
-                zc7 : {a b : Ordinal} → odef pchain a → b o< osuc x → (ab : odef A b) →
+                zc7 : {a b : Ordinal} → odef pchain a → b o< x → (ab : odef A b) →
                     HasPrev A pchain ab f ∨  IsSup A pchain ab →
                             * a < * b → odef pchain b
-                zc7 {a} {b} za b<ox ab P a<b with osuc-≡< b<ox
-                ... | case2 lt = zcp za ? lt ab P a<b
+                zc7 {a} {b} za b<ox ab P a<b with osuc-≡< ?
+                ... | case2 lt = zcp za ? ? ab P a<b
                 ... | case1 b=x = ? 
                 -- subst (λ k → odef chain0 k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc (HasPrev.ay pr))
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) ax )
@@ -601,18 +599,18 @@
                 record {  chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal
                      ; initial = pinit ; chain∋init  = pcy ; is-max = p-ismax } where
                 p-ismax :  {a b : Ordinal} → odef pchain  a →
-                    b o< osuc x → (ab : odef A b) →
+                    b o< x → (ab : odef A b) →
                     ( HasPrev A pchain ab f ∨ IsSup A pchain ab ) →
                         * a < * b → odef pchain b
                 p-ismax {a} {b} ua b<ox ab (case1 hasp) a<b = ?
                 p-ismax {a} {b} ua b<ox ab (case2 sup)  a<b = ?
 
           ... | case2 ¬x=sup =  no-extenion z18 where -- x is not f y' nor sup of former ZChain from y -- no extention
-                z18 :  {a b : Ordinal} → odef pchain a → b o< osuc x → (ab : odef A b) →
+                z18 :  {a b : Ordinal} → odef pchain a → b o< x → (ab : odef A b) →
                             HasPrev A pchain ab f ∨ IsSup A pchain   ab →
                             * a < * b → odef pchain b
-                z18 {a} {b} za b<x ab P a<b with osuc-≡< b<x
-                ... | case2 lt = zcp za ? lt ab P a<b
+                z18 {a} {b} za b<x ab P a<b with osuc-≡< ?
+                ... | case2 lt = zcp za ? ? ab P a<b
                 ... | case1 b=x with P
                 ... | case1 pr = subst (λ k → odef pchain k ) (sym (HasPrev.x=fy pr)) ( pnext (HasPrev.ay pr) )
                 ... | case2 b=sup = ⊥-elim ( ¬x=sup record { 
@@ -652,7 +650,7 @@
           pcy : odef pchain y
           pcy = ⟪ ay , record { u =  o∅ ; u<x = case2 refl ; uchain = ch-init _ (init ay)  }  ⟫
 
-          no-extenion : ( {a b : Ordinal} → odef pchain a → b o< osuc x → (ab : odef A b) →
+          no-extenion : ( {a b : Ordinal} → odef pchain a → b o< x → (ab : odef A b) →
                     HasPrev A pchain ab f ∨  IsSup A pchain ab →
                             * a < * b → odef pchain b ) → ZChain A f mf ay x
           no-extenion is-max  = record { initial = pinit ; chain∋init = pcy 
@@ -702,10 +700,10 @@
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax )
           ... | case1 is-sup = {!!} -- x is a sup of (zc ?) 
           ... | case2 ¬x=sup =  no-extenion z18 where -- x is not f y' nor sup of former ZChain from y -- no extention
-                z18 :  {a b : Ordinal} → odef pchain a → b o< osuc x → (ab : odef A b) →
+                z18 :  {a b : Ordinal} → odef pchain a → b o< x → (ab : odef A b) →
                             HasPrev A pchain ab f ∨ IsSup A pchain   ab →
                             * a < * b → odef pchain b
-                z18 {a} {b} za b<x ab P a<b with osuc-≡< b<x
+                z18 {a} {b} za b<x ab P a<b with osuc-≡< ?
                 ... | case2 lt = zcp za ? lt ab P a<b
                 ... | case1 b=x with P
                 ... | case1 pr = subst (λ k → odef pchain k ) (sym (HasPrev.x=fy pr)) ( pnext (HasPrev.ay pr) )