Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 861:4e60b42b83a3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 08 Sep 2022 14:33:08 +0900
parents 105f8d6c51fb
children 269467244745
files src/zorn.agda
diffstat 1 files changed, 142 insertions(+), 165 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Thu Sep 08 12:44:22 2022 +0900
+++ b/src/zorn.agda	Thu Sep 08 14:33:08 2022 +0900
@@ -261,6 +261,77 @@
     ch-is-sup  : (u : Ordinal) {z : Ordinal }  (u≤x : u o≤ x) ( is-sup : ChainP A f mf ay supf u ) 
         ( fc : FClosure A f (supf u) z ) → UChain A f mf ay supf x z
 
+-- data UChain is total
+
+chain-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal )
+   {s s1 a b : Ordinal } ( ca : UChain A f mf ay supf s a ) ( cb : UChain A f mf ay supf s1 b ) → Tri (* a < * b) (* a ≡ * b) (* b < * a )
+chain-total A f mf {y} ay supf {xa} {xb} {a} {b} ca cb = ct-ind xa xb ca cb where
+     ct-ind : (xa xb : Ordinal) → {a b : Ordinal} → UChain A f mf ay supf xa a → UChain A f mf ay supf xb b → Tri (* a < * b) (* a ≡ * b) (* b < * a)
+     ct-ind xa xb {a} {b} (ch-init fca) (ch-init fcb) = fcn-cmp y f mf fca fcb
+     ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub u≤x supb fcb) with ChainP.fcy<sup supb fca
+     ... | case1 eq with s≤fc (supf ub) f mf fcb
+     ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
+          ct00 : * a ≡ * b
+          ct00 = trans (cong (*) eq) eq1
+     ... | case2 lt = tri< ct01  (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt)  where
+          ct01 : * a < * b 
+          ct01 = subst (λ k → * k < * b ) (sym eq) lt
+     ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub u≤x supb fcb) | case2 lt = tri< ct01  (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt)  where
+          ct00 : * a < * (supf ub)
+          ct00 = lt
+          ct01 : * a < * b 
+          ct01 with s≤fc (supf ub) f mf fcb
+          ... | case1 eq =  subst (λ k → * a < k ) eq ct00
+          ... | case2 lt =  IsStrictPartialOrder.trans POO ct00 lt
+     ct-ind xa xb {a} {b} (ch-is-sup ua u≤x supa fca) (ch-init fcb) with ChainP.fcy<sup supa fcb
+     ... | case1 eq with s≤fc (supf ua) f mf fca
+     ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
+          ct00 : * a ≡ * b
+          ct00 = sym (trans (cong (*) eq) eq1 )
+     ... | case2 lt = tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01    where
+          ct01 : * b < * a 
+          ct01 = subst (λ k → * k < * a ) (sym eq) lt
+     ct-ind xa xb {a} {b} (ch-is-sup ua u≤x supa fca) (ch-init fcb) | case2 lt = tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01    where
+          ct00 : * b < * (supf ua)
+          ct00 = lt
+          ct01 : * b < * a 
+          ct01 with s≤fc (supf ua) f mf fca
+          ... | case1 eq =  subst (λ k → * b < k ) eq ct00
+          ... | case2 lt =  IsStrictPartialOrder.trans POO ct00 lt
+     ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x supb fcb) with trio< ua ub
+     ... | tri< a₁ ¬b ¬c with ChainP.order supb  (subst₂ (λ j k → j o< k ) (sym (ChainP.supu=u supa )) (sym (ChainP.supu=u supb )) a₁)  fca 
+     ... | case1 eq with s≤fc (supf ub) f mf fcb 
+     ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
+          ct00 : * a ≡ * b
+          ct00 = trans (cong (*) eq) eq1
+     ... | case2 lt =  tri< ct02  (λ eq → <-irr (case1 (sym eq)) ct02) (λ lt → <-irr (case2 ct02) lt)  where
+          ct02 : * a < * b 
+          ct02 = subst (λ k → * k < * b ) (sym eq) lt
+     ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x supb fcb) | tri< a₁ ¬b ¬c | case2 lt = tri< ct02  (λ eq → <-irr (case1 (sym eq)) ct02) (λ lt → <-irr (case2 ct02) lt)  where
+          ct03 : * a < * (supf ub)
+          ct03 = lt
+          ct02 : * a < * b 
+          ct02 with s≤fc (supf ub) f mf fcb
+          ... | case1 eq =  subst (λ k → * a < k ) eq ct03
+          ... | case2 lt =  IsStrictPartialOrder.trans POO ct03 lt
+     ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x  supb fcb) | tri≈ ¬a  eq ¬c 
+         = fcn-cmp (supf ua) f mf fca (subst (λ k → FClosure A f k b ) (cong supf (sym eq)) fcb )
+     ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x supb fcb) | tri> ¬a ¬b c with ChainP.order supa (subst₂ (λ j k → j o< k ) (sym (ChainP.supu=u supb )) (sym (ChainP.supu=u supa )) c) fcb 
+     ... | case1 eq with s≤fc (supf ua) f mf fca 
+     ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
+          ct00 : * a ≡ * b
+          ct00 = sym (trans (cong (*) eq) eq1)
+     ... | case2 lt =  tri> (λ lt → <-irr (case2 ct02) lt) (λ eq → <-irr (case1 eq) ct02) ct02    where
+          ct02 : * b < * a 
+          ct02 = subst (λ k → * k < * a ) (sym eq) lt
+     ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x supb fcb) | tri> ¬a ¬b c | case2 lt = tri> (λ lt → <-irr (case2 ct04) lt) (λ eq → <-irr (case1 (eq)) ct04) ct04    where
+          ct05 : * b < * (supf ua)
+          ct05 = lt
+          ct04 : * b < * a 
+          ct04 with s≤fc (supf ua) f mf fca
+          ... | case1 eq =  subst (λ k → * b < k ) eq ct05
+          ... | case2 lt =  IsStrictPartialOrder.trans POO ct05 lt
+
 ∈∧P→o< :  {A : HOD } {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A
 ∈∧P→o< {A } {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p )))
 
