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

changeset 960:b7370c39769e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
IsMinSUP< is wrong
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 04 Nov 2022 17:27:12 +0900
parents 1ef03eedd148
children 811135ad1904
files src/zorn.agda
diffstat 1 files changed, 104 insertions(+), 84 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Fri Nov 04 08:17:21 2022 +0900
+++ b/src/zorn.agda	Fri Nov 04 17:27:12 2022 +0900
@@ -244,7 +244,7 @@
 --    field
 --       x≤sup   : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x )
 
-record IsMinSup (A B : HOD) ( f : Ordinal → Ordinal ) {x : Ordinal } (xa : odef A x)     : Set n where
+record IsMinSUP (A B : HOD) ( f : Ordinal → Ordinal ) {x : Ordinal } (xa : odef A x)     : Set n where
    field
       x≤sup   : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x )
       minsup : { sup1 : Ordinal } → odef A sup1 
@@ -409,7 +409,7 @@
    field
       supf :  Ordinal → Ordinal 
       sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z  
-           → IsMinSup A (UnionCF A f mf ay supf b) f ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf b) f b ) → supf b ≡ b 
+           → IsMinSUP A (UnionCF A f mf ay supf b) f ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf b) f b ) → supf b ≡ b 
 
       asupf :  {x : Ordinal } → odef A (supf x)
       supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
@@ -470,15 +470,46 @@
 
    -- ordering is not proved here but in ZChain1 
 
-   -- b o< x → IsMinSup A (UnionCF A f mf ay supf x) ab → IsMinSup A (UnionCF A f mf ay supf b) ab
-   --   is not valid without ¬ HasPrev
+   IsMinSUP→NotHasPrev : {x sp : Ordinal } → odef A sp 
+       → ({y : Ordinal} → odef (UnionCF A f mf ay supf x) y → (y ≡ sp ) ∨ (y << sp ))
+       → ( {a : Ordinal } → a << f a )
+       → ¬ ( HasPrev A (UnionCF A f mf ay supf x) f sp )
+   IsMinSUP→NotHasPrev {x} {sp} asp is-sup <-mono-f hp = ⊥-elim (<-irr ( <=to≤  fsp≤sp) sp<fsp ) where
+       sp<fsp : sp << f sp
+       sp<fsp = <-mono-f 
+       pr = HasPrev.y hp 
+       im00 : f (f pr) <= sp
+       im00 = is-sup ( f-next (f-next (HasPrev.ay hp)))
+       fsp≤sp : f sp <=  sp
+       fsp≤sp = subst (λ k → f k <= sp ) (sym (HasPrev.x=fy hp)) im00
+
+   IsMinSUP< : ( {a : Ordinal } → a << f a )
+       → {b x : Ordinal } → {ab : odef A b}  → x o≤ z → b o< x 
+       → IsMinSUP A (UnionCF A f mf ay supf x) f ab → IsMinSUP A (UnionCF A f mf ay supf b) f ab
+   IsMinSUP< <-mono-f {b} {x} {ab} x≤z b<x record { x≤sup = x≤sup ; minsup = minsup ; not-hp = nhp } 
+     = record { x≤sup = m02 ; minsup = m07 ; not-hp = IsMinSUP→NotHasPrev ab m02 <-mono-f } where
+             m02 : {z : Ordinal} → odef (UnionCF A f mf ay supf b) z → (z ≡ b) ∨ (z << b)
+             m02 {z} uz = x≤sup (chain-mono f mf ay supf supf-mono (o<→≤ b<x) uz) 
+             m10 : {s : Ordinal }  →  (odef A s ) 
+                →  ( {w : Ordinal} → odef (UnionCF A f mf ay supf b) w → (w ≡ s) ∨ (w << s) ) 
+                →    {w : Ordinal} → odef (UnionCF A f mf ay supf x) w → (w ≡ s) ∨ (w << s)
+             m10 {s} as b-is-sup ⟪ aa , ch-init fc ⟫ = ?
+             m10 {s} as b-is-sup ⟪ aa , ch-is-sup u {w} u<x is-sup-z fc ⟫ = m01 where
+                m01 : w <= s
+                m01 with trio< (supf u) (supf b)
+                ... | tri< a ¬b ¬c = b-is-sup ⟪ aa , ch-is-sup u {w} a is-sup-z fc ⟫ 
+                ... | tri≈ ¬a b ¬c = ?
+                ... | tri> ¬a ¬b c = ?
+             m07 :  {s : Ordinal} → odef A s → ({z : Ordinal} →
+                odef (UnionCF A f mf ay supf b) z → (z ≡ s) ∨ (z << s)) → b o≤ s
+             m07 {s} as b-is-sup = minsup as (m10 as b-is-sup )
 
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
         {y : Ordinal} (ay : odef A y)  (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
    supf = ZChain.supf zc
    field
       is-max :  {a b : Ordinal } → (ca : odef (UnionCF A f mf ay supf z) a ) → supf b o< supf z  → (ab : odef A b) 
-          → HasPrev A (UnionCF A f mf ay supf z) f b ∨  IsMinSup A (UnionCF A f mf ay supf b) f ab  
+          → HasPrev A (UnionCF A f mf ay supf z) f b ∨  IsMinSUP A (UnionCF A f mf ay supf b) f ab  
           → * a < * b  → odef ((UnionCF A f mf ay supf z)) b
       order : {b s z1 : Ordinal} → b o< & A → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
 
@@ -653,7 +684,7 @@
            zc-b<x {b} lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) (ZChain.supf-inject zc lt  )
            is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
               ZChain.supf zc b o< ZChain.supf zc x → (ab : odef A b) →
