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

changeset 748:6c8ba542d11b

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 Fri, 22 Jul 2022 10:15:05 +0900
parents c35a5001a0f8
children c3388f0e9899
files src/zorn.agda
diffstat 1 files changed, 91 insertions(+), 105 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Thu Jul 21 13:20:04 2022 +0900
+++ b/src/zorn.agda	Fri Jul 22 10:15:05 2022 +0900
@@ -264,21 +264,14 @@
       y<s      : y << supf u  -- not a initial chain
       supfu=u  : supf u ≡ u 
 
-data Chain (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal) : Ordinal →  Ordinal → Set n where
-    ch-init    : (z : Ordinal) → FClosure A f y z  → Chain A f mf  ay supf o∅ z 
-    ch-is-sup : {sup z : Ordinal } 
-         → ( is-sup : ChainP A f mf ay supf sup z)
-         → ( fc : FClosure A f (supf sup) z ) → Chain A f mf ay supf sup z
-
 -- Union of supf z which o< x
 --
 
-record UChain  ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y )
-       (supf : Ordinal → Ordinal) (x : Ordinal)  (z : Ordinal) : Set n where 
-   field
-      u : Ordinal
-      u<x : (u o< x ) ∨ ( u ≡ o∅)
-      uchain : Chain A f mf ay supf u z
+data UChain  ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y )
+       (supf : Ordinal → Ordinal) (x : Ordinal) : (z : Ordinal) → Set n where 
+    ch-init : {z : Ordinal } (fc : FClosure A f y z) → UChain A f mf ay supf x z
+    ch-is-sup  : (u : Ordinal) {z : Ordinal } (u<x : u o< x ) ( is-sup : ChainP A f mf ay supf u z) 
+        ( fc : FClosure A f (supf u) z ) → UChain A f mf ay supf x z
 
 ∈∧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 )))
@@ -321,47 +314,49 @@
       A∋maximal : A ∋ maximal
       ¬maximal<x : {x : HOD} → A ∋ x  → ¬ maximal < x       -- A is Partial, use negative
 
--- data Chain is total
+-- 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 : Chain A f mf ay supf s a ) ( cb : Chain A f mf ay supf s1 b ) → Tri (* a < * b) (* a ≡ * b) (* b < * a )
+   {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} → Chain A f mf ay supf xa a → Chain A f mf ay supf xb b → Tri (* a < * b) (* a ≡ * b) (* b < * a)
-     ct-ind xa xb {a} {b} (ch-init a fca) (ch-init b fcb) = fcn-cmp y f mf fca fcb
-     ct-ind xa xb {a} {b} (ch-init a fca) (ch-is-sup supb fcb) = tri< ct01  (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt)  where
-          ct00 : * a < * (supf xb)
+     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 ub<x supb fcb) = tri< ct01  (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt)  where
+          ct02 : * a < * (supf xb)
+          ct02 = ? -- ChainP.fcy<sup supb fca
+          ct00 : * a < * (supf ub)
           ct00 = ChainP.fcy<sup supb fca
           ct01 : * a < * b 
-          ct01 with s≤fc (supf xb) f mf fcb
+          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 supa fca) (ch-init b fcb)= tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01    where
+     ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-init fcb)= tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01    where
           ct00 : * b < * (supf xa)
-          ct00 = ChainP.fcy<sup supa fcb
+          ct00 = ? -- ChainP.fcy<sup supa fcb
           ct01 : * b < * a 
-          ct01 with s≤fc (supf xa) f mf  fca
+          ct01 with s≤fc (supf xa) 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 supa fca) (ch-is-sup supb fcb) with trio< xa xb
+     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 = tri< ct02  (λ eq → <-irr (case1 (sym eq)) ct02) (λ lt → <-irr (case2 ct02) lt)  where
-          ct03 : * a < * (supf xb)
-          ct03 = ChainP.order supb a₁ (ChainP.csupz supa)
+          ct03 : * a < * (supf ub)
+          ct03 = ChainP.order supb  a₁ (ChainP.csupz supa)
           ct02 : * a < * b 
-          ct02 with s≤fc (supf xb) f mf fcb
+          ct02 with s≤fc (supf ub) f mf fcb
           ... | case1 eq =  subst (λ k → * a < k ) eq ct03
           ... | case2 lt =  IsStrictPartialOrder.trans POO ct03 lt
