# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1650599545 -32400
# Node ID 06a655ca04b8bc70cc582a7d309c07aa533f4f9b
# Parent  6e94ea146fc1537598c5b7523ffd5fa94845fcad
...

diff -r 6e94ea146fc1 -r 06a655ca04b8 src/zorn.agda
--- a/src/zorn.agda	Wed Apr 20 10:44:38 2022 +0900
+++ b/src/zorn.agda	Fri Apr 22 12:52:25 2022 +0900
@@ -143,6 +143,7 @@
 -- OS<-cmp : {x : HOD} → Trichotomous {_} {IsTotalOrderSet x} _OS≈_ _OS<_ 
 -- OS<-cmp A B = {!!}
 
+-- tree structure
 data IChain  (A : HOD) : Ordinal → Set n where
     ifirst : {ox : Ordinal} → odef A ox → IChain A ox
     inext  : {ox oy : Ordinal} → odef A oy → * ox < * oy → IChain A ox → IChain A oy
@@ -168,6 +169,9 @@
       iy : IChain A y
       ic : ic-connect x iy 
 
+--
+-- all tree from x
+--
 IChainSet : (A : HOD) {x : Ordinal} → odef A  x → HOD
 IChainSet A {x} ax = record { od = record { def = λ y → odef A y ∧ IChained A x y }
     ; odmax = & A ; <odmax = λ {y} lt → subst (λ k → k o< & A) &iso (c<→o< (subst (λ k → odef A k) (sym &iso) (proj1 lt))) } 
@@ -196,6 +200,8 @@
       y>x  : * x < * y
 
 -- finite IChain
+--
+--    tree structured
 
 ic→A∋y : (A : HOD) {x y : Ordinal}  (ax : A ∋ * x) → odef (IChainSet A ax) y → A ∋ * y
 ic→A∋y A {x} {y} ax ⟪ ay , _ ⟫ = subst (λ k → odef A k) (sym &iso) ay
@@ -332,9 +338,9 @@
 --
 -- possible three cases in a limit ordinal step
 -- 
--- case 1) < goes > x                       (will contradic in the transfinite induction )
+-- case 1) < goes x o<
 -- case 2) no > x in some chain ( maximal )
--- case 3) countably infinite chain below x (will be prohibited by sup condtion )
+-- case 3) countably infinite chain below x 
 --
 Zorn-lemma-3case : { A : HOD } 
     → o∅ o< & A 
@@ -420,21 +426,24 @@
              y<z  = ic→< {A} PO y (subst (λ k → odef A k) &iso ay) (IChained.iy (proj2 icy))
                (subst (λ k → ic-connect k (IChained.iy (proj2 icy))) &iso (IChained.ic (proj2 icy)))
 
-<-TransFinite : ( A : HOD ) → IsTotalOrderSet A → { P : {x : HOD }  → A ∋ x → Set (Level.suc n) }
-         → ( (x y : HOD) →  (ax : A ∋ x ) → A ∋ y  → x < y → P ax  ) → {x : HOD} → (ax : odef A (& (* (& x  )))) → P ax
-<-TransFinite A TA {P} prev {x} ax = TransFinite ind (& x) ax  where
-      ind :  (x : Ordinal) → ((y : Ordinal) → y o< x → (ay : A ∋ * y) → P ay) → (ax : A ∋ * x) → P ax
-      ind = {!!}
+-- <-TransFinite : ( A : HOD ) → IsTotalOrderSet A 
+--          → ( (x : Ordinal) → ((y : Ordinal) → y o< x → ZChain A y) → ZChain A x ) → (x : Ordinal ) → ZChain A x
+-- <-TransFinite A TA ind x = TransFinite {ZChain A} ind x 
 
-record ZChain ( A : HOD ) (y : Ordinal)   : Set (Level.suc n) where
+--
+-- inductive maxmum tree from x
+-- tree structure
+--
+
+≤-monotonic-f : (A : HOD) → ( Ordinal → Ordinal ) → Set (Level.suc n)
+≤-monotonic-f A f = (x : Ordinal ) → odef A x → ( * x ≤ * (f x) ) ∧  odef A (f x )
+
+record ZChain ( A : HOD ) {x : Ordinal} (ax : A ∋ * x) (z : Ordinal)  : Set (Level.suc n) where
    field
-      zmax : HOD
-      A∋max : A ∋ zmax
-      y<max : y o< & zmax
       chain : HOD
-      chain⊆A : chain ⊆ A  
-      total : IsTotalOrderSet chain 
-      chain-max : (x : HOD) → chain ∋ x → (x ≡ zmax ) ∨ ( x < zmax )
+      chain⊆A : chain ⊆ A
+      f-total : ( f : Ordinal → Ordinal ) → ≤-monotonic-f A f → IsTotalOrderSet chain 
+      is-max :  ( f : Ordinal → Ordinal ) → ≤-monotonic-f A f → {a b : Ordinal } → odef chain a → a o< z → * a < * b  → odef chain b
 
 record SUP ( A B : HOD )  : Set (Level.suc n) where
    field