-              HasPrev A (UnionCF A f mf ay supf x) f b  ∨ IsMinSup A (UnionCF A f mf ay supf b) f ab →
+              HasPrev A (UnionCF A f mf ay supf x) f b  ∨ IsMinSUP A (UnionCF A f mf ay supf b) f ab →
               * a < * b → odef (UnionCF A f mf ay supf x) b
            is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P
            is-max {a} {b} ua b<x ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b 
@@ -668,11 +699,11 @@
                     chain-mono1 (o<→≤ b<x) (HasPrev.ay  nhp) ; x=fy = HasPrev.x=fy nhp } )
               m05 : ZChain.supf zc b ≡ b
               m05 =  ZChain.sup=u zc ab (o<→≤ (z09 ab) )
-                      ⟪ record { x≤sup = λ {z} uz → IsMinSup.x≤sup (proj2 is-sup) uz  
+                      ⟪ record { x≤sup = λ {z} uz → IsMinSUP.x≤sup (proj2 is-sup) uz  
                           ; minsup = m07 ; not-hp = m04 }  , m04 ⟫ where
                  m07 :  {s : Ordinal} → odef A s → ({z : Ordinal} →
                      odef (UnionCF A f mf ay (ZChain.supf zc) b) z → (z ≡ s) ∨ (z << s)) → b o≤ s
-                 m07 {s} as s-is-sup = IsMinSup.minsup (proj2 is-sup) as s-is-sup
+                 m07 {s} as s-is-sup = IsMinSUP.minsup (proj2 is-sup) as s-is-sup
               m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b
               m08 {z} fcz = ZChain.fcy<sup zc (o<→≤ b<A) fcz
               m09 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b 
@@ -683,11 +714,11 @@
         ... | no lim = record { is-max = is-max ; order = order }  where
            is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
               ZChain.supf zc b o< ZChain.supf zc x → (ab : odef A b) →
-              HasPrev A (UnionCF A f mf ay supf x) f b  ∨ IsMinSup A (UnionCF A f mf ay supf b) f ab →
+              HasPrev A (UnionCF A f mf ay supf x) f b  ∨ IsMinSUP A (UnionCF A f mf ay supf b) f ab →
               * a < * b → odef (UnionCF A f mf ay supf x) b
            is-max {a} {b} ua sb<sx ab P a<b with ODC.or-exclude O P
            is-max {a} {b} ua sb<sx ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b 
-           is-max {a} {b} ua sb<sx ab P a<b | case2 is-sup with IsMinSup.x≤sup (proj2 is-sup) (init-uchain A f mf ay )
+           is-max {a} {b} ua sb<sx ab P a<b | case2 is-sup with IsMinSUP.x≤sup (proj2 is-sup) (init-uchain A f mf ay )
            ... | case1 b=y = ⟪ subst (λ k → odef A k ) b=y ay , ch-init (subst (λ k → FClosure A f y k ) b=y (init ay refl ))  ⟫
            ... | case2 y<b = ⟪ ab , ch-is-sup b sb<sx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl))  ⟫ where
               m09 : b o< & A