@@ -286,13 +357,9 @@
       supf :  Ordinal → Ordinal 
    chain : HOD
    chain = UnionCF A f mf ay supf z
+   chain⊆A : chain ⊆' A
+   chain⊆A = λ lt → proj1 lt
    field
-      chain⊆A : chain ⊆' A
-      chain∋init : odef chain y
-      initial : {z : Ordinal } → odef chain z → * y ≤ * z
-      f-next : {a : Ordinal } → odef chain a → odef chain (f a)
-      f-total : IsTotalOrderSet chain
-
       supf-max : {x : Ordinal } → z o≤ x  → supf z ≡ supf x
       sup : {x : Ordinal } → x o≤ z  → SUP A (UnionCF A f mf ay supf x)
       sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z  
@@ -301,6 +368,22 @@
       supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
       csupf : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf (supf b)) (supf b) 
 
+   chain∋init : odef chain y
+   chain∋init = ⟪ ay , ch-init (init ay refl)    ⟫
+   f-next : {a : Ordinal} → odef chain a → odef chain (f a)
+   f-next {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 (mf a aa) , ch-init (fsuc _ fc)  ⟫
+   f-next {a} ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u u≤x is-sup (fsuc _ fc ) ⟫
+   initial : {z : Ordinal } → odef chain z → * y ≤ * z
+   initial {a} ⟪ aa , ua ⟫  with  ua
+   ... | ch-init fc = s≤fc y f mf fc
+   ... | ch-is-sup u u≤x is-sup fc = ≤-ftrans (<=to≤ zc7) (s≤fc _ f mf fc)  where
+        zc7 : y <= supf u 
+        zc7 = ChainP.fcy<sup is-sup (init ay refl)
+   f-total : IsTotalOrderSet chain
+   f-total {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 
+               uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
+               uz01 = chain-total A f mf ay supf ( (proj2 ca)) ( (proj2 cb)) 
+
    supf-inject : {x y : Ordinal } → supf x o< supf y → x o<  y 
    supf-inject {x} {y} sx<sy with trio< x y
    ... | tri< a ¬b ¬c = a
@@ -401,77 +484,6 @@
       as : A ∋ maximal
       ¬maximal<x : {x : HOD} → A ∋ x  → ¬ maximal < x       -- A is Partial, use negative
 
--- data UChain is total
-
-chain-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal )
-   {s s1 a b : Ordinal } ( ca : UChain A f mf ay supf s a ) ( cb : UChain A f mf ay supf s1 b ) → Tri (* a < * b) (* a ≡ * b) (* b < * a )
-chain-total A f mf {y} ay supf {xa} {xb} {a} {b} ca cb = ct-ind xa xb ca cb where
-     ct-ind : (xa xb : Ordinal) → {a b : Ordinal} → UChain A f mf ay supf xa a → UChain A f mf ay supf xb b → Tri (* a < * b) (* a ≡ * b) (* b < * a)
-     ct-ind xa xb {a} {b} (ch-init fca) (ch-init fcb) = fcn-cmp y f mf fca fcb
-     ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub u≤x supb fcb) with ChainP.fcy<sup supb fca
-     ... | case1 eq with s≤fc (supf ub) f mf fcb
-     ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
-          ct00 : * a ≡ * b
-          ct00 = trans (cong (*) eq) eq1
-     ... | case2 lt = tri< ct01  (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt)  where
-          ct01 : * a < * b 
-          ct01 = subst (λ k → * k < * b ) (sym eq) lt
-     ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub u≤x supb fcb) | case2 lt = tri< ct01  (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt)  where
-          ct00 : * a < * (supf ub)
-          ct00 = lt
-          ct01 : * a < * b 
-          ct01 with s≤fc (supf ub) f mf fcb
-          ... | case1 eq =  subst (λ k → * a < k ) eq ct00
-          ... | case2 lt =  IsStrictPartialOrder.trans POO ct00 lt
-     ct-ind xa xb {a} {b} (ch-is-sup ua u≤x supa fca) (ch-init fcb) with ChainP.fcy<sup supa fcb
-     ... | case1 eq with s≤fc (supf ua) f mf fca
-     ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
-          ct00 : * a ≡ * b
-          ct00 = sym (trans (cong (*) eq) eq1 )
-     ... | case2 lt = tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01    where
-          ct01 : * b < * a 
-          ct01 = subst (λ k → * k < * a ) (sym eq) lt
-     ct-ind xa xb {a} {b} (ch-is-sup ua u≤x supa fca) (ch-init fcb) | case2 lt = tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01    where
-          ct00 : * b < * (supf ua)
-          ct00 = lt
-          ct01 : * b < * a 
-          ct01 with s≤fc (supf ua) f mf fca
-          ... | case1 eq =  subst (λ k → * b < k ) eq ct00
-          ... | case2 lt =  IsStrictPartialOrder.trans POO ct00 lt
-     ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x supb fcb) with trio< ua ub
-     ... | tri< a₁ ¬b ¬c with ChainP.order supb  (subst₂ (λ j k → j o< k ) (sym (ChainP.supu=u supa )) (sym (ChainP.supu=u supb )) a₁)  fca 
-     ... | case1 eq with s≤fc (supf ub) f mf fcb 
-     ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
-          ct00 : * a ≡ * b
-          ct00 = trans (cong (*) eq) eq1
-     ... | case2 lt =  tri< ct02  (λ eq → <-irr (case1 (sym eq)) ct02) (λ lt → <-irr (case2 ct02) lt)  where
-          ct02 : * a < * b 
-          ct02 = subst (λ k → * k < * b ) (sym eq) lt
-     ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x supb fcb) | tri< a₁ ¬b ¬c | case2 lt = tri< ct02  (λ eq → <-irr (case1 (sym eq)) ct02) (λ lt → <-irr (case2 ct02) lt)  where
-          ct03 : * a < * (supf ub)
-          ct03 = lt
-          ct02 : * a < * b 
-          ct02 with s≤fc (supf ub) f mf fcb
-          ... | case1 eq =  subst (λ k → * a < k ) eq ct03
-          ... | case2 lt =  IsStrictPartialOrder.trans POO ct03 lt
-     ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x  supb fcb) | tri≈ ¬a  eq ¬c 
-         = fcn-cmp (supf ua) f mf fca (subst (λ k → FClosure A f k b ) (cong supf (sym eq)) fcb )
-     ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x supb fcb) | tri> ¬a ¬b c with ChainP.order supa (subst₂ (λ j k → j o< k ) (sym (ChainP.supu=u supb )) (sym (ChainP.supu=u supa )) c) fcb 
-     ... | case1 eq with s≤fc (supf ua) f mf fca 
-     ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
-          ct00 : * a ≡ * b
-          ct00 = sym (trans (cong (*) eq) eq1)
-     ... | case2 lt =  tri> (λ lt → <-irr (case2 ct02) lt) (λ eq → <-irr (case1 eq) ct02) ct02    where
-          ct02 : * b < * a 
-          ct02 = subst (λ k → * k < * a ) (sym eq) lt
-     ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x supb fcb) | tri> ¬a ¬b c | case2 lt = tri> (λ lt → <-irr (case2 ct04) lt) (λ eq → <-irr (case1 (eq)) ct04) ct04    where
-          ct05 : * b < * (supf ua)
-          ct05 = lt
-          ct04 : * b < * a 
-          ct04 with s≤fc (supf ua) f mf fca
-          ... | case1 eq =  subst (λ k → * b < k ) eq ct05
-          ... | case2 lt =  IsStrictPartialOrder.trans POO ct05 lt
-
 init-uchain : (A : HOD)  ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } → (ay : odef A y ) 
     { supf : Ordinal → Ordinal } { x : Ordinal } → odef (UnionCF A f mf ay supf x) y
 init-uchain A f mf ay = ⟪ ay , ch-init (init ay refl)   ⟫