-     ... | tri≈ ¬a  refl ¬c = fcn-cmp (supf xa) f mf fca fcb
+     ... | tri≈ ¬a  refl ¬c = fcn-cmp (supf xa) f mf ? ?
      ... | tri> ¬a ¬b c = tri> (λ lt → <-irr (case2 ct04) lt) (λ eq → <-irr (case1 (eq)) ct04) ct04    where
           ct05 : * b < * (supf xa)
-          ct05 = ChainP.order supa c (ChainP.csupz supb)
+          ct05 = ? --  ChainP.order supa ? (ChainP.csupz supb)
           ct04 : * b < * a 
-          ct04 with s≤fc (supf xa) f mf fca
+          ct04 with s≤fc (supf xa) 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 , record { u = o∅ ; u<x = case2 refl ; uchain = ch-init _ (init ay)  } ⟫
+init-uchain A f mf ay = ⟪ ay , ch-init (init ay)   ⟫
 
 ChainP-next : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal )
    → {x z : Ordinal } →  ChainP A f mf ay supf x z → ChainP A f mf ay supf x (f z )
@@ -433,35 +428,34 @@
      SZ1 A f mf {y} ay zc x = TransFinite { λ x →  ZChain1 A f mf ay zc x } zc1 x where
         chain-mono2 : (x : Ordinal) {a b c : Ordinal} → a o≤ b → b o≤ x →
             odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c
-        chain-mono2 x {a} {b} {c} a≤b b≤x ⟪ ua , record { u = _ ; u<x = u<x ; uchain = ch-init .c fc } ⟫ = 
-            ⟪ ua , record { u = _ ; u<x = case2 refl  ; uchain = ch-init c fc } ⟫ 
-        chain-mono2 x {a} {b} {c} a≤b b≤x ⟪ ua , record { u = u ; u<x = case1 u<x ; uchain = ch-is-sup is-sup fc } ⟫ = 
-            ⟪ ua , record { u = u ; u<x = case1 (ordtrans<-≤ u<x a≤b) ; uchain = ch-is-sup is-sup fc } ⟫ 
+        chain-mono2 x {a} {b} {c} a≤b b≤x ⟪ ua , ch-init fc  ⟫ = 
+            ⟪ ua , ch-init fc  ⟫ 
+        chain-mono2 x {a} {b} {c} a≤b b≤x ⟪ uaa ,  ch-is-sup ua u<x is-sup fc  ⟫ = 
+            ⟪ uaa , ch-is-sup ua ? is-sup fc  ⟫ 
         chain<ZA : {x : Ordinal } → UnionCF A f mf ay (ZChain.supf zc) x ⊆' UnionCF A f mf ay (ZChain.supf zc) (& A)
-        chain<ZA {x} ux with UChain.uchain (proj2 ux)
-        ... | ch-init _ fc = ⟪ proj1 ux , record { u = UChain.u (proj2 ux) ; u<x = case2 refl ; uchain = ch-init _ fc  } ⟫
-        ... | ch-is-sup is-sup fc = ⟪ proj1 ux , record { u = UChain.u (proj2 ux) ; u<x = case1 u<x ; uchain = UChain.uchain (proj2 ux) } ⟫ where
-            u<A : (& ( * ( ZChain.supf zc (UChain.u (proj2 ux)))))  o< & A
-            u<A = c<→o< (subst (λ k → odef A k ) (sym &iso) (A∋fcs _ f mf fc) )
-            u<x : UChain.u (proj2 ux) o< & A
-            u<x = subst (λ k → k o< & A ) (trans &iso (ChainP.supfu=u is-sup)) u<A
+        chain<ZA {x} ux with proj2 ux
+        ... | ch-init fc = ⟪ proj1 ux , ch-init fc ⟫
+        ... | ch-is-sup u pu<x is-sup fc = ⟪ proj1 ux , ? ⟫ where
+            u<A : (& ( * ( ZChain.supf zc x)))  o< & A
+            u<A = ? -- c<→o< (subst (λ k → odef A k ) (sym &iso) (A∋fcs _ f mf fc) )
+            u<x :  ZChain.supf zc x o< & A
+            u<x = ? -- subst (λ k → k o< & A ) (trans &iso (ChainP.supfu=u is-sup)) ? -- u<A
         is-max-hp : (x : Ordinal) {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
             b o< x → (ab : odef A b) →
             HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) ab f → 
             * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b
         is-max-hp x {a} {b} ua b<x ab has-prev a<b = m04 where
             m04 : odef (UnionCF A f mf ay (ZChain.supf zc) x) b