@@ -705,8 +736,8 @@
                  ; x=fy = HasPrev.x=fy nhp } )
               m05 : ZChain.supf zc b ≡ b
               m05 = ZChain.sup=u zc ab (o<→≤  m09)
-                      ⟪ record { x≤sup = λ lt → IsMinSup.x≤sup (proj2 is-sup) lt 
-                         ; minsup = IsMinSup.minsup (proj2 is-sup) ; not-hp = m04 } , m04 ⟫    -- ZChain on x
+                      ⟪ record { x≤sup = λ lt → IsMinSUP.x≤sup (proj2 is-sup) lt 
+                         ; minsup = IsMinSUP.minsup (proj2 is-sup) ; not-hp = m04 } , m04 ⟫    -- ZChain on x
               m06 : ChainP A f mf ay supf b 
               m06 = record { fcy<sup = m07 ;  order = m08 ; supu=u = m05 }
 
@@ -730,7 +761,7 @@
      record xSUP (B : HOD) (f : Ordinal → Ordinal ) (x : Ordinal) : Set n where
         field
            ax : odef A x
-           is-sup : IsMinSup A B f ax
+           is-sup : IsMinSUP A B f ax
 
      --
      -- create all ZChains under o< x
@@ -1215,10 +1246,10 @@
                           zc37 : MinSUP A (UnionCF A f mf ay supf0 z)
                           zc37 = record { sup = ? ; asm = ? ; x≤sup = ? }
                  sup=u : {b : Ordinal} (ab : odef A b) →
-                    b o≤ x → IsMinSup A (UnionCF A f mf ay supf0 b) supf0 ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf0 b) f b ) → supf0 b ≡ b
+                    b o≤ x → IsMinSUP A (UnionCF A f mf ay supf0 b) supf0 ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf0 b) f b ) → supf0 b ≡ b
                  sup=u {b} ab b≤x is-sup with trio< b px
-                 ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) ⟪ record { x≤sup = λ lt → IsMinSup.x≤sup (proj1 is-sup) lt ; minsup = ? } , proj2 is-sup ⟫ 
-                 ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) ⟪ record { x≤sup = λ lt → IsMinSup.x≤sup (proj1 is-sup) lt ; minsup = ? } , proj2 is-sup ⟫ 
+                 ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) ⟪ record { x≤sup = λ lt → IsMinSUP.x≤sup (proj1 is-sup) lt ; minsup = ? } , proj2 is-sup ⟫ 
+                 ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) ⟪ record { x≤sup = λ lt → IsMinSUP.x≤sup (proj1 is-sup) lt ; minsup = ? } , proj2 is-sup ⟫ 
                  ... | tri> ¬a ¬b px<b = zc31 ? where
                      zc30 : x ≡ b
                      zc30 with osuc-≡< b≤x
@@ -1227,7 +1258,7 @@
                      zcsup : xSUP (UnionCF A f mf ay supf0 px) supf0 x 
                      zcsup with zc30
                      ... | refl = record { ax = ab ; is-sup = record { x≤sup = λ {w} lt → 
-                        IsMinSup.x≤sup (proj1 is-sup) ? ; minsup = ? } } 
+                        IsMinSUP.x≤sup (proj1 is-sup) ? ; minsup = ? } } 
                      zc31 : ( (¬ xSUP (UnionCF A f mf ay supf0 px) supf0 x ) ∨  HasPrev A (UnionCF A f mf ay supf0 px) f x ) → supf0 b ≡ b
                      zc31 (case1 ¬sp=x) with zc30
                      ... | refl = ⊥-elim (¬sp=x zcsup )
@@ -1319,7 +1350,7 @@
                      zc8 = ZChain.supf-is-minsup (pzc z a) {!!}
                  ... | tri≈ ¬a b ¬c = {!!}
                  ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z z≤x )) 
