# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1658648435 -32400
# Node ID a2947dfff80dbc9f86142f26fae7dcfb01b84470
# Parent  359f1577f947f0fee165d45eb464c3110bb8a75c
is-max on first transfinite induction is not good

diff -r 359f1577f947 -r a2947dfff80d src/zorn.agda
--- a/src/zorn.agda	Sun Jul 24 15:25:08 2022 +0900
+++ b/src/zorn.agda	Sun Jul 24 16:40:35 2022 +0900
@@ -654,7 +654,7 @@
           --
           no-extension : ZChain A f mf ay x
           no-extension = record { supf = supf0
-               ; initial = pinit ; chain∋init = pcy  ; csupf = csupf ; sup=f = ? ; order = ? ; fcy<sup = ?
+               ; initial = pinit ; chain∋init = pcy  ; csupf = csupf ; sup=u = ? ; order = ? ; fcy<sup = ?
               ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal } 
 
           zc4 : ZChain A f mf ay x 
@@ -665,7 +665,7 @@
           ... | 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 ) apx )
           ... | case1 is-sup = -- x is a sup of zc 
-                record {  supf = psupf1 ; chain⊆A = ? ; f-next = ? ; f-total = ? ; csupf = ? ; sup=f = ? ; order = ? ; fcy<sup = ?
+                record {  supf = psupf1 ; chain⊆A = ? ; f-next = ? ; f-total = ? ; csupf = ? ; sup=u = ? ; order = ? ; fcy<sup = ?
                      ; initial = ? ; chain∋init  = ? }  where
              psupf1 : Ordinal → Ordinal
              psupf1 z with trio< z x 
@@ -673,6 +673,7 @@
              ... | tri≈ ¬a b ¬c = x
              ... | tri> ¬a ¬b c = x
           ... | case2 ¬x=sup =  no-extension -- px is not f y' nor sup of former ZChain from y -- no extention
+
      ... | no lim = zc5 where
 
           pzc : (z : Ordinal) → z o< x → ZChain A f mf ay z
@@ -763,6 +764,16 @@
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
                uz01 = chain-total A f mf ay psupf ( (proj2 ca)) ( (proj2 cb)) 
 
+          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 → 
+                * 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 )) ⟫ 
+          ... | ⟪ ab0 , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ ab , 
+                     subst (λ k → UChain A f mf ay supf x k )
+                          (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u≤x (ChainP-next A f mf ay _ is-sup) (fsuc _ fc))  ⟫ 
+
           no-extension : ZChain A f mf ay x
           no-extension  = record { initial = pinit ; chain∋init = pcy  ; supf = psupf  ; csupf = csupf ; sup=u = ? ; order = ? ; fcy<sup = ?
               ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal }
@@ -781,6 +792,26 @@
              ... | tri< a ¬b ¬c = ZChain.supf (pzc z a) z
              ... | tri≈ ¬a b ¬c = x
              ... | tri> ¬a ¬b c = x
+             is-max :  {a b : Ordinal } → (ca : odef (UnionCF A f mf ay psupf1 x) a ) →  b o< x  → (ab : odef A b) 
+               → HasPrev A (UnionCF A f mf ay psupf1 x) ab f ∨  IsSup A (UnionCF A f mf ay psupf1 x) ab  
+               → * a < * b  → odef ((UnionCF A f mf ay psupf1 x)) b
+             is-max {a} {b} ua b<x ab (case1 hasp) a<b = is-max-hp psupf1 x ua b<x ab hasp 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 )
+             ... | case1 b=y = ⊥-elim ( <-irr ?
+                       (subst (λ k → * a < * k ) (sym b=y) a<b ) )
+             ... | case2 y<b = m04 where 
+                 m07 : {z : Ordinal} → FClosure A f y z → z << psupf1 b
+                 m07 {z} fc = ?
+                 m08 : {sup1 z1 : Ordinal} → sup1 o< b → FClosure A f (psupf1 sup1) z1 → z1 << psupf1 b
+                 m08 {sup1} {z1} s<b fc = ?
+                 m05 : b ≡ psupf1 b 
+                 m05 = ?
+                 m06 : ChainP A f mf ay psupf1 b b
+                 m06 = record { fcy<sup = m07 ; csupz = subst (λ k →  FClosure A f k b ) m05 (init ab) ; order = m08 ; supfu=u = sym m05 }
+                 m04 : odef (UnionCF A f mf ay psupf1 x) b
+                 m04 = ⟪ ab , ch-is-sup b ? m06 (subst (λ k → FClosure A f k b) m05 (init ab))  ⟫
+
+
           ... | case2 ¬x=sup =  no-extension -- x is not f y' nor sup of former ZChain from y -- no extention
          
      SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f mf ay   (& A)