# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1657587378 -32400
# Node ID 96184d542e20fbfbe1a00146236b641afb155747
# Parent  0e28091e9271d2dec7b2c5861f47b2cb1bd2dfac
...

diff -r 0e28091e9271 -r 96184d542e20 src/zorn.agda
--- a/src/zorn.agda	Mon Jul 11 21:26:49 2022 +0900
+++ b/src/zorn.agda	Tue Jul 12 09:56:18 2022 +0900
@@ -456,7 +456,9 @@
      -- ZChain forces fix point on any ≤-monotonic function (fixpoint)
      -- ¬ Maximal create cf which is a <-monotonic function by axiom of choice. This contradicts fix point of ZChain
      --
-     z04 :  (nmx : ¬ Maximal A ) → (zc0 : (x : Ordinal) → ZChain1 A (cf nmx) (cf-is-≤-monotonic nmx)  as0 x) (zc : ZChain A (cf nmx) (cf-is-≤-monotonic nmx) as0 zc0 (& A)) 
+     z04 :  (nmx : ¬ Maximal A ) 
+           → (zc0 : (x : Ordinal) → ZChain1 A (cf nmx) (cf-is-≤-monotonic nmx)  as0 x) 
+           → (zc : ZChain A (cf nmx) (cf-is-≤-monotonic nmx) as0 zc0 (& A)) 
            → IsTotalOrderSet (ZChain.chain zc) → ⊥
      z04 nmx zc0 zc total = <-irr0  {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.A∋maximal  sp1 ))))
                                                (subst (λ k → odef A (& k)) (sym *iso) (SUP.A∋maximal sp1) )
@@ -537,17 +539,18 @@
              zc01 : odef A z ∧ UChain A f mf ay (ZChain1.supf (zc0 (& A))) (& A) z
              zc01 = uz
      ... | tri< 0<x ¬b ¬c with Oprev-p x
-     ... | yes op = {!!} where
+     ... | yes op = zc4 where
           --
           -- we have previous ordinal to use induction
           --
           px = Oprev.oprev op
-          supf : Ordinal → HOD
-          supf x =  {!!} -- ChainF A f mf ay x zc0 
           zc : ZChain A f mf ay zc0 (Oprev.oprev op)
           zc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) 
           px<x : px o< x
           px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc
+          zc0-b<x : (b : Ordinal ) → b o< x → b o< osuc px
+          zc0-b<x b lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt 
+
           -- if previous chain satisfies maximality, we caan reuse it
           --
           no-extenion : ( {a b z : Ordinal} → (z<x : z o< x)  → odef (ZChain.chain zc) a → b o< osuc x → (ab : odef A b) →
@@ -556,16 +559,14 @@
           no-extenion is-max  = record { initial = ZChain.initial zc ; chain∋init = ZChain.chain∋init zc }
 
           zc4 : ZChain A f mf ay zc0 x 
-          zc4 with o≤? x o∅
-          ... | yes x=0 = {!!}
-          ... | no 0<x with ODC.∋-p O A (* x)
+          zc4 with ODC.∋-p O A (* x)
           ... | no noax = no-extenion zc1  where -- ¬ A ∋ p, just skip
                 zc1 : {a b z : Ordinal} → (z<x : z o< x) → odef (ZChain.chain zc ) a → b o< osuc x → (ab : odef A b) →
                     HasPrev A (ZChain.chain zc ) ab f ∨  IsSup A (ZChain.chain zc ) ab →
                             * a < * b → odef (ZChain.chain zc ) b
                 zc1 {a} {b} z<x za b<ox ab P a<b with osuc-≡< b<ox
                 ... | case1 eq = ⊥-elim ( noax (subst (λ k → odef A k) (trans eq (sym &iso)) ab ) )
-                ... | case2 lt = ZChain.is-max zc za {!!}  ab P a<b
+                ... | case2 lt = ZChain.is-max zc za (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt ) ab P a<b
           ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) ax f )   
                -- we have to check adding x preserve is-max ZChain A y f mf zc0 x
           ... | case1 pr = no-extenion zc7  where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
@@ -578,7 +579,7 @@
                 ... | case1 b=x = subst (λ k → odef chain0 k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc (HasPrev.ay pr))
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) ax )
           ... | case1 is-sup = -- x is a sup of zc 