-                 sup=u : {b : Ordinal} (ab : odef A b) → b o≤ x → IsMinSup A (UnionCF A f mf ay supf1 b) f ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf1 b) f b ) → supf1 b ≡ b
+                 sup=u : {b : Ordinal} (ab : odef A b) → b o≤ x → IsMinSUP A (UnionCF A f mf ay supf1 b) f ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf1 b) f b ) → supf1 b ≡ b
                  sup=u {z} ab z≤x is-sup with trio< z x
                  ... | tri< a ¬b ¬c = ? -- ZChain.sup=u (pzc (osuc b)  (ob<x lim a))  ab {!!} record { x≤sup = {!!} }
                  ... | tri≈ ¬a b ¬c = {!!} -- ZChain.sup=u (pzc (osuc ?)  ?)  ab {!!} record { x≤sup = {!!} }
@@ -1331,7 +1362,7 @@
           ... | yes ax with ODC.p∨¬p O ( HasPrev A pchain f x  )   
                -- 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 (IsMinSup A pchain f ax )
+          ... | case2 ¬fy<x with ODC.p∨¬p O (IsMinSUP A pchain f ax )
           ... | case1 is-sup = ? -- record { supf = supf1  ; sup=u = {!!} 
                -- ; sup = {!!} ; supf-is-sup = {!!} ; supf-mono = {!!};  asupf = {!!}  } -- 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
@@ -1346,14 +1377,10 @@
      msp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y)  
          → (zc : ZChain A f mf ay x ) 
          → MinSUP A (UnionCF A f mf ay (ZChain.supf zc) x)
-     msp0 f mf {x} ay zc = minsupP (UnionCF A f mf ay (ZChain.supf zc) x) (ZChain.chain⊆A zc) ztotal where
-        ztotal : IsTotalOrderSet (ZChain.chain zc) 
-        ztotal {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)) 
+     msp0 f mf {x} ay zc = minsupP (UnionCF A f mf ay (ZChain.supf zc) x) (ZChain.chain⊆A zc) (ZChain.f-total zc)
 
      fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )  (zc : ZChain A f mf as0 (& A) )
-            → (sp1 : MinSUP A (ZChain.chain zc))   -- & (SUP.sup (sp0 f mf as0 zc  ))
+            → (sp1 : MinSUP A (ZChain.chain zc)) 
             → (ssp<as :  ZChain.supf zc (MinSUP.sup sp1) o< ZChain.supf zc (& A))
             → f (MinSUP.sup sp1)  ≡ MinSUP.sup sp1
      fixpoint f mf zc sp1 ssp<as = z14 where
@@ -1364,49 +1391,41 @@
            asp : odef A sp
            asp = MinSUP.asm sp1
            z10 :  {a b : Ordinal } → (ca : odef chain a ) → supf b o< supf (& A) → (ab : odef A b ) 
-              →  HasPrev A chain f b  ∨  IsMinSup A (UnionCF A f mf ab (ZChain.supf zc) b) f ab
+              →  HasPrev A chain f b  ∨  IsMinSUP A (UnionCF A f mf as0 (ZChain.supf zc) b) f ab
               → * a < * b  → odef chain b
-           z10 = ? -- ZChain1.is-max (SZ1 f mf as0 zc (& A) )
+           z10 = ZChain1.is-max (SZ1 f mf as0 zc (& A) )
            z22 : sp o< & A
            z22 = z09 asp
-           x≤sup : {x : HOD} → chain ∋ x → (& x ≡ sp ) ∨ (x < * sp )
-           x≤sup bz with MinSUP.x≤sup sp1 bz 
-           ... | case1 eq = ?
-           ... | case2 lt = ?
            z12 : odef chain sp
            z12 with o≡? (& s) sp
            ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc )
            ... | no ne = ZChain1.is-max (SZ1 f mf as0 zc (& A)) {& s} {sp} ( ZChain.chain∋init zc ) ssp<as asp
                 (case2 z19 ) z13 where
                z13 :  * (& s) < * sp
