# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1654645672 -32400
# Node ID 40090ce9232c9c192339a9ea2c80f7f0b38da74c
# Parent  9922bfe92278ff99c5aba51abb24c77b26ed8293
...

diff -r 9922bfe92278 -r 40090ce9232c src/zorn.agda
--- a/src/zorn.agda	Tue Jun 07 18:37:57 2022 +0900
+++ b/src/zorn.agda	Wed Jun 08 08:47:52 2022 +0900
@@ -254,7 +254,7 @@
       chainf :  (b : Ordinal) → HOD
       chain-mono :  {a b : Ordinal} → a o< b → chainf a  ⊆' chainf b
       chain=zchain : {b : Ordinal} → chainf z ≡ ZChain.chain zchain 
-      
+
 record Maximal ( A : HOD )  : Set (Level.suc n) where
    field
       maximal : HOD
@@ -389,21 +389,19 @@
           sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc
           c = & (SUP.sup sp1)
 
-     ind1 :   ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) →  (x : Ordinal)
-          → ((y : Ordinal) → y o< x → {y = y₁ : Ordinal} → odef A y₁ → ZChain∧Chain A y₁ f y) →
-            {y : Ordinal} → odef A y → ZChain∧Chain A y f x
-     ind1 = {!!}
-
      --
      -- create all ZChains under o< x
      --
-     ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (x : Ordinal) →
-            ((z : Ordinal) → z o< x → {y : Ordinal} → (ya : odef A y) → ZChain A y f z ) → { y : Ordinal } → (ya : odef A y) → ZChain A y f x
-     ind f mf x prev {y} ay with Oprev-p x
-     ... | yes op = zc4 where
+     ind :   ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) →  (x : Ordinal)
+          → ((z : Ordinal) → z o< x → {y : Ordinal} → odef A y → ZChain∧Chain A y f z) →
+            {y : Ordinal} → odef A y → ZChain∧Chain A y f x
+     ind f mf x prevzc {y} ay with Oprev-p x
+     ... | yes op = record { zchain = zc4 ; chainf = {!!} ; chain-mono = {!!} ; chain=zchain = {!!} } where
           --
           -- we have previous ordinal to use induction
           --
+          prev : (z : Ordinal) → z o< x → {y : Ordinal} → odef A y → ZChain A y f z
+          prev z z<x ay = ZChain∧Chain.zchain (prevzc z z<x ay)
           px = Oprev.oprev op
           zc0 : ZChain A y f (Oprev.oprev op)
           zc0 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) ay
@@ -433,11 +431,11 @@
                 ... | case1 b=x = subst (λ k → odef chain k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc0 (HasPrev.ay pr))
                 zc9 :  ZChain A y f x
                 zc9 = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next =  ZChain.f-next zc0 -- no extention
-                     ; initial = ZChain.initial zc0 ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = zc17 ; fc∨sup = {!!}}  
+                     ; initial = ZChain.initial zc0 ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = zc17 ; fc∨sup = {!!}   }
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc0) ax )
           ... | case1 is-sup = -- x is a sup of zc0 
                 record { chain = schain ; chain⊆A = s⊆A  ; f-total = scmp ; f-next = scnext 
-                     ; initial = scinit ; f-immediate =  simm ; chain∋x  = case1 (ZChain.chain∋x zc0) ; is-max = s-ismax ; fc∨sup = {!!}} where 
+                     ; initial = scinit ; f-immediate =  simm ; chain∋x  = case1 (ZChain.chain∋x zc0) ; is-max = s-ismax ; fc∨sup = {!!} } where 
                 sup0 : SUP A (ZChain.chain zc0) 
                 sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where
                         x21 :  {y : HOD} → ZChain.chain zc0 ∋ y → (y ≡ * x) ∨ (y < * x)
@@ -550,10 +548,15 @@
                 ... | case2 b=sup = ⊥-elim ( ¬x=sup record { 
                       x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=x (sym &iso)) (IsSup.x<sup b=sup zy)  } ) 
      ... | no ¬ox with trio< x y