-                record {  chain⊆A = {!!} ; f-next = {!!}  ; f-total = {!!}
+                record {  chain⊆A = pchain⊆A ; f-next = {!!}  ; f-total = {!!}
                      ; initial = {!!} ; chain∋init  = {!!} ; is-max = {!!}   } where
                 sup0 : SUP A (ZChain.chain zc ) 
                 sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where
@@ -590,7 +591,14 @@
                 sp = SUP.sup sup0 
                 x=sup : x ≡ & sp 
                 x=sup = sym &iso 
+                pchain : HOD
+                pchain = UnionCF A f mf ay (ZChain1.supf (zc0 (& A))) (& A)
+                pchain⊆A : {y : Ordinal} → odef pchain y →  odef A y
+                pchain⊆A {y} ny = proj1 ny
+
+                -- odef A z ∧ UChain A f mf ay (ZChain1.supf (zc0 (& A))) (& A) z 
                 chain0 = ZChain.chain zc 
+                -- ≡ odef chain0 z ∨ FClosure A f (& sp) z
                 sc<A : {y : Ordinal} → odef chain0 y ∨ FClosure A f (& sp) y → y o< & A
                 sc<A {y} (case1 zx) = subst (λ k → k o< (& A)) &iso ( c<→o< (ZChain.chain⊆A zc (subst (λ k → odef chain0 k) (sym &iso) zx )))
                 sc<A {y} (case2 fx) = subst (λ k → k o< (& A)) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso) (A∋fc (& sp) f mf fx )) )
@@ -665,7 +673,7 @@
                      z23 : odef chain0 b
                      z23 with IsSup.x<sup (z24 p) ( ZChain.chain∋init zc )
                      ... | case1 y=b  = subst (λ k → odef chain0 k )  y=b ( ZChain.chain∋init zc )
-                     ... | case2 y<b  = ZChain.is-max zc (ZChain.chain∋init zc ) {!!} ab (case2 (z24 p)) y<b
+                     ... | case2 y<b  = ZChain.is-max zc (ZChain.chain∋init zc ) (zc0-b<x b b<x) ab (case2 (z24 p)) y<b
                 seq : schain ≡ supf0 x 
                 seq with trio< x x
                 ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl )
@@ -682,29 +690,23 @@
                             HasPrev A (ZChain.chain zc ) ab f ∨ IsSup A (ZChain.chain zc )   ab →
                             * a < * b → odef (ZChain.chain zc ) b
                 z18 {a} {b} z<x za b<x ab p a<b with osuc-≡< b<x
-                ... | case2 lt = ZChain.is-max zc za {!!} ab p a<b 
+                ... | case2 lt = ZChain.is-max zc za (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt ) ab p a<b 
                 ... | case1 b=x with p
-                ... | case1 pr = ⊥-elim ( ¬fy<x record {y = HasPrev.y pr ; ay = {!!} ; x=fy = trans (trans &iso (sym b=x) ) (HasPrev.x=fy pr ) } )
+                ... | case1 pr = ⊥-elim ( ¬fy<x record {y = HasPrev.y pr ; ay = HasPrev.ay pr ; x=fy = trans (trans &iso (sym b=x) ) (HasPrev.x=fy pr ) } )
                 ... | 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 {!!} )  } ) 
+                      x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=x (sym &iso)) (IsSup.x<sup b=sup zy )  } ) 
      ... | no op = zc5 where
-          supf : (z : Ordinal ) → z o< x  → HOD
-          supf x lt = {!!} -- ZChain1.chainf ( zc0  (& A) ) x 
-          uzc : {!!} -- {z : Ordinal} → (u : UChain x supf z) → ZChain A f mf ay zc0 (UChain.u u)
+          uzc : {z : Ordinal} → (u : UChain A f mf ay (ZChain1.supf (zc0 (& A))) x z ) → ZChain A f mf ay zc0 (UChain.u u)
           uzc {z} u =  prev (UChain.u u) (UChain.u<x u) 
-          Uz : HOD
-          Uz = {!!} -- record { od = record { def = λ z → odef A z ∧ ( UChain x supf z ∨ FClosure A f y z ) } ; odmax = & A ; <odmax = {!!}  }
-          -- Uzchain : ¬ (odef (ZChain1.chainf (zc0 (& A) ) x) x) → ZChain A f mf ay zc0 x
-          -- Uzchain nz = record { chain-mono = {!!}  ; chain⊆A = {!!} ; chain∋init = {!!} ; initial = {!!} ; f-next = {!!} ; f-total = {!!} ; is-max = {!!} }
+          UZ : HOD
+          UZ = UnionCF A f mf ay (ZChain1.supf (zc0 (& A))) x
           zc5 : ZChain A f mf ay zc0 x 
-          zc5 with o≤? x o∅
-          ... | yes x=0 = {!!}
-          ... | no 0<x with ODC.∋-p O A (* x)
+          zc5 with ODC.∋-p O A (* x)
           ... | no noax = {!!} where -- ¬ A ∋ p, just skip
-          ... | yes ax with ODC.p∨¬p O ( HasPrev A Uz ax f )   
+          ... | yes ax with ODC.p∨¬p O ( HasPrev A UZ ax f )   
                -- we have to check adding x preserve is-max ZChain A y f mf zc0 x
           ... | case1 pr = {!!} where -- 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 Uz ax )
+          ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A UZ ax )
           ... | case1 is-sup = {!!} -- x is a sup of (zc ?) 
           ... | case2 ¬x=sup =  {!!} -- no-extenion z18 where -- x is not f y' nor sup of former ZChain from y -- no extention