-               z13 with x≤sup ( ZChain.chain∋init zc )
-               ... | case1 eq = ⊥-elim ( ne ? )
-               ... | case2 lt = ? -- subst₂ (λ j k → j < k ) (sym *iso) (sym *iso) lt
-               z19 : IsMinSup A (UnionCF A f mf as0 (ZChain.supf zc) sp) f asp
-               z19 = record {   x≤sup = z20 ; minsup = ?  ; not-hp = ? }  where
+               z13 with MinSUP.x≤sup sp1 ( ZChain.chain∋init zc )
+               ... | case1 eq = ⊥-elim ( ne eq )
+               ... | case2 lt = lt -- subst₂ (λ j k → j < k ) (sym *iso) (sym *iso) lt
+               z19 : IsMinSUP A (UnionCF A f mf as0 (ZChain.supf zc) sp) f asp
+               z19 = record {   x≤sup = z20 ; minsup = ?  ; not-hp = ZChain.IsMinSUP→NotHasPrev zc ? z20 ? }  where
                    z20 : {y : Ordinal} → odef (UnionCF A f mf as0 (ZChain.supf zc) sp) y → (y ≡ sp) ∨ (y << sp)
-                   z20 {y} zy with x≤sup (subst (λ k → odef chain k ) (sym &iso) ?)
-                   ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso ? ) -- ( cong (&) y=p ))
-                   ... | case2 y<p = case2 ? -- (subst (λ k → * y < k ) (sym *iso) y<p )
-           ztotal : IsTotalOrderSet (ZChain.chain zc)
-           ztotal {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 as0 supf ( (proj2 ca)) ( (proj2 cb)) 
+                   z20 {y} zy with MinSUP.x≤sup sp1 (subst (λ k → odef chain k ) (sym &iso) (chain-mono f mf as0 supf (ZChain.supf-mono zc) (o<→≤ z22)  zy ))
+                   ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso y=p ) 
+                   ... | case2 y<p = case2 (subst (λ k → * k < _ ) &iso y<p )
            z14 :  f sp ≡ sp
-           z14 with ztotal (subst (λ k → odef chain k) (sym &iso)  (ZChain.f-next zc z12 )) ?
+           z14 with ZChain.f-total zc (subst (λ k → odef chain k) (sym &iso)  (ZChain.f-next zc z12 )) (subst (λ k → odef chain k) (sym &iso) z12 )
            ... | tri< a ¬b ¬c = ⊥-elim z16 where
                z16 : ⊥
                z16 with proj1 (mf (( MinSUP.sup sp1)) ( MinSUP.asm sp1 ))
-               ... | case1 eq = ⊥-elim (¬b (subst₂ (λ j k → j ≡ k ) refl *iso (sym ? ) ))
-               ... | case2 lt = ⊥-elim (¬c (subst₂ (λ j k → k < j ) refl *iso ? ))
-           ... | tri≈ ¬a b ¬c = subst ( λ k → k ≡ (MinSUP.sup sp1) ) &iso ? -- ( cong (&) b )
+               ... | case1 eq = ⊥-elim (¬b (sym eq) ) 
+               ... | case2 lt = ⊥-elim (¬c lt ) 
+           ... | tri≈ ¬a b ¬c = subst₂ (λ j k → j ≡ k ) &iso &iso ( cong (&) b ) 
            ... | tri> ¬a ¬b c = ⊥-elim z17 where
                z15 : (f sp ≡ MinSUP.sup sp1) ∨ (* (f sp) < * (MinSUP.sup sp1) )
-               z15  = ? -- x≤sup (subst (λ k → odef chain k ) (sym &iso) (ZChain.f-next zc z12 ))
+               z15  = MinSUP.x≤sup sp1 (ZChain.f-next zc z12 )
                z17 : ⊥
                z17 with z15
-               ... | case1 eq = ¬b ?
-               ... | case2 lt = ¬a ?
+               ... | case1 eq = ¬b (cong (*) eq)
+               ... | case2 lt = ¬a lt
 
      tri : {n : Level} (u w : Ordinal ) { R : Set n }  → ( u o< w → R ) → ( u ≡  w → R ) → ( w o< u → R ) → R
      tri {_} u w p q r with trio< u w
@@ -1510,9 +1529,6 @@
 
           sc=c : supf mc ≡ mc
           sc=c = ZChain.sup=u zc (MinSUP.asm msp1) (o<→≤ (∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫ )) ⟪ is-sup , not-hasprev ⟫ where