@@ -727,47 +739,12 @@
 
           pchain : HOD
           pchain  = UnionCF A f mf ay (ZChain.supf zc) px
-          ptotal : IsTotalOrderSet pchain
-          ptotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 
-               uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
-               uz01 = chain-total A f mf ay (ZChain.supf zc) ( (proj2 ca)) ( (proj2 cb)) 
-          pchain⊆A : {y : Ordinal} → odef pchain y →  odef A y
-          pchain⊆A {y} ny = proj1 ny
-          pnext : {a : Ordinal} → odef pchain a → odef pchain (f a)
-          pnext {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 (mf a aa) , ch-init (fsuc _ fc)  ⟫
-          pnext {a} ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u u≤x is-sup (fsuc _ fc ) ⟫
-          pinit :  {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁
-          pinit {a} ⟪ aa , ua ⟫  with  ua
-          ... | ch-init fc = s≤fc y f mf fc
-          ... | ch-is-sup u u≤x is-sup fc = ≤-ftrans (<=to≤ zc7) (s≤fc _ f mf fc)  where
-               zc7 : y <= (ZChain.supf zc) u 
-               zc7 = ChainP.fcy<sup is-sup (init ay refl)
-          pcy : odef pchain y
-          pcy = ⟪ ay , ch-init (init ay refl)    ⟫
 
           supf0 = ZChain.supf zc
 
           pchain1 : HOD
           pchain1  = UnionCF A f mf ay supf0 x
 
-          ptotal1 : IsTotalOrderSet pchain1
-          ptotal1 {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 
-               uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
-               uz01 = chain-total A f mf ay supf0 ( (proj2 ca)) ( (proj2 cb)) 
-          pchain⊆A1 : {y : Ordinal} → odef pchain1 y →  odef A y
-          pchain⊆A1 {y} ny = proj1 ny
-          pnext1 : {a : Ordinal} → odef pchain1 a → odef pchain1 (f a)
-          pnext1 {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 (mf a aa) , ch-init (fsuc _ fc)  ⟫
-          pnext1 {a} ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u u≤x is-sup (fsuc _ fc ) ⟫
-          pinit1 :  {y₁ : Ordinal} → odef pchain1 y₁ → * y ≤ * y₁
-          pinit1 {a} ⟪ aa , ua ⟫  with  ua
-          ... | ch-init fc = s≤fc y f mf fc
-          ... | ch-is-sup u u≤x is-sup fc = ≤-ftrans (<=to≤ zc7) (s≤fc _ f mf fc)  where
-               zc7 : y <= supf0 u 
-               zc7 = ChainP.fcy<sup is-sup (init ay refl)
-          pcy1 : odef pchain1 y
-          pcy1 = ⟪ ay , ch-init (init ay refl)    ⟫
-
           supfx : {z : Ordinal } → x o≤ z →  supf0 px ≡ supf0 z
           supfx {z} x≤z with trio< z px
           ... | tri< a ¬b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → z o< k ) (Oprev.oprev=x op) (ordtrans a <-osuc )))
@@ -789,6 +766,13 @@
               zc02 = ZChain.supf-max zc (o<→≤ (pxo<x op))
               zc01 : supf0 px ≡ supf0 z
               zc01 = ZChain.supf-max zc (OrdTrans (o<→≤ (pxo<x op)) z≤x)
+          zc04 : {b : Ordinal} → b o≤ x → (b o≤ px ) ∨ (b ≡ x )
+          zc04 {b} b≤x with trio< b px 
+          ... | tri< a ¬b ¬c = case1 (o<→≤ a)
+          ... | tri≈ ¬a b ¬c = case1 (o≤-refl0 b)
+          ... | tri> ¬a ¬b px<b with osuc-≡< b≤x
+          ... | case1 eq = case2 eq
+          ... | case2 b<x = ⊥-elim ( ¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x  ⟫ ) 
 
           -- if previous chain satisfies maximality, we caan reuse it
           --
@@ -796,8 +780,7 @@
 
           no-extension : ( (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨  HasPrev A pchain x f) → ZChain A f mf ay x
           no-extension P = record { supf = supf0 ;  sup = λ lt → STMP.tsup (sup lt ) ; supf-mono = supf-mono ; supf-max = supf-max
-               ; initial = pinit1 ; chain∋init = pcy1 ; sup=u = sup=u ; supf-is-sup = λ lt → STMP.tsup=sup (sup lt) ; csupf = csupf
-              ;  chain⊆A = λ lt → proj1 lt ;  f-next = pnext1 ;  f-total = ptotal1 }  where
+              ; sup=u = sup=u ; supf-is-sup = λ lt → STMP.tsup=sup (sup lt) ; csupf = csupf }  where
                  pchain0=1 : pchain ≡ pchain1
                  pchain0=1 =  ==→o≡ record { eq→ = zc10 ; eq← = zc11 P } where
                      zc10 :  {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z
@@ -884,14 +867,6 @@
                      zc31 (case2 hasPrev ) with zc30
                      ... | refl = ⊥-elim ( proj2 is-sup (subst (λ k → HasPrev A k x f) pchain0=1 hasPrev ) ) 
 
-                 zc04 : {b : Ordinal} → b o≤ x → (b o≤ px ) ∨ (b ≡ x )
-                 zc04 {b} b≤x with trio< b px 
-                 ... | tri< a ¬b ¬c = case1 (o<→≤ a)
-                 ... | tri≈ ¬a b ¬c = case1 (o≤-refl0 b)
-                 ... | tri> ¬a ¬b px<b with osuc-≡< b≤x
-                 ... | case1 eq = case2 eq
-                 ... | case2 b<x = ⊥-elim ( ¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x  ⟫ ) 
-
                  csupf :  {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf0 (supf0 b)) (supf0 b)
                  csupf {b} b≤x with zc04 b≤x 
                  ... | case2 b=x = subst (λ k → odef (UnionCF A f mf ay supf0 k) k) (ZChain.supf-max zc zc05 ) ( ZChain.csupf zc o≤-refl ) where
@@ -907,30 +882,52 @@
           ... | case1 pr = no-extension (case2 pr) -- 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 (ZChain.chain zc ) ax )
           ... | case1 is-sup = -- x is a sup of zc 
-                record {  supf = ? ; chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} ; csupf = {!!} ; sup=u = {!!} ; supf-mono = {!!}
-                   ;  initial = {!!} ; chain∋init  = {!!} ; sup = {!!} ; supf-is-sup = {!!}   }  where
+                record {  supf = supf1 
+                   ; csupf = {!!} ; sup=u = {!!} ; supf-mono = {!!}
+                   ; sup = {!!} ; supf-is-sup = {!!}   }  where
              supf1 : Ordinal → Ordinal
              supf1 z with trio< z px 
              ... | tri< a ¬b ¬c = ZChain.supf zc z
              ... | tri≈ ¬a b ¬c = ZChain.supf zc z
              ... | tri> ¬a ¬b c = x
