# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1662608662 -32400
# Node ID 105f8d6c51fb193a5f11a11474f1545f9b0aa6fd
# Parent  f72b35ab0ef978d082308c3660442bffed1d14f0
no-extension on immidate ordinal passed

diff -r f72b35ab0ef9 -r 105f8d6c51fb src/ODC.agda
--- a/src/ODC.agda	Thu Sep 08 09:16:51 2022 +0900
+++ b/src/ODC.agda	Thu Sep 08 12:44:22 2022 +0900
@@ -88,6 +88,13 @@
 ... | yes p = p
 ... | no ¬p = ⊥-elim ( notnot ¬p )
 
+or-exclude : {A B : Set n} → A ∨ B → A ∨ ( (¬ A)  ∧  B )
+or-exclude {A} {B} ab with p∨¬p A
+or-exclude {A} {B} (case1 a) | case1 a0 = case1 a
+or-exclude {A} {B} (case1 a) | case2 ¬a = ⊥-elim ( ¬a a )
+or-exclude {A} {B} (case2 b) | case1 a = case1 a
+or-exclude {A} {B} (case2 b) | case2 ¬a = case2 ⟪ ¬a , b ⟫
+
 open _⊆_
 
 power→⊆ :  ( A t : HOD) → Power A ∋ t → t ⊆ A
diff -r f72b35ab0ef9 -r 105f8d6c51fb src/zorn.agda
--- a/src/zorn.agda	Thu Sep 08 09:16:51 2022 +0900
+++ b/src/zorn.agda	Thu Sep 08 12:44:22 2022 +0900
@@ -295,7 +295,8 @@
 
       supf-max : {x : Ordinal } → z o≤ x  → supf z ≡ supf x
       sup : {x : Ordinal } → x o≤ z  → SUP A (UnionCF A f mf ay supf x)
-      sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z  → IsSup A (UnionCF A f mf ay supf b) ab → supf b ≡ b 
+      sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z  
+           → 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
       csupf : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf (supf b)) (supf b) 
@@ -574,14 +575,18 @@
               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
-           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 
+           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 (o<→≤ 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 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<→≤ (z09 ab) )
-                      record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono1 (o<→≤ b<x) uz )  }  
+                      ⟪ record { x<sup = λ {z} uz → IsSup.x<sup (proj2 is-sup) (chain-mono1 (o<→≤ b<x) uz )  }  , m04 ⟫
               m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b
               m08 {z} fcz = ZChain.fcy<sup zc b<A fcz
               m09 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b 
@@ -594,8 +599,9 @@
               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
-           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 )
+           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 )
            ... | 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 = chain-mono1 (osucc b<x) 
              ⟪ ab , ch-is-sup b (ordtrans o≤-refl <-osuc )  m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl))  ⟫ where
@@ -606,9 +612,12 @@
               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
+              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 is-sup (chain-mono1 (o<→≤ b<x) lt )}    -- ZChain on x
+                      ⟪ 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 = record { fcy<sup = m07 ;  order = m08 ; supu=u = m05 }
 
@@ -856,10 +865,10 @@
                      zc33 : supf0 z ≡ & (SUP.sup zc32)
                      zc33 = trans (sym (supfx (o≤-refl0 (sym zc30)))) ( ZChain.supf-is-sup zc o≤-refl  )
                  sup=u : {b : Ordinal} (ab : odef A b) →
-                    b o≤ x → IsSup A (UnionCF A f mf ay supf0 b) ab → supf0 b ≡ b
+                    b o≤ x → IsSup A (UnionCF A f mf ay supf0 b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf0 b) b f ) → supf0 b ≡ b
                  sup=u {b} ab b≤x is-sup with trio< b px
-                 ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) record { x<sup = λ lt → IsSup.x<sup is-sup lt } 
-                 ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) record { x<sup = λ lt → IsSup.x<sup is-sup lt } 
+                 ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) ⟪ record { x<sup = λ lt → IsSup.x<sup (proj1 is-sup) lt } , proj2 is-sup ⟫ 
+                 ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) ⟪ record { x<sup = λ lt → IsSup.x<sup (proj1 is-sup) lt } , proj2 is-sup ⟫ 
                  ... | tri> ¬a ¬b px<b = zc31 P where
                      zc30 : x ≡ b
                      zc30 with osuc-≡< b≤x