-            m04 = ⟪ m07   , record { u = UChain.u (proj2 m06) ; u<x = UChain.u<x (proj2 m06) 
-                ; uchain = subst (λ k → Chain A f mf ay (ZChain.supf zc) (UChain.u (proj2 m06)) k) (sym (HasPrev.x=fy has-prev)) m08 } ⟫ where
+            m04 = ⟪ m07   , subst (λ k → UChain A f mf ay (ZChain.supf zc) ? k) (sym (HasPrev.x=fy has-prev)) m08  ⟫ where
                 m06 : odef (UnionCF A f mf ay (ZChain.supf zc) x) (HasPrev.y has-prev )
                 m06 = HasPrev.ay has-prev
                 m07 : odef A b 
                 m07 = subst (λ k → odef A k ) (sym (HasPrev.x=fy has-prev)) (proj2 (mf _ (proj1 m06) ))
-                m08 :  Chain A f mf ay (ZChain.supf zc) (UChain.u (proj2 m06)) (f ( HasPrev.y has-prev ))
+                m08 :  UChain A f mf ay (ZChain.supf zc) ? (f ( HasPrev.y has-prev ))
                 m08 with proj2 m06
-                ... | record { u = _ ; u<x = u<x ; uchain = ch-init .(HasPrev.y has-prev) fc } = 
-                          ch-init (f (HasPrev.y has-prev)) (fsuc _ fc) 
-                ... | record { u = u ; u<x = u<x ; uchain = ch-is-sup is-sup fc } = ch-is-sup (ChainP-next A f mf ay _ is-sup) (fsuc _ fc) 
+                ... | ch-init fc  = 
+                          ch-init (fsuc _ fc) 
+                ... | ch-is-sup u u<x is-sup fc  = ? -- ch-is-sup u u<x (ChainP-next A f mf ay _ is-sup) (fsuc _ fc) 
         zc1 :  (x : Ordinal) →  ((y₁ : Ordinal) → y₁ o< x → ZChain1 A f mf ay zc y₁) → ZChain1 A f mf ay zc x
         zc1 x prev with Oprev-p x
         ... | yes op = record { is-max = is-max ; chain-mono2 = chain-mono2 x ; fcy<sup = ? ; sup=u = ? ; order = ? } where
@@ -482,16 +476,8 @@
                  m01 with trio< b px    --- px  < b < x
                  ... | tri> ¬a ¬b c = ⊥-elim (¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x  ⟫)
                  ... | tri< b<px ¬b ¬c = chain-mono2 x ( o<→≤  (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ))  o≤-refl m04 where
-                    m02 : (UChain.u (proj2 ua) o< px) ∨ (UChain.u (proj2 ua) ≡ o∅)
-                    m02 with UChain.u<x (proj2 ua)
-                    ... | case2 u=0 = case2 u=0
-                    ... | case1 u<x with trio< (UChain.u (proj2 ua))  px
-                    ... | tri< a ¬b ¬c = case1 a
-                    ... | tri> ¬a ¬b c = ⊥-elim (¬p<x<op ⟪ c , subst (λ k → _ o< k ) (sym (Oprev.oprev=x op)) u<x  ⟫) --    u<x px<u
-                    ... | tri≈ ¬a b ¬c = ?  -- u = px case
-                    ---   if u = px, x is sup    px ≡ u < a < b o< x,   b ≡ px ∨ b o< a
                     m03 :  odef (UnionCF A f mf ay (ZChain.supf zc) px) a
-                    m03 = ⟪ proj1 ua , record { u = UChain.u (proj2 ua)  ; u<x = m02 ; uchain = UChain.uchain (proj2 ua) } ⟫
+                    m03 = ⟪ proj1 ua , ? ⟫
                     m04 : odef (UnionCF A f mf ay (ZChain.supf zc) px) b
                     m04 = ZChain1.is-max (prev px px<x) m03 b<px ab 
                          (case2 record {x<sup = λ {z} lt → IsSup.x<sup is-sup (chain-mono2 x ( o<→≤  (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ))  o≤-refl lt)  } ) a<b