-              is-sup :  IsMinSup A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc) (cf nmx) (MinSUP.asm msp1)
-              is-sup = record { x≤sup = λ zy → MinSUP.x≤sup msp1 (chain-mono (cf nmx) (cf-is-≤-monotonic nmx) as0 supf (ZChain.supf-mono zc) (o<→≤ mc<A) zy )
-                          ; minsup = ? } 
               not-hasprev :  ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc) (cf nmx) mc
               not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-init fc ⟫ ; x=fy = x=fy } = ⊥-elim ( <-irr z31 z30 ) where 
                    z30 : * mc < * (cf nmx mc)
@@ -1529,38 +1545,10 @@
                    z32 = ftrans<=-< z31 (subst (λ k → * mc < * k ) (cong (cf nmx) x=fy) z30 )
                    z48 : ( * (cf nmx (cf nmx y)) ≡ * (supf mc)) ∨ (* (cf nmx (cf nmx y)) < * (supf mc) )
                    z48 = <=to≤ (ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) mc<A u<x (fsuc _ ( fsuc  _ fc )))
+              is-sup :  IsMinSUP A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc) (cf nmx) (MinSUP.asm msp1)
+              is-sup = record { x≤sup = λ zy → MinSUP.x≤sup msp1 (chain-mono (cf nmx) (cf-is-≤-monotonic nmx) as0 supf (ZChain.supf-mono zc) (o<→≤ mc<A) zy )
+                          ; minsup = ? ; not-hp = not-hasprev } 
 
-          is-sup : IsMinSup A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) (cf nmx) (MinSUP.asm spd)
-          is-sup = record { x≤sup = z22 ; minsup = ? } where
-                z23 : {z : Ordinal } → odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc) z → (z ≡ MinSUP.sup spd) ∨ (z << MinSUP.sup spd)
-                z23 lt = MinSUP.x≤sup spd lt
-                z22 :  {y : Ordinal} → odef (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) y →
-                   (y ≡ MinSUP.sup spd) ∨ (y << MinSUP.sup spd)
-                z22 {a} ⟪ aa , ch-init fc ⟫ = case2 ( ( ftrans<=-< z32 ( sc<<d {mc} asc spd ) )) where
-                    z32 : ( a  ≡  supf mc ) ∨ ( * a < * (supf mc) )
-                    z32 = ZChain.fcy<sup zc (o<→≤ mc<A) fc
-                z22 {a} ⟪ aa , ch-is-sup u u<x is-sup1 fc ⟫ = tri u (supf mc)
-                       z60 z61 ( λ sc<u → ⊥-elim ( o≤> ( subst (λ k → k o≤ supf mc) (ChainP.supu=u is-sup1) z51) sc<u )) where
-                    z53 : supf u o< supf (& A)
-                    z53 = ordtrans<-≤ u<x (ZChain.supf-mono zc (o<→≤ d<A) )
-                    z52 : ( u ≡ mc ) ∨  ( u << mc )
-                    z52 = MinSUP.x≤sup msp1 ⟪ subst (λ k → odef A k ) (ChainP.supu=u is-sup1) (A∋fcs _ _ (cf-is-≤-monotonic nmx) fc) 
-                           , ch-is-sup u z53 is-sup1 (init (ZChain.asupf zc)  (ChainP.supu=u is-sup1)) ⟫
-                    z56 : u ≡ mc → supf u ≡  supf mc
-                    z56 eq = cong supf eq
-                    z57 : u << mc → supf u o≤ supf mc
-                    z57 lt = ZChain.supf-<= zc (case2 z58) where
-                        z58 : supf u << supf mc -- supf u o< supf d -- supf u << supf d
-                        z58 = subst₂ ( λ j k → j << k ) (sym (ChainP.supu=u is-sup1)) (sym sc=c)  lt 
-                    z51 : supf u o≤ supf mc
-                    z51 = or z52 (λ le → o≤-refl0 (z56 le) ) z57 
-                    z60 : u o< supf mc → (a ≡ d ) ∨ ( * a < * d )
-                    z60 u<smc = case2 ( ftrans<=-< (ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) mc<A 
-                        (subst (λ k → k o< supf mc) (sym (ChainP.supu=u is-sup1))  u<smc)  fc ) smc<<d )
-                    z61 : u ≡ supf mc → (a ≡ d ) ∨ ( * a < * d )
-                    z61 u=sc = case2 (fsc<<d {mc} asc spd (subst (λ k → FClosure A (cf nmx) k a) (trans (ChainP.supu=u is-sup1) u=sc) fc ) )
-                    -- u<x    : ZChain.supf zc u o< ZChain.supf zc d
-                    --     supf u o< spuf c → order
 
           not-hasprev : ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 supf d) (cf nmx) d
           not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-init fc ⟫ ; x=fy = x=fy } = ⊥-elim ( <-irr z31 z30 ) where 