@@ -868,11 +877,12 @@
                      zcsup : xSUP (UnionCF A f mf ay supf0 px) x 
                      zcsup with zc30
                      ... | refl = record { ax = ab ; is-sup = record { x<sup = λ {w} lt → 
-                        IsSup.x<sup is-sup (subst (λ k → odef k w) pchain0=1 lt)  } }
-                     zc31 : ( (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨  HasPrev A pchain x f) → supf0 b ≡ b
-                     zc31 (case1 ¬sp=x) = ⊥-elim (¬sp=x zcsup ) 
-                     zc31 (case2 hasPrev ) = ?
-                     --  f a ≡ x ,   a ≡ x ∨ ( a < x ) -- supf0 (f a) ≡ f a/j
+                        IsSup.x<sup (proj1 is-sup) (subst (λ k → odef k w) pchain0=1 lt)  } }
+                     zc31 : ( (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨  HasPrev A (UnionCF A f mf ay supf0 px) x f) → supf0 b ≡ b
+                     zc31 (case1 ¬sp=x) with zc30
+                     ... | refl = ⊥-elim (¬sp=x zcsup )
+                     zc31 (case2 hasPrev ) with zc30
+                     ... | refl = ⊥-elim ( proj2 is-sup (subst (λ k → HasPrev A k x f) pchain0=1 hasPrev ) ) 
 
                  zc04 : {b : Ordinal} → b o≤ x → (b o≤ px ) ∨ (b ≡ x )
                  zc04 {b} b≤x with trio< b px 
@@ -891,10 +901,10 @@
 
           zc4 : ZChain A f mf ay x 
           zc4 with ODC.∋-p O A (* x)
-          ... | no noax = no-extension {!!} -- ¬ A ∋ p, just skip
+          ... | no noax = no-extension (case1 ( λ s → noax (subst (λ k → odef A k ) (sym &iso) (xSUP.ax s) ))) -- ¬ A ∋ p, just skip
           ... | 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
+          ... | case1 pr = no-extension (case2 pr) -- 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 )
           ... | case1 is-sup = -- x is a sup of zc 
                 record {  supf = ? ; chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} ; csupf = {!!} ; sup=u = {!!} ; supf-mono = {!!}
@@ -922,7 +932,11 @@
                   ... | tri≈ ¬a b ¬c = {!!}
                   ... | tri> ¬a ¬b c = {!!}
 
-          ... | case2 ¬x=sup =  no-extension {!!} -- px is not f y' nor sup of former ZChain from y -- no extention
+          ... | case2 ¬x=sup =  no-extension (case1 nsup) where -- px is not f y' nor sup of former ZChain from y -- no extention
+             nsup : ¬ xSUP (UnionCF A f mf ay supf0 px) x 
+             nsup s = ¬x=sup z12 where
+                z12 : IsSup A (UnionCF A f mf ay supf0 px) ax
+                z12 = record { x<sup = λ {z} lt → subst (λ k → (z ≡ k) ∨ (z << k )) (sym &iso) ( IsSup.x<sup ( xSUP.is-sup s ) lt ) }
 
      ... | no lim = zc5 where
 
@@ -997,7 +1011,7 @@
           zc70 pr xsup = ?
 
           no-extension : ¬ ( xSUP (UnionCF A f mf ay supf0 x) x ) → ZChain A f mf ay x
-          no-extension ¬sp=x  = record { initial = pinit ; chain∋init = pcy  ; supf = supf1  ; sup=u = sup=u
+          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 = csupf ; chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal } where
                  supfu : {u : Ordinal } → ( a : u o< x ) → (z : Ordinal) → Ordinal
@@ -1034,7 +1048,7 @@
                      zc8 = ZChain.supf-is-sup (pzc z a) {!!}
                  ... | tri≈ ¬a b ¬c = {!!}
                  ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z z≤x )) 
-                 sup=u : {b : Ordinal} (ab : odef A b) → b o≤ x → IsSup A (UnionCF A f mf ay supf1 b) ab → supf1 b ≡ b
+                 sup=u : {b : Ordinal} (ab : odef A b) → b o≤ x → IsSup A (UnionCF A f mf ay supf1 b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf1 b) b f ) → supf1 b ≡ b
                  sup=u {z} ab z≤x is-sup with trio< z x
                  ... | tri< a ¬b ¬c = ? -- ZChain.sup=u (pzc (osuc b)  (ob<x lim a))  ab {!!} record { x<sup = {!!} }
                  ... | tri≈ ¬a b ¬c = {!!} -- ZChain.sup=u (pzc (osuc ?)  ?)  ab {!!} record { x<sup = {!!} }