@@ -528,7 +514,7 @@
                  m06 = record { fcy<sup = m07 ; csupz = subst (λ k →  FClosure A f k b ) m05 (init ab) ; order = m08 ; y<s = y<s 
                        ; supfu=u = sym m05 }
                  m04 : odef (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) b
-                 m04 = ⟪ ab , record { u = b ; u<x = case1 <-osuc ; uchain = ch-is-sup m06 (subst (λ k → FClosure A f k b) m05 (init ab)) } ⟫
+                 m04 = ⟪ ab , ch-is-sup ? ? m06 (subst (λ k → FClosure A f k b) m05 (init ab))  ⟫
 
      ---
      --- the maximum chain  has fix point of any ≤-monotonic function
@@ -599,19 +585,19 @@
           isupf : Ordinal → Ordinal
           isupf z = y
           cy : odef (UnionCF A f mf ay isupf o∅) y
-          cy = ⟪ ay , record { u = o∅ ; u<x = case2 refl ; uchain = ch-init _ (init ay)  } ⟫
+          cy = ⟪ ay , ch-init ?  ⟫
           isy : {z : Ordinal } → odef (UnionCF A f mf ay isupf o∅) z → * y ≤ * z
-          isy {z} ⟪ az , uz ⟫ with UChain.uchain uz 
-          ... | ch-init z fc = s≤fc y f mf fc 
-          ... | ch-is-sup is-sup fc = ⊥-elim ( <-irr (case1 refl) ( ChainP.fcy<sup is-sup (init ay) ) )
+          isy {z} ⟪ az , uz ⟫ with uz 
+          ... | ch-init fc = s≤fc y f mf fc 
+          ... | ch-is-sup u u<x is-sup fc = ⊥-elim ( <-irr (case1 refl) ( ChainP.fcy<sup is-sup (init ay) ) )
           inext : {a : Ordinal} → odef (UnionCF A f mf ay isupf o∅) a → odef (UnionCF A f mf ay isupf o∅) (f a)
-          inext {a} ua with UChain.uchain (proj2 ua)
-          ... | ch-init a fc = ⟪ proj2 (mf _ (proj1 ua))  , record { u = o∅ ; u<x = case2 refl ; uchain = ch-init _ (fsuc _ fc ) } ⟫
-          ... | ch-is-sup is-sup fc = ⊥-elim ( <-irr (case1 refl) ( ChainP.fcy<sup is-sup (init ay) ) )
+          inext {a} ua with (proj2 ua)
+          ... | ch-init fc = ⟪ proj2 (mf _ (proj1 ua))  , ch-init (fsuc _ fc )  ⟫
+          ... | ch-is-sup u u<x is-sup fc = ⊥-elim ( <-irr (case1 refl) ( ChainP.fcy<sup is-sup (init ay) ) )
           itotal : IsTotalOrderSet (UnionCF A f mf ay isupf o∅) 
           itotal {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 isupf (UChain.uchain (proj2 ca)) (UChain.uchain (proj2 cb)) 
+               uz01 = chain-total A f mf ay isupf (proj2 ca) (proj2 cb) 
           imax : {a b : Ordinal} → odef (UnionCF A f mf ay isupf o∅) a →
             b o< o∅ → (ab : odef A b) →
             HasPrev A (UnionCF A f mf ay isupf o∅) ab f ∨ IsSup A (UnionCF A f mf ay isupf o∅) ab →
@@ -643,25 +629,25 @@
           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) (UChain.uchain (proj2 ca)) (UChain.uchain (proj2 cb)) 
+               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 , ua ⟫ = ⟪ afa , record { u = UChain.u ua ; u<x = UChain.u<x ua ; uchain = fua } ⟫ where
+          pnext {a} ⟪ aa , ua ⟫ = ⟪ afa , fua  ⟫ where
                afa : odef A ( f a )
                afa = proj2 ( mf a aa )