@@ -1609,6 +1597,38 @@
                 -- ... | case1 eq =  MinSUP.x≤sup spd ( subst₂ (λ j k → FClosure A (cf nmx) j k ) (trans (ChainP.supu=u is-sup1) eq) refl fc )
                 -- ... | case2 lt = z45 (case2 (z47 {mc} {d} {asc} spd (z49 lt) z48 ))
 
+          is-sup : IsMinSUP A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) (cf nmx) (MinSUP.asm spd)
+          is-sup = record { x≤sup = z22 ; minsup = ? ; not-hp = not-hasprev } where
+                z23 : {z : Ordinal } → odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc) z → (z ≡ MinSUP.sup spd) ∨ (z << MinSUP.sup spd)
+                z23 lt = MinSUP.x≤sup spd lt
+                z22 :  {y : Ordinal} → odef (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) y →
+                   (y ≡ MinSUP.sup spd) ∨ (y << MinSUP.sup spd)
+                z22 {a} ⟪ aa , ch-init fc ⟫ = case2 ( ( ftrans<=-< z32 ( sc<<d {mc} asc spd ) )) where
+                    z32 : ( a  ≡  supf mc ) ∨ ( * a < * (supf mc) )
+                    z32 = ZChain.fcy<sup zc (o<→≤ mc<A) fc
+                z22 {a} ⟪ aa , ch-is-sup u u<x is-sup1 fc ⟫ = tri u (supf mc)
+                       z60 z61 ( λ sc<u → ⊥-elim ( o≤> ( subst (λ k → k o≤ supf mc) (ChainP.supu=u is-sup1) z51) sc<u )) where
+                    z53 : supf u o< supf (& A)
+                    z53 = ordtrans<-≤ u<x (ZChain.supf-mono zc (o<→≤ d<A) )
+                    z52 : ( u ≡ mc ) ∨  ( u << mc )
+                    z52 = MinSUP.x≤sup msp1 ⟪ subst (λ k → odef A k ) (ChainP.supu=u is-sup1) (A∋fcs _ _ (cf-is-≤-monotonic nmx) fc) 
+                           , ch-is-sup u z53 is-sup1 (init (ZChain.asupf zc)  (ChainP.supu=u is-sup1)) ⟫
+                    z56 : u ≡ mc → supf u ≡  supf mc
+                    z56 eq = cong supf eq
+                    z57 : u << mc → supf u o≤ supf mc
+                    z57 lt = ZChain.supf-<= zc (case2 z58) where
+                        z58 : supf u << supf mc -- supf u o< supf d -- supf u << supf d
+                        z58 = subst₂ ( λ j k → j << k ) (sym (ChainP.supu=u is-sup1)) (sym sc=c)  lt 
+                    z51 : supf u o≤ supf mc
+                    z51 = or z52 (λ le → o≤-refl0 (z56 le) ) z57 
+                    z60 : u o< supf mc → (a ≡ d ) ∨ ( * a < * d )
+                    z60 u<smc = case2 ( ftrans<=-< (ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) mc<A 
+                        (subst (λ k → k o< supf mc) (sym (ChainP.supu=u is-sup1))  u<smc)  fc ) smc<<d )
+                    z61 : u ≡ supf mc → (a ≡ d ) ∨ ( * a < * d )
+                    z61 u=sc = case2 (fsc<<d {mc} asc spd (subst (λ k → FClosure A (cf nmx) k a) (trans (ChainP.supu=u is-sup1) u=sc) fc ) )
+                    -- u<x    : ZChain.supf zc u o< ZChain.supf zc d
+                    --     supf u o< spuf c → order
+
           sd=d : supf d ≡ d
           sd=d = ZChain.sup=u zc (MinSUP.asm spd) (o<→≤ d<A) ⟪ is-sup , not-hasprev ⟫