@@ -447,35 +456,83 @@
     → IsPartialOrderSet A 
     → ( ( B : HOD) → (B⊆A : B ⊆ A) → IsTotalOrderSet B → SUP A B   ) -- SUP condition
     → Maximal A 
-Zorn-lemma {A}  0<A PO supP = zorn04 where
+Zorn-lemma {A}  0<A PO supP = zorn00 where
      z01 : {a b : HOD} → A ∋ a → A ∋ b  → (a ≡ b ) ∨ (a < b ) → b < a → ⊥
      z01 {a} {b} A∋a A∋b (case1 a=b) b<a = IsStrictPartialOrder.irrefl PO {me A∋b} {me A∋a} (sym a=b) b<a
      z01 {a} {b} A∋a A∋b (case2 a<b) b<a = IsStrictPartialOrder.irrefl PO {me A∋b} {me A∋b} refl
           (IsStrictPartialOrder.trans PO {me A∋b} {me A∋a} {me A∋b}  b<a a<b)
-     s = ODC.minimal O A (λ eq → ¬x<0 (subst (_o<_ o∅) (=od∅→≡o∅ eq) 0<A))
-     sa = ODC.x∋minimal O A (λ eq → ¬x<0 (subst (_o<_ o∅) (=od∅→≡o∅ eq) 0<A))
-     MaxTC : HOD
-     MaxTC = {!!}
-     z02 : {x max : Ordinal } → (ax : A ∋ * x ) → InfiniteChain A max ax  → ⊥
-     z02 {x} {max} ax ifc = zc5 ifc where
-          FC : HOD
-          FC = IChainSet A ax
-          zc6 : (ifc : InfiniteChain A max ax)  → ¬ SUP A (InFCSet A ax ifc) 
-          zc6 ifc sup = z01 {!!} (SUP.A∋maximal sup) (SUP.x<sup sup {!!} ) {!!} where
-          zc5 : InfiniteChain A max ax → ⊥
-          zc5 ifc = zc6 ifc ( supP (InFCSet A ax ifc) (InFCSet⊆A A {x} ax ifc) (  TransitiveClosure-is-total  A {x} ax PO ifc ))
-     -- z03 : {x : Ordinal } → (ax : A ∋ * x ) → InfiniteChain A (& A)  ax  → ⊥
-     -- z03 {x}  ax ifc = {!!}
+     s : HOD
+     s = ODC.minimal O A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A )) 
+     sa : A ∋ * ( & s  )
+     sa =  subst (λ k → odef A (& k) ) (sym *iso) ( ODC.x∋minimal O A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A ))  )
+     HasMaximal : HOD
+     HasMaximal = record { od = record { def = λ x → (m : Ordinal) →  odef A m → odef A x ∧ (¬ (* x < * m))} ; odmax = & A ; <odmax = {!!} } where
+         z07 :  {y : Ordinal} → ((m : Ordinal) → odef A y ∧ odef A m ∧ (¬ (* y < * m))) → y o< & A
+         z07 {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 (p (& s)) )))
+     cf : ¬ Maximal A → Ordinal → Ordinal
+     cf  = {!!}
+     cf-is-<-monotonic : (nmx : ¬ Maximal A ) → (x : Ordinal) →  odef A x → ( * x < * (cf nmx x) ) ∧  odef A (cf nmx x )
+     cf-is-<-monotonic = {!!}
+     cf-is-≤-monotonic : (nmx : ¬ Maximal A ) →  ≤-monotonic-f A ( cf nmx )
+     cf-is-≤-monotonic = {!!}
+     zsup : ZChain A sa (& A) → ( f : Ordinal → Ordinal ) → ≤-monotonic-f A f  → Ordinal
+     zsup zc f mf = & ( SUP.sup (supP (ZChain.chain zc) (ZChain.chain⊆A zc) ( ZChain.f-total zc f mf )  ) )
+     A∋zsup : (zc : ZChain A sa (& A)) →  (nmx : ¬ Maximal A )  →  A ∋ * (zsup zc (cf nmx) (cf-is-≤-monotonic nmx))
+     A∋zsup zc nmx = {!!}
+     z03 : (zc : ZChain A sa (& A)) → ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → f (zsup zc f mf ) ≡ zsup zc f mf 
+     z03 = {!!}
+     z04 : (zc : ZChain A sa (& A)) → ¬ Maximal A  → ⊥
+     z04 zc nmx = z01  {* (cf nmx c)} {* c} sa (A∋zsup zc nmx ) (case1 ( cong (*)( z03 zc (cf nmx) (cf-is-≤-monotonic nmx ))))
+           (proj1 (cf-is-<-monotonic nmx c ((subst λ k → odef A k ) &iso (A∋zsup zc nmx )))) where
+          c = zsup zc (cf nmx) (cf-is-≤-monotonic nmx)
      -- ZChain is not compatible with the SUP condition
