# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1651018105 -32400
# Node ID f8eb56442f2ca4cb95735f86b40a5ea103ecc8f8
# Parent  27bb51b7f012f615ac4a2a8f2f7670e92e30d6ff
tranfinite reorganization in Zorn

diff -r 27bb51b7f012 -r f8eb56442f2c src/zorn.agda
--- a/src/zorn.agda	Wed Apr 27 05:19:31 2022 +0900
+++ b/src/zorn.agda	Wed Apr 27 09:08:25 2022 +0900
@@ -224,6 +224,8 @@
      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 ))  )
+     sa0 : odef A (& s)
+     sa0 =  subst (λ k → odef A (& k) ) {!!} ( 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 → odef A x ∧ ( (m : Ordinal) →  odef A m → ¬ (* x < * m)) }  ; odmax = & A ; <odmax = z07 } 
      no-maximum : HasMaximal =h= od∅ → (x : Ordinal) → odef A x ∧ ((m : Ordinal) →  odef A m →  odef A x ∧ (¬ (* x < * m) )) →  ⊥
@@ -362,8 +364,7 @@
                 zc7 :  ZChain A sa f mf supO x
                 zc7 with ODC.∋-p O  (ZChain.chain zc0) (* ( f x ) )
                 ... | yes y = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next =  zc20 (ZChain.f-next zc0)
-                     ; f-immediate =  ZChain.f-immediate zc0 ; ¬chain∋x>z = z22 ; chain∋x  =  ZChain.chain∋x zc0
-                     ; is-max = λ za ba a<x → zc20 (λ za a<x → ZChain.is-max zc0 za ba a<x ) za a<x  }  where -- no extention
+                     ; f-immediate =  ZChain.f-immediate zc0 ; ¬chain∋x>z = z22 ; chain∋x  =  ZChain.chain∋x zc0 ; is-max = λ za ba a<x → zc20 (λ za a<x → ZChain.is-max zc0 za ba a<x ) za a<x  }  where -- no extention
                     z22 : {a : Ordinal} → x o< osuc a → ¬ odef (ZChain.chain zc0) a
                     z22 {a} x<oa = ZChain.¬chain∋x>z zc0 (ordtrans (subst (λ k → px o< k ) (Oprev.oprev=x op) <-osuc ) x<oa )
                     zc20 : {P : Ordinal →  Set n} → ({a : Ordinal} → odef (ZChain.chain zc0) a → a o< px → P a)
@@ -372,6 +373,11 @@
                     ... | tri< a₁ ¬b ¬c = prev za a₁
                     ... | tri≈ ¬a b ¬c = ⊥-elim ( ZChain.¬chain∋x>z zc0 (subst (λ k → k o< osuc a) b <-osuc ) za )
                     ... | tri> ¬a ¬b c = ⊥-elim ( ZChain.¬chain∋x>z zc0 (ordtrans c <-osuc ) za )
+                    z21 :  {a : Ordinal} → odef (ZChain.chain zc0) a → a o< x → odef (ZChain.chain zc0) (f a)
+                    z21 {a} za a<x with trio< a x
+                    ... | tri< a₁ ¬b ¬c = ZChain.f-next zc0 za {!!} 
+                    ... | tri≈ ¬a b ¬c = {!!}
+                    ... | tri> ¬a ¬b c = ⊥-elim ( o<> c a<x )
                 ... | no not = record { chain = zc5 ; chain⊆A =  ⊆-zc5
                     ; f-total = zc6 ; f-next = {!!} ; f-immediate = {!!} ; chain∋x  = case1 (ZChain.chain∋x zc0) ; ¬chain∋x>z = {!!} ; is-max = {!!} } where
                 --   extend with f x -- cahin ∋ y ∧  chain ∋ f y ∧ x ≡ f ( f y )
@@ -443,6 +449,24 @@
          nmx mx =  ∅< {HasMaximal} zc5 ( ≡o∅→=od∅  ¬Maximal ) where
               zc5 : odef A (& (Maximal.maximal mx)) ∧ (( y : Ordinal ) →  odef A y → ¬ (* (& (Maximal.maximal mx)) < * y)) 
               zc5 = ⟪  Maximal.A∋maximal mx , (λ y ay mx<y → Maximal.¬maximal<x mx (subst (λ k → odef A k ) (sym &iso) ay) (subst (λ k → k < * y) *iso mx<y) ) ⟫
+         record ZChain1 ( A : HOD )  {x : Ordinal} (ax : odef A x) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f )
+                 (sup : (C : Ordinal ) → (* C ⊆ A) → IsTotalOrderSet (* C) → Ordinal) : Set (Level.suc n) where
+           field
+              chain : HOD
+              chain⊆A : chain ⊆ A
+              chain∋x : odef chain x
+              f-total : IsTotalOrderSet chain 
+              f-next : {a : Ordinal } → odef chain a → odef chain (f a)
+              f-immediate : { x y : Ordinal } → odef chain x → odef chain y → ¬ ( ( * x < * y ) ∧ ( * y < * (f x )) )
+              is-max :  {a b : Ordinal } → (ca : odef chain a ) → (ba : odef A b) 
+                  → Prev< A chain ba f
+                       ∨  (sup (& chain) (subst (λ k → k  ⊆ A) (sym *iso) chain⊆A)  (subst (λ k → IsTotalOrderSet k) (sym *iso) f-total) ≡ b )
+                  → * a < * b  → odef chain b
+         ind4 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (x : Ordinal) →
+            ((y : Ordinal) → y o< x → odef A y ∧ ((ya : odef A y) → ZChain1 A ya f mf supO)) → odef A x ∧ ((ya : odef A x) → ZChain1 A ya f mf supO)
+         ind4 = {!!}
+         zorn04 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → odef A (& s) ∧ ((ya : odef A (& s)) → ZChain1 A ya f mf supO )
+         zorn04 f mf = TransFinite {λ y →  odef A y ∧ ( (ya : odef A y ) → ZChain1 A ya f mf supO ) } (ind4 f mf)  (& s ) 
          zorn03 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → ZChain A sa f mf supO (& A)
          zorn03 f mf = TransFinite (ind f mf)  (& A)