-     ... | tri< a ¬b ¬c = record { chain = {!!} ; chain⊆A = {!!}  ; f-total = {!!}  ; f-next = {!!}
+     ... | tri< a ¬b ¬c = record { zchain = 
+            record { chain = {!!} ; chain⊆A = {!!}  ; f-total = {!!}  ; f-next = {!!}
                      ; initial = {!!} ; f-immediate = {!!} ; chain∋x  = {!!} ; is-max = {!!} ; fc∨sup = {!!} }
+            ; chainf = {!!} ; chain-mono = {!!} ; chain=zchain = {!!} }
      ... | tri≈ ¬a b ¬c = {!!}
-     ... | tri> ¬a ¬b y<x = {!!} where
+     ... | tri> ¬a ¬b y<x = record { zchain = UnionZ 
+            ; chainf = {!!} ; chain-mono = {!!} ; chain=zchain = {!!} } where
+       prev : (z : Ordinal) → z o< x → {y : Ordinal} → odef A y → ZChain A y f z
+       prev z z<x ay = ZChain∧Chain.zchain (prevzc z z<x ay)
        UnionZ : ZChain A y f x
        UnionZ = record { chain = Uz ; chain⊆A = Uz⊆A  ; f-total = u-total  ; f-next = u-next
                      ; initial = u-initial ; f-immediate = {!!} ; chain∋x  = {!!} ; is-max = {!!} ; fc∨sup = {!!} }  where --- limit ordinal case
@@ -575,8 +578,20 @@
          u-initial {z} u = ZChain.initial ( uzc u )  (UZFChain.chain∋z u)
          u-chain∋x :  odef Uz y
          u-chain∋x = record { u = y ; u<x = y<x ; chain∋z = ZChain.chain∋x (prev y y<x ay ) }
+         u-total1 : {x y : HOD } → (ux : odef Uz (& x)) → (uy : odef Uz (& y))
+             → & x o< & y → odef (ZChain.chain (uzc ux)) (& x) → odef (ZChain.chain (uzc uy)) (& x)
+         u-total1 {x} {y} ux uy  x<y =  ZChain∧Chain.chain-mono {!!} x<y where
+             u00 : ZChain∧Chain A {!!} f {!!}
+             u00 = prevzc {!!} {!!} {!!}
+             u02 : HOD
+             u02 = ZChain∧Chain.chainf u00 {!!}
+             u01 : odef {!!} (& x) → odef {!!} (& y)
+             u01 = ZChain∧Chain.chain-mono u00 x<y 
          u-total : IsTotalOrderSet Uz
-         u-total {x} {y} ux uy = {!!}
+         u-total {x} {y} ux uy with trio< (& x) (& y)
+         ... | tri< a ¬b ¬c = ZChain.f-total (uzc uy) (u-total1 ux uy a (UZFChain.chain∋z ux)) (UZFChain.chain∋z uy)
+         ... | tri≈ ¬a b ¬c =  tri≈ {!!} {!!} {!!}
+         ... | tri> ¬a ¬b c = ZChain.f-total (uzc ux) (UZFChain.chain∋z ux) (u-total1 uy ux c (UZFChain.chain∋z uy)) 
          --- ux ⊆ uy ∨ uy ⊆ ux
          
      zorn00 : Maximal A 
@@ -595,13 +610,11 @@
          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) ) ⟫
-         zorn03 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (ya : odef A (& s)) → ZChain A (& s) f (& A)
-         zorn03 f mf = TransFinite {λ z → {y : Ordinal } → (ya : odef A y ) → ZChain A y f z } (ind f mf) (& A)
+         zorn03 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (ya : odef A (& s)) → ZChain∧Chain A (& s) f (& A)
+         zorn03 f mf = TransFinite {λ z → {y : Ordinal } → (ya : odef A y ) → ZChain∧Chain  A y f z } (ind f mf) (& A)
+
          zorn04 : ZChain A (& s) (cf nmx)  (& A)
-         zorn04 = zorn03 (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as )
-
-         zorn05 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (ya : odef A (& s)) → ZChain∧Chain A (& s) f (& A)
-         zorn05 f mf = TransFinite {λ z → {y : Ordinal } → (ya : odef A y ) → ZChain∧Chain  A y f z } {!!} (& A)
+         zorn04 = ZChain∧Chain.zchain (zorn03 (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as ))
 
 -- usage (see filter.agda )
 --