-     ind : (x : Ordinal) → ((y : Ordinal) → y o< x →  ZChain A y ∨ Maximal A )
-         →  ZChain A x ∨ Maximal A 
-     ind x prev = {!!}
-     zorn03 : (x : Ordinal) → ZChain A x  ∨ Maximal A 
-     zorn03 x = TransFinite ind  x
-     zorn04 : Maximal A 
-     zorn04 with zorn03 (& A)
-     ... | case1 chain = ⊥-elim ( o<> (c<→o< {ZChain.zmax chain} {A} (ZChain.A∋max chain))  (ZChain.y<max chain) )
-     ... | case2 m = m
+     ind : (x : Ordinal) → ((y : Ordinal) → y o< x →  ZChain A sa y ∨ Maximal A )
+         →  ZChain A sa x ∨ Maximal A 
+     ind x prev with Oprev-p x
+     ... | yes op with ODC.∋-p O A (* x)
+     ... | no ¬Ax = zc1 where
+          -- we have previous ordinal and ¬ A ∋ x, use previous Zchain
+          px = Oprev.oprev op
+          zc1 : ZChain A sa x ∨ Maximal A
+          zc1 with prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc) 
+          ... | case2 x = case2 x  -- we have the Maximal
+          ... | case1 zc = case1 {!!}
+     ... | yes ax = zc4 where -- we have previous ordinal and A ∋ x
+          px = Oprev.oprev op
+          zc1 : OSup> A (subst (OD.def (od A)) (sym &iso) (subst (OD.def (od A)) &iso ax)) → ZChain A sa x ∨ Maximal A
+          zc1 os with  prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc) 
+          ... | case2 mx = case2 mx
+          ... | case1 zc = case1 {!!}
+          zc4 : ZChain A sa x ∨ Maximal A
+          zc4 with Zorn-lemma-3case 0<A PO x (subst (λ k → odef A k) &iso ax )
+          ... | case1 y>x = zc1 y>x
+          ... | case2 (case1 mx) = case2 mx
+          ... | case2 (case2 ic) with  prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc) 
+          ... | case2 mx = case2 mx
+          ... | case1 zc = {!!}
+     ind x prev | no ¬ox with trio< (& A) x   --- limit ordinal case
+     ... | t = {!!}
+
+     zorn00 : Maximal A 
+     zorn00 with is-o∅ ( & HasMaximal )
+     ... | no not = record { maximal = ODC.minimal O HasMaximal  (λ eq → not (=od∅→≡o∅ eq)) ; A∋maximal = zorn01 ; ¬maximal<x  = zorn02 } where
+         -- yes we have the maximal
+         zorn03 :  odef HasMaximal ( & ( ODC.minimal O HasMaximal  (λ eq → not (=od∅→≡o∅ eq)) ) )
+         zorn03 =  ODC.x∋minimal  O HasMaximal  (λ eq → not (=od∅→≡o∅ eq))
+         zorn01 :  A ∋ ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq))
+         zorn01 =  proj1 (zorn03 (& s) (subst (λ k → odef A (& k) ) *iso sa) ) 
+         zorn02 : {x : HOD} → A ∋ x → ¬ (ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) < x)
+         zorn02 {x} ax m<x = proj2 (zorn03 (& x) ax) (subst₂ (λ j k → j < k) (sym *iso) (sym *iso) m<x )
+     ... | yes ¬Maximal = ⊥-elim ( z04 zorn03  zorn04 ) where
+         -- if we have no maximal, make ZChain, which contradict SUP condition
+         zorn04 : ¬ Maximal A 
+         zorn04 mx =  ∅< {HasMaximal} zc5 ( ≡o∅→=od∅  ¬Maximal ) where
+              zc5 : (y : Ordinal) →  odef A y → odef A (& (Maximal.maximal mx )) ∧ (¬ (* (& (Maximal.maximal mx ))  < * y ))
+              zc5 y ay = ⟪  Maximal.A∋maximal mx , (λ mx<y → Maximal.¬maximal<x mx (subst (λ k → odef A k ) (sym &iso) ay) (subst (λ k → k < * y) *iso mx<y) )  ⟫
+         zorn03 : ZChain A sa (& A)
+         zorn03 with TransFinite ind  (& A)
+         ... | case1 zc = zc
+         ... | case2 mx = ⊥-elim ( zorn04 mx )
 
 -- usage (see filter.agda )
 --