-               fua : Chain A f mf ay (ZChain.supf zc)  (UChain.u ua) (f a)
-               fua with UChain.uchain ua
-               ... | ch-init a fc = ch-init (f a) ( fsuc _ fc )
-               ... | ch-is-sup is-sup fc = ch-is-sup (ChainP-next A f mf ay _ is-sup ) (fsuc _ fc )
+               fua : UChain A f mf ay (ZChain.supf zc)  ? (f a)
+               fua = ? -- with ? 
+               -- ... | ch-init fc = ch-init  ( fsuc _ fc )
+               --- ... | ch-is-sup u is-sup fc = ch-is-sup ? (ChainP-next A f mf ay _ is-sup ) (fsuc _ fc )
           pinit :  {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁
-          pinit {a} ⟪ aa , ua ⟫  with UChain.uchain ua
-          ... | ch-init a fc = s≤fc y f mf fc
-          ... | ch-is-sup is-sup fc = ≤-ftrans (case2 zc7) (s≤fc _ f mf fc)  where
-               zc7 : y << (ZChain.supf zc) (UChain.u ua)
+          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 (case2 zc7) (s≤fc _ f mf fc)  where
+               zc7 : y << (ZChain.supf zc) ? -- (UChain.u ua)
                zc7 = ChainP.fcy<sup is-sup (init ay)
           pcy : odef pchain y
-          pcy = ⟪ ay , record { u =  o∅ ; u<x = case2 refl ; uchain = ch-init _ (init ay)  }  ⟫
+          pcy = ⟪ ay , ch-init (init ay)    ⟫
 
           supf0 = ZChain.supf (prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ))
 
@@ -677,13 +663,13 @@
               sup=u {b} {ab} b<x is-sup with trio< b px
               ... | tri< a ¬b ¬c = ZChain.sup=u zc {b} {ab} a record { x<sup = pc20 } where
                      pc20 : {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op)) z → (z ≡ b) ∨ (z << b)
-                     pc20 {z} ⟪ az , record { u = u0 ; u<x = u<x ; uchain = ch-init _ fc } ⟫ = 
-                         IsSup.x<sup is-sup ⟪ az , record { u = u0 ; u<x = case2 refl  ; uchain = ch-init _ fc } ⟫ 
-                     pc20 {z} ⟪ az , record { u = u0 ; u<x = u<x ; uchain = ch-is-sup is-sup-c fc } ⟫ with u<x 
-                     ... | case2 u=0 = ?
-                     ... | case1 u<px = IsSup.x<sup is-sup ⟪ az , record { u = u0 
-                       ; u<x = case1 (subst (λ k → u0 o< k) (Oprev.oprev=x op) (ordtrans u<px <-osuc))
-                       ; uchain = ch-is-sup is-sup-c fc } ⟫ 
+                     pc20 {z} ⟪ az , ch-init fc  ⟫ = 
+                         IsSup.x<sup is-sup ⟪ az ,  ch-init fc  ⟫ 
+                     pc20 {z} ⟪ az , ch-is-sup u u<x is-sup-c fc  ⟫ = ? -- with u<x 
+                     -- ... | case2 u=0 = ?
+                     -- ... | case1 u<px = IsSup.x<sup is-sup ⟪ az , ch-is-sup
+                     --   (case1 (subst (λ k → ? o< k) (Oprev.oprev=x op) (ordtrans u<px <-osuc)))
+                     --   is-sup-c fc  ⟫ 
               ... | tri≈ ¬a refl ¬c = ?
               ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op))  b<x  ⟫ )
               order : {b sup1 z1 : Ordinal} → b o< x → sup1 o< b → FClosure A f (supf0 sup1) z1 → z1 << supf0 b
@@ -692,17 +678,17 @@
               ... | tri≈ ¬a refl ¬c = ?
               ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op))  b<x  ⟫ )
 