-             supx : SUP A (UnionCF A f mf ay supf0 x)
-             supx = record { sup = * x ; as = subst (λ k → odef A k ) {!!} ax ; x<sup = {!!} }
-             spx = & (SUP.sup supx )
-             x=spx : x ≡ spx
-             x=spx = sym &iso
-             psupf1 : Ordinal → Ordinal
-             psupf1 z = ?
-             csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay psupf1 b) (psupf1 b)
-             csupf {b} b≤x with trio< b px | inspect psupf1 b
-             ... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ {!!} , {!!} ⟫
-             ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ {!!} , {!!} ⟫
-             ... | tri> ¬a ¬b c | record { eq = eq1 } = {!!} where -- b ≡ x, supf x ≡ sp
-                  zc30 : x ≡ b
-                  zc30 with trio< x b
-                  ... | tri< a ¬b ¬c = {!!}
-                  ... | tri≈ ¬a b ¬c = {!!}
-                  ... | tri> ¬a ¬b c = {!!}
+
+             pchainx : HOD
+             pchainx = UnionCF A f mf ay supf1 x
+
+             supf0px=x : supf0 px ≡ x
+             supf0px=x = ? where
+                 zc50 : supf0 px ≡ & (SUP.sup (ZChain.sup zc o≤-refl ) )
+                 zc50 = ZChain.spuf-is-sup zc ?
+
+             supf-monox : {a b : Ordinal } → a o≤ b → supf1 a o≤ supf1 b
+             supf-monox {i} {j} i≤j with trio< i px | trio< j px
+             ... | tri< a ¬b ¬c | tri< ja ¬jb ¬jc  = ?
+             ... | tri< a ¬b ¬c | tri≈ ¬ja jb ¬jc  = ?
+             ... | tri< a ¬b ¬c | tri> ¬ja ¬jb jc  = ?
+             ... | tri≈ ¬a b ¬c | tri< ja ¬jb ¬jc  = ?
+             ... | tri≈ ¬a b ¬c | tri≈ ¬ja jb ¬jc  = ?
+             ... | tri≈ ¬a b ¬c | tri> ¬ja ¬jb jc  = ?
+             ... | tri> ¬a ¬b c | tri< ja ¬jb ¬jc  = ?
+             ... | tri> ¬a ¬b c | tri≈ ¬ja jb ¬jc  = ?
+             ... | tri> ¬a ¬b c | tri> ¬ja ¬jb jc  = ?
+
+             pchain⊆x : UnionCF A f mf ay supf0 px ⊆'  UnionCF A f mf ay supf1 x
+             pchain⊆x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ 
+             pchain⊆x ⟪ au , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ au , ch-is-sup u ? ? ? ⟫ 
+
+             supfx1 : {z : Ordinal } → x o≤ z →  supf1 z ≡ x
+             supfx1 {z} x≤z with trio< z px
+             ... | tri< a ¬b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → z o< k ) (Oprev.oprev=x op) (ordtrans a <-osuc )))
+             ... | tri≈ ¬a b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → k o< x ) (sym b) (pxo<x op)))
+             ... | tri> ¬a ¬b c = refl
+            
+             csupf :  {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 (supf1 b)) (supf1 b)
+             csupf {b} b≤x with zc04 b≤x 
+             ... | case2 b=x = ⟪ ? , ch-is-sup x ? ? (init ? ? ) ⟫
+             ... | case1 b≤px with ZChain.csupf zc b≤px 
+             ... | ⟪ au , ch-init fc ⟫ = ⟪ ? , ch-init ? ⟫ 
+             ... | ⟪ au , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ ? , ch-is-sup u ? ? ? ⟫ 
+
 
           ... | case2 ¬x=sup =  no-extension (case1 nsup) where -- px is not f y' nor sup of former ZChain from y -- no extention
              nsup : ¬ xSUP (UnionCF A f mf ay supf0 px) x 
