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

diff -r 8facdd7cc65a -r 6e94ea146fc1 src/zorn.agda
--- a/src/zorn.agda	Wed Apr 20 01:54:57 2022 +0900
+++ b/src/zorn.agda	Wed Apr 20 10:44:38 2022 +0900
@@ -140,18 +140,8 @@
       x : HOD
       iso : TA OS≈ (Cut<T TA x) 
 
-OS<-cmp : {x : HOD} → Trichotomous {_} {IsTotalOrderSet x} _OS≈_ _OS<_ 
-OS<-cmp A B = {!!}
-
-record ZChain ( A : HOD ) (y : Ordinal)   : Set (Level.suc n) where
-   field
-      max : HOD
-      A∋max : A ∋ max
-      y<max : y o< & max
-      chain : HOD
-      chain⊆A : chain ⊆ A  
-      total : IsTotalOrderSet chain 
-      chain-max : (x : HOD) → chain ∋ x → (x ≡ max ) ∨ ( x < max )
+-- OS<-cmp : {x : HOD} → Trichotomous {_} {IsTotalOrderSet x} _OS≈_ _OS<_ 
+-- OS<-cmp A B = {!!}
 
 data IChain  (A : HOD) : Ordinal → Set n where
     ifirst : {ox : Ordinal} → odef A ox → IChain A ox
@@ -270,7 +260,7 @@
     IPO : IsPartialOrderSet (InFCSet A ax ifc )
     IPO = ⊆-IsPartialOrderSet record { incl = λ {y} lt → incl (InFCSet⊆A A {x} ax ifc) lt} PO
     B = IChainSet A ax
-    cnext = {!!} -- cinext A ax ifc
+    cnext = cinext A ax ifc
     ct02 : {oy : Ordinal} → (y : Chain B x cnext oy ) → A ∋ * oy 
     ct02 y = incl (IChainSet⊆A {A} ax) (subst (λ k → odef (IChainSet A ax) k) (sym &iso) (ct∈A B x cnext y) ) 
     ct-inject : {ox oy : Ordinal} → (x1 : Chain B x cnext ox ) → (y : Chain B x cnext oy )
@@ -288,7 +278,7 @@
         ct07 :  * ox < * (cnext oy1)
         ct07 with ODC.∋-p O (IChainSet A ax) (* oy1)
         ... | no not  = ⊥-elim ( not (subst (λ k → odef (IChainSet A ax) k ) (sym &iso) ay ) )
-        ... | yes ay1 = {!!} where -- IsStrictPartialOrder.trans PO {me (ct02 x1) } {me (ct02 y)} {me ct031 } (ct-monotonic x1 y a ) ct011 where
+        ... | yes ay1 = IsStrictPartialOrder.trans PO {me (ct02 x1) } {me (ct02 y)} {me ct031 } (ct-monotonic x1 y a ) ct011 where
            ct031 :  A ∋ * (IChainSup>.y (InfiniteChain.c-infinite ifc oy1 (subst (λ k → odef (IChainSet A ax) k) &iso ay1 ) )) 
            ct031 = subst (λ k → odef A k ) (sym &iso) (
               IChainSup>.A∋y (InfiniteChain.c-infinite ifc oy1 (subst (λ k → odef (IChainSet A ax) k) &iso ay1 )) )
@@ -298,7 +288,7 @@
            ct11 : * ox < * (cnext oy1)
            ct11 with ODC.∋-p O (IChainSet A ax) (* oy1)
            ... | no not  = ⊥-elim ( not (subst (λ k → odef (IChainSet A ax) k ) (sym &iso) ay ) )
-           ... | yes ay1 = subst (λ k → * k < _) (sym (ct-inject _ _ b)) {!!} where
+           ... | yes ay1 = subst (λ k → * k < _) (sym (ct-inject _ _ b)) ct011  where
               ct011 :  * oy1 < * ( IChainSup>.y (InfiniteChain.c-infinite ifc oy1 (subst (λ k → odef (IChainSet A ax) k) &iso ay1 )) )
               ct011 = IChainSup>.y>x (InfiniteChain.c-infinite ifc oy1 (subst (λ k → odef (IChainSet A ax) k) &iso ay1 )) 
     ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> lt c ) 
@@ -328,17 +318,6 @@
         ct15 : ¬ (elm x1 <  elm y)
         ct15 lt = ct13 {x1} {y} lt (subst₂ (λ j k → j < k ) *iso *iso (ct-monotonic (is-elm y) (is-elm x1) c )  )
 
-extendInfiniteChain : (A : HOD) → {x mx y my : Ordinal}  (ax : A ∋ * x) (ay : A ∋ * y)
-     → IsPartialOrderSet A 
-     → (ifcx : InfiniteChain A mx ax ) → (ifcy : InfiniteChain A my ay )
-     → * y ≤ * mx
-     → InfiniteChain A (maxα mx my) ax 
-extendInfiniteChain A {x} {mx} {y} {my} ax ay PO ifcx ifcy y<mx = record { chain<x = eic00 ; c-infinite = eic01 } where
-    eic00 : (z : Ordinal) → odef (IChainSet A ax) z → z o< maxα mx my
-    eic00 z xz = {!!}
-    eic01 :  (z : Ordinal) (cy : odef (IChainSet A ax) z) → IChainSup> A (ic→A∋y A ax cy)
-    eic01 z cy = {!!}
-      
 record IsFC (A : HOD) {x : Ordinal}  (ax : A ∋ * x) (y : Ordinal) : Set n where
    field
       icy : odef (IChainSet A ax) y  
@@ -441,6 +420,22 @@
              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 = {!!}
+
+record ZChain ( A : HOD ) (y : 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 )
+
 record SUP ( A B : HOD )  : Set (Level.suc n) where
    field
       sup : HOD
@@ -459,22 +454,14 @@
           (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 nxa (SUP.A∋maximal sup) (SUP.x<sup sup {!!} ) {!!} where
-              nx : Ordinal
-              nx = cinext A ax ifc (& (SUP.sup sup))
-              zc7 : A ∋ * (& (SUP.sup sup))
-              zc7 = subst (λ k → odef A k ) (cong (&) (sym *iso)) (SUP.A∋maximal sup)
-              sup-ics :  odef (IChainSet A ax) (& (SUP.sup sup))
-              sup-ics = {!!} -- SUP.A∋maximal sup
-              ncsup : (z : Ordinal) → (az : odef (IChainSet A ax) z)  → IChainSup> A {z} (subst (odef A) (sym &iso) (proj1 az)) 
-              ncsup z az = InfiniteChain.c-infinite ifc z az
-              nxa : A ∋ * nx
-              nxa = {!!} -- cinext∈A A ax ifc (& (SUP.sup sup)) {!!}
+          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  → ⊥
@@ -487,7 +474,7 @@
      zorn03 x = TransFinite ind  x
      zorn04 : Maximal A 
      zorn04 with zorn03 (& A)
-     ... | case1 chain = ⊥-elim ( o<> (c<→o< {ZChain.max chain} {A} (ZChain.A∋max chain))  (ZChain.y<max chain) )
+     ... | case1 chain = ⊥-elim ( o<> (c<→o< {ZChain.zmax chain} {A} (ZChain.A∋max chain))  (ZChain.y<max chain) )
      ... | case2 m = m
 
 -- usage (see filter.agda )