-          chain-x : ( {z : Ordinal} → (az : odef pchain z) → ¬ ( UChain.u (proj2 az) ≡ px  )) → pchain ⊆' UnionCF A f mf ay (ZChain.supf zc) px
-          chain-x ne {z} ⟪ az , record { u = u ; u<x = case2 u=y ; uchain = uc } ⟫ = 
-              ⟪ az , record { u = u ; u<x = case2 u=y ; uchain = uc } ⟫ 
-          chain-x ne {z} ⟪ az , record { u = u ; u<x = case1 u<x ; uchain = ch-init z fc } ⟫ with trio<  o∅ px
-          ... | tri< a ¬b ¬c = ⟪ az , record { u = u ; u<x = case1 a ; uchain = ch-init z fc } ⟫  
-          ... | tri≈ ¬a b ¬c = ⟪ az , record { u = u ; u<x = case2 refl ; uchain = ch-init z fc } ⟫  
-          ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
-          chain-x ne {z} uz@record { proj1 = az ; proj2 =  record { u = u ; u<x = case1 u<x ; uchain = ch-is-sup is-sup fc } } with trio< u px
-          ... | tri< a ¬b ¬c = ⟪ az , record { u = u ; u<x = case1 a ; uchain = ch-is-sup is-sup fc } ⟫ 
-          ... | tri≈ ¬a b ¬c = ⊥-elim ( ne uz  b )
-          ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op))  u<x  ⟫ )
+          -- chain-x : ( {z : Ordinal} → (az : odef pchain z) → ¬ ( (proj2 az) ≡ px  )) → pchain ⊆' UnionCF A f mf ay (ZChain.supf zc) px
+          -- chain-x ne {z} ⟪ az , record { u = u ; u<x = case2 u=y ; uchain = uc } ⟫ = 
+          --     ⟪ az , record { u = u ; u<x = case2 u=y ; uchain = uc } ⟫ 
+          -- chain-x ne {z} ⟪ az , record { u = u ; u<x = case1 u<x ; uchain = ch-init fc } ⟫ with trio<  o∅ px
+          -- ... | tri< a ¬b ¬c = ⟪ az , record { u = u ; u<x = case1 a ; uchain = ch-init fc } ⟫  
+          -- ... | tri≈ ¬a b ¬c = ⟪ az , record { u = u ; u<x = case2 refl ; uchain = ch-init fc } ⟫  
+          -- ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
+          --- chain-x ne {z} uz@record { proj1 = az ; proj2 =  record { u = u ; u<x = case1 u<x ; uchain = ch-is-sup u is-sup fc } } with trio< u px
+          --- ... | tri< a ¬b ¬c = ⟪ az , record { u = u ; u<x = case1 a ; uchain = ch-is-sup u is-sup fc } ⟫ 
+          --- ... | tri≈ ¬a b ¬c = ⊥-elim ( ne uz  b )
+          --- ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op))  u<x  ⟫ )
 
           zc4 : ZChain A f mf ay x 
           zc4 with ODC.∋-p O A (* px)
@@ -739,26 +725,26 @@
           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 psupf0 (UChain.uchain (proj2 ca)) (UChain.uchain (proj2 cb)) 
+               uz01 = chain-total A f mf ay psupf0 ( (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 , ua ⟫ = ⟪ afa , record { u = UChain.u ua ; u<x = UChain.u<x ua ; uchain = fua } ⟫ where
+          pnext {a} ⟪ aa , ua ⟫ = ⟪ afa , fua  ⟫ where
                afa : odef A ( f a )
                afa = proj2 ( mf a aa )
-               fua : Chain A f mf ay psupf0 (UChain.u ua) (f a)
-               fua with UChain.uchain ua
-               ... | ch-init a fc = ch-init (f a) ( fsuc _ fc )
-               ... | ch-is-sup is-sup fc = ch-is-sup (ChainP-next A f mf ay _ is-sup ) (fsuc _ fc )
+               fua : UChain A f mf ay psupf0 ? (f a)
+               fua = ? -- with  ua
+               -- ... | ch-init fc = ch-init  ( fsuc _ fc )
+               --- ... | ch-is-sup u is-sup fc = ch-is-sup u (ChainP-next A f mf ay _ is-sup ) (fsuc _ fc )
           pinit :  {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁
-          pinit {a} ⟪ aa , ua ⟫  with UChain.uchain ua
-          ... | ch-init a fc = s≤fc y f mf fc
-          ... | ch-is-sup is-sup fc = ≤-ftrans (case2 zc7) (s≤fc _ f mf fc)  where
-               zc7 : y << psupf0 (UChain.u ua)
+          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 (case2 zc7) (s≤fc _ f mf fc)  where
+               zc7 : y << psupf0 ?
                zc7 = ChainP.fcy<sup is-sup (init ay)
           pcy : odef pchain y
-          pcy = ⟪ ay , record { u =  o∅ ; u<x = case2 refl ; uchain = ch-init _ (init ay)  }  ⟫
+          pcy = ⟪ ay , ch-init (init ay)    ⟫
 
           no-extension : ZChain A f mf ay x
           no-extension  = record { initial = pinit ; chain∋init = pcy  ; supf = psupf0