@@ -979,24 +976,6 @@
           pchain1 : HOD
           pchain1 = UnionCF A f mf ay supf1 x
 
-          pchain⊆A : {y : Ordinal} → odef pchain1 y →  odef A y
-          pchain⊆A {y} ny = proj1 ny
-          pnext : {a : Ordinal} → odef pchain1 a → odef pchain1 (f a)
-          pnext {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf a aa ) , ch-init (fsuc _ fc) ⟫
-          pnext {a} ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪  proj2 ( mf a aa ) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫
-          pinit :  {y₁ : Ordinal} → odef pchain1 y₁ → * y ≤ * y₁
-          pinit {a} ⟪ aa , ua ⟫  with  ua
-          ... | ch-init fc = s≤fc y f mf fc
-          ... | ch-is-sup u u≤x is-sup fc = ≤-ftrans (<=to≤ zc7) (s≤fc _ f mf fc)  where
-               zc7 : y <= supf1 _
-               zc7 = ChainP.fcy<sup is-sup (init ay refl)
-          pcy : odef pchain1 y
-          pcy = ⟪ ay , ch-init (init ay refl)    ⟫
-          ptotal : IsTotalOrderSet pchain1
-          ptotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 
-               uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
-               uz01 = chain-total A f mf ay supf1 ( (proj2 ca)) ( (proj2 cb)) 
-
           is-max-hp : (supf : Ordinal → Ordinal) (x : Ordinal) {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
                 b o< x → (ab : odef A b) →
                 HasPrev A (UnionCF A f mf ay supf x) b f → 
@@ -1011,9 +990,8 @@
           zc70 pr xsup = ?
 
           no-extension : ¬ ( xSUP (UnionCF A f mf ay supf0 x) x ) → ZChain A f mf ay x
-          no-extension ¬sp=x  = record { initial = pinit ; chain∋init = pcy  ; supf = supf1  ; sup=u = sup=u 
-               ; sup = sup ; supf-is-sup = sis ; supf-mono = {!!}
-               ; csupf = csupf ; chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal } where
+          no-extension ¬sp=x  = record { supf = supf1  ; sup=u = sup=u 
+               ; sup = sup ; supf-is-sup = sis ; supf-mono = {!!} ; csupf = csupf } where
                  supfu : {u : Ordinal } → ( a : u o< x ) → (z : Ordinal) → Ordinal
                  supfu {u} a z = ZChain.supf (pzc (osuc u) (ob<x lim a)) z
                  pchain0=1 : pchain ≡ pchain1
@@ -1070,9 +1048,8 @@
                -- we have to check adding x preserve is-max ZChain A y f mf x
           ... | case1 pr = no-extension {!!} 
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax )
-          ... | case1 is-sup = record { initial = {!!} ; chain∋init = {!!}  ; supf = supf1  ; sup=u = {!!} 
-               ; sup = {!!} ; supf-is-sup = {!!} ; supf-mono = {!!}
-               ;  chain⊆A = {!!} ;  f-next = {!!} ;  f-total = {!!} ; csupf = {!!}  } -- where -- x is a sup of (zc ?) 
+          ... | case1 is-sup = record { supf = supf1  ; sup=u = {!!} 
+               ; sup = {!!} ; supf-is-sup = {!!} ; supf-mono = {!!};  csupf = {!!}  } -- where -- x is a sup of (zc ?) 
           ... | case2 ¬x=sup =  no-extension {!!} -- x is not f y' nor sup of former ZChain from y -- no extention
          
      SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f mf ay   (& A)