Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 975:1e88cce74699
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 08 Nov 2022 11:26:59 +0900 |
| parents | 9bfe54cd9fb9 |
| children | 8fe873f0c88e |
| files | src/zorn.agda |
| diffstat | 1 files changed, 49 insertions(+), 232 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Mon Nov 07 22:01:54 2022 +0900 +++ b/src/zorn.agda Tue Nov 08 11:26:59 2022 +0900 @@ -418,7 +418,7 @@ minsup : {x : Ordinal } → x o≤ z → MinSUP A (UnionCF A f mf ay supf x) supf-is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ MinSUP.sup ( minsup x≤z ) - csupf : {b : Ordinal } → supf b o< z → odef (UnionCF A f mf ay supf z) (supf b) -- supf z is not an element of this chain + csupf : {b : Ordinal } → supf b o< supf z → odef (UnionCF A f mf ay supf z) (supf b) -- supf z is not an element of this chain chain : HOD chain = UnionCF A f mf ay supf z @@ -666,7 +666,7 @@ s<z : s o< & A s<z = ordtrans s<b b<z zc04 : odef (UnionCF A f mf ay supf (& A)) (supf s) - zc04 = ZChain.csupf zc (z09 (ZChain.asupf zc)) + zc04 = ZChain.csupf zc (ordtrans<-≤ ss<sb (ZChain.supf-mono zc (o<→≤ b<z) )) zc05 : odef (UnionCF A f mf ay supf b) (supf s) zc05 with zc04 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ @@ -896,7 +896,7 @@ zc41 : ZChain A f mf ay x zc41 with zc43 x zc41 | (case2 sp≤x ) = record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono ; supf-< = ? - ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = csupf1 } where + ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = ? } where -- supf0 px is included in the chain of sp1 -- supf0 px ≡ px ∧ supf0 px o< sp1 → ( UnionCF A f mf ay supf0 px ∪ FClosure (supf0 px) ) ≡ UnionCF supf1 x -- else UnionCF A f mf ay supf0 px ≡ UnionCF supf1 x @@ -1006,7 +1006,7 @@ ... | tri< sf0px<px ¬b ¬c = cp3 ( subst ( λ k → FClosure A f k z) (trans (trans (sf1=sf0 u<x0) eq) (ZChain.supfmax zc px<x) ) fc) where cp3 : {z : Ordinal } → FClosure A f (supf0 px) z → odef (UnionCF A f mf ay supf0 x) z - cp3 (init uz refl) = chain-mono f mf ay supf0 (ZChain.supf-mono zc) (o<→≤ px<x) (ZChain.csupf zc sf0px<px) + cp3 (init uz refl) = chain-mono f mf ay supf0 (ZChain.supf-mono zc) (o<→≤ px<x) (ZChain.csupf zc ?) -- sf0px<px) cp3 (fsuc uz fc) = ZChain.f-next zc (cp3 fc) ... | tri≈ ¬a b ¬c = ⊥-elim (ne b) ... | tri> ¬a ¬b px<sf0px = ⊥-elim (¬p<x<op ⟪ cp5 , cp4 ⟫ ) where @@ -1127,7 +1127,7 @@ zc17 : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 px → FClosure A f (supf1 s) z1 → (z1 ≡ supf1 px) ∨ (z1 << supf1 px) zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k )) mins-is-spx - (MinSUP.x≤sup mins (csupf17 (fcup fc (o<→≤ s<px) )) ) where + (MinSUP.x≤sup mins (zc28 (fcup fc (o<→≤ s<px) )) ) where mins : MinSUP A (UnionCF A f mf ay supf0 px) mins = ZChain.minsup zc o≤-refl mins-is-spx : MinSUP.sup mins ≡ supf1 px @@ -1136,9 +1136,9 @@ s<px = supf-inject0 supf1-mono ss<spx sf<px : supf0 s o< px sf<px = subst₂ (λ j k → j o< k ) (sf1=sf0 (o<→≤ s<px)) (trans (sf1=sf0 o≤-refl) (sfpx=px)) ss<spx - csupf17 : {z1 : Ordinal } → FClosure A f (supf0 s) z1 → odef (UnionCF A f mf ay supf0 px) z1 - csupf17 (init as refl ) = ZChain.csupf zc sf<px - csupf17 (fsuc x fc) = ZChain.f-next zc (csupf17 fc) + zc28 : {z1 : Ordinal } → FClosure A f (supf0 s) z1 → odef (UnionCF A f mf ay supf0 px) z1 + zc28 (init as refl ) = ZChain.csupf zc ? -- sf<px + zc28 (fsuc x fc) = ZChain.f-next zc (zc28 fc) record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where @@ -1181,63 +1181,13 @@ fcy<sup {z} fc with trio< z1 px ... | tri< a ¬b ¬c = ZChain.fcy<sup zc (o<→≤ a) fc ... | tri≈ ¬a b ¬c = ZChain.fcy<sup zc (o≤-refl0 b) fc - ... | tri> ¬a ¬b c = MinSUP.x≤sup sup1 (case1 ⟪ A∋fc _ fc , ch-init fc ⟫) + ... | tri> ¬a ¬b c = MinSUP.x≤sup sup1 (case1 ⟪ A∋fc _ f mf fc , ch-init fc ⟫) order : {s w : Ordinal} → (lt : supf1 s o< supf1 z1) → FClosure A f (supf1 s ) w → (w ≡ supf1 z1 ) ∨ ( w << supf1 z1 ) - order {s} {z1} lt fc with trio< z1 px - ... | tri< a ¬b ¬c = ? + order {s} {w} lt fc with trio< z1 px + ... | tri< a ¬b ¬c = subst (λ k → w <= k ) ? ( MinSUP.x≤sup (ZChain.minsup zc ?) ? ) ... | tri≈ ¬a b ¬c = ? - ... | tri> ¬a ¬b c = MinSUP.x≤sup sup1 ? + ... | tri> ¬a ¬b c = <=-trans ( MinSUP.x≤sup sup1 ?) ? - csupf1 : {z1 : Ordinal } → supf1 z1 o< x → odef (UnionCF A f mf ay supf1 x) (supf1 z1) - csupf1 {z1} sz1<x = csupf2 where - -- z1 o< px → supf1 z1 ≡ supf0 z1 - -- z1 ≡ px , supf0 px o< px .. px o< z1, x o≤ z1 ... supf1 z1 ≡ sp1 - -- z1 ≡ px , supf0 px ≡ px - psz1≤px : supf1 z1 o≤ px - psz1≤px = subst (λ k → supf1 z1 o< k ) (sym opx=x) sz1<x - csupf2 : odef (UnionCF A f mf ay supf1 x) (supf1 z1) - csupf2 with 3cases - ... | case2 (case2 p) with trio< z1 px | inspect supf1 z1 - ... | tri< a ¬b ¬c | record { eq = eq1 } with osuc-≡< psz1≤px - ... | case2 lt = zc12 (proj1 p) (proj2 p) (case1 cs03) where - cs03 : odef (UnionCF A f mf ay supf0 px) (supf0 z1) - cs03 = ZChain.csupf zc (subst (λ k → k o< px) (sf1=sf0 (o<→≤ a)) lt ) - ... | case1 sfz=px with osuc-≡< ( supf1-mono (o<→≤ a) ) - ... | case1 sfz=sfpx = zc12 (proj1 p) (proj2 p) (case2 (init (ZChain.asupf zc) cs04 )) where - cs04 : supf0 px ≡ supf0 z1 - cs04 = begin - supf0 px ≡⟨ sym (sf1=sf0 o≤-refl) ⟩ - supf1 px ≡⟨ sym sfz=sfpx ⟩ - supf1 z1 ≡⟨ sf1=sf0 (o<→≤ a) ⟩ - supf0 z1 ∎ where open ≡-Reasoning - ... | case2 sfz<sfpx = ⊥-elim ( ¬p<x<op ⟪ cs05 , cs06 ⟫ ) where - --- supf1 z1 ≡ px , z1 o< px , px ≡ supf0 z1 o< supf0 px o< x - cs05 : px o< supf0 px - cs05 = subst₂ ( λ j k → j o< k ) sfz=px (sf1=sf0 o≤-refl ) sfz<sfpx - cs06 : supf0 px o< osuc px - cs06 = subst₂ (λ j k → j o< k ) (sym (proj1 p)) (sym opx=x) px<x - csupf2 | case2 (case2 p) | tri≈ ¬a b ¬c | record { eq = eq1 } = zc12 (proj1 p) (proj2 p) - (case2 (init (ZChain.asupf zc) (cong supf0 (sym b)))) - csupf2 | case2 (case2 p) | tri> ¬a ¬b px<z1 | record { eq = eq1 } = ⊥-elim ( ¬p<x<op ⟪ cs08 , cs09 ⟫ ) where - cs08 : px o< sp1 - cs08 = subst (λ k → k o< sp1 ) (proj1 p) (proj2 p ) - cs09 : sp1 o< osuc px - cs09 = subst ( λ k → sp1 o< k ) (sym (Oprev.oprev=x op)) sz1<x - csupf2 | case2 (case1 p) with trio< (supf0 px) sp1 -- ¬ (supf0 px o< sp1 -- sp1 o≤ spuf0 px) - ... | tri< a ¬b ¬c = ⊥-elim (p a) - ... | tri≈ ¬a b ¬c = ? - ... | tri> ¬a ¬b c = ⊥-elim ( o≤> sfpx≤sp1 c ) - csupf2 | case1 p with trio< (supf0 px) px -- ¬ (supf0 px ≡ px ) - ... | tri< sf0px<px ¬b ¬c = ? where - cs10 : odef (UnionCF A f mf ay supf0 px) (supf0 px) - cs10 = ZChain.csupf zc sf0px<px - ... | tri≈ ¬a b ¬c = ⊥-elim (p b) - ... | tri> ¬a ¬b px<sf0px = ? where - cs11 : px o< z1 → odef (UnionCF A f mf ay supf1 x) (supf1 z1) - cs11 px<z1 = ⊥-elim ( ¬p<x<op ⟪ px<sf0px , subst₂ (λ j k → j o< k ) refl (sym (Oprev.oprev=x op)) - (ordtrans≤-< (subst (λ k → supf0 px o< k) (cong osuc (sym (sf1=sp1 px<z1 ))) sfpx≤sp1 ) sz1<x) ⟫ ) - cs12 : z1 o≤ px → odef (UnionCF A f mf ay supf1 x) (supf1 z1) - cs12 = ? zc41 | (case1 x<sp ) = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ? @@ -1591,35 +1541,44 @@ -- z04 : (nmx : ¬ Maximal A ) → (zc : ZChain A (cf nmx) (cf-is-≤-monotonic nmx) as0 (& A)) → ⊥ - z04 nmx zc = <-irr0 {* (cf nmx c)} {* c} - (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (MinSUP.asm msp1 )))) - (subst (λ k → odef A k) (sym &iso) (MinSUP.asm msp1) ) - (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc msp1 ss<sa ))) -- x ≡ f x ̄ - (proj1 (cf-is-<-monotonic nmx c (MinSUP.asm msp1 ))) where -- x < f x + z04 nmx zc = <-irr0 {* (cf nmx a)} {* a} + (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (MinSUP.asm asup )))) + (subst (λ k → odef A k) (sym &iso) (MinSUP.asm asup) ) + (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc asup sa<sa ))) -- x ≡ f x ̄ + (proj1 (cf-is-<-monotonic nmx a (MinSUP.asm asup ))) where -- x < f x supf = ZChain.supf zc - msp1 : MinSUP A (ZChain.chain zc) - msp1 = msp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc + asup : MinSUP A (ZChain.chain zc) + asup = msp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc + a : Ordinal + a = MinSUP.sup asup + a<A : a o< & A + a<A = ∈∧P→o< ⟪ MinSUP.asm asup , lift true ⟫ + + csup : MinSUP A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 supf a) + csup = ZChain.minsup zc (o<→≤ a<A) c : Ordinal - c = MinSUP.sup msp1 - mc = c - mc<A : mc o< & A - mc<A = ∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫ - c=mc : c ≡ mc - c=mc = refl - z20 : mc << cf nmx mc - z20 = proj1 (cf-is-<-monotonic nmx mc (MinSUP.asm msp1) ) - asc : odef A (supf mc) - asc = ZChain.asupf zc - spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc ) - spd = ysup (cf nmx) (cf-is-≤-monotonic nmx) asc - d = MinSUP.sup spd + c = MinSUP.sup csup + ac : odef A c + ac = ? + sfc=c : supf a ≡ c + sfc=c = ZChain.supf-is-minsup zc (o<→≤ a<A) + c<A : c o< & A + c<A = ∈∧P→o< ⟪ MinSUP.asm csup , lift true ⟫ + + dsup : MinSUP A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 supf c) + dsup = ZChain.minsup zc (o<→≤ c<A) + d : Ordinal + d = MinSUP.sup dsup + ad : odef A d + ad = ? + sfc=d : supf c ≡ d + sfc=d = ZChain.supf-is-minsup zc (o<→≤ c<A) d<A : d o< & A - d<A = ∈∧P→o< ⟪ MinSUP.asm spd , lift true ⟫ - msup : MinSUP A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 supf d) - msup = ZChain.minsup zc (o<→≤ d<A) - sd=ms : supf d ≡ MinSUP.sup ( ZChain.minsup zc (o<→≤ d<A) ) - sd=ms = ZChain.supf-is-minsup zc (o<→≤ d<A) + d<A = ∈∧P→o< ⟪ MinSUP.asm dsup , lift true ⟫ + + zc40 : uchain (cf nmx) (cf-is-≤-monotonic nmx) ac ⊆' UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 supf d + zc40 = ? sc<<d : {mc : Ordinal } → (asc : odef A (supf mc)) → (spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc )) → supf mc << MinSUP.sup spd @@ -1644,152 +1603,10 @@ ... | case1 eq1 = case1 (cong (*) (trans (cong (cf nmx) (sym eq)) eq1) ) ... | case2 lt = case2 (subst (λ k → * k < * d1 ) (cong (cf nmx) eq) lt) - fsc<<d : {mc z : Ordinal } → (asc : odef A (supf mc)) → (spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc )) - → (fc : FClosure A (cf nmx) (supf mc) z) → z << MinSUP.sup spd - fsc<<d {mc} {z} asc spd fc = z25 where - d1 : Ordinal - d1 = MinSUP.sup spd -- supf d1 ≡ d - z24 : (z ≡ d1) ∨ ( z << d1 ) - z24 = MinSUP.x≤sup spd fc - -- - -- f ( f .. ( supf mc ) <= d1 - -- f d1 <= d1 - -- - z25 : z << d1 - z25 with z24 - ... | case2 lt = lt - ... | case1 eq = ⊥-elim ( <-irr z29 (proj1 (cf-is-<-monotonic nmx d1 (MinSUP.asm spd)) ) ) where - -- supf mc ≡ d1 - z32 : ((cf nmx z) ≡ d1) ∨ ( (cf nmx z) << d1 ) - z32 = MinSUP.x≤sup spd (fsuc _ fc) - z29 : (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1) - z29 with z32 - ... | case1 eq1 = case1 (cong (*) (trans (cong (cf nmx) (sym eq)) eq1) ) - ... | case2 lt = case2 (subst (λ k → * k < * d1 ) (cong (cf nmx) eq) lt) - - smc<<d : supf mc << d - smc<<d = sc<<d asc spd - - sz<<c : {z : Ordinal } → z o< & A → supf z <= mc - sz<<c z<A = MinSUP.x≤sup msp1 (ZChain.csupf zc (z09 (ZChain.asupf zc) )) - - 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 - 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) - z30 = proj1 (cf-is-<-monotonic nmx mc (MinSUP.asm msp1)) - z31 : ( * (cf nmx mc) ≡ * mc ) ∨ ( * (cf nmx mc) < * mc ) - z31 = <=to≤ ( MinSUP.x≤sup msp1 (subst (λ k → odef (ZChain.chain zc) (cf nmx k)) (sym x=fy) - ⟪ proj2 (cf-is-≤-monotonic nmx _ (proj2 (cf-is-≤-monotonic nmx _ ua1 ) )) , ch-init (fsuc _ (fsuc _ fc)) ⟫ )) - not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-is-sup u u<x is-sup1 fc ⟫; x=fy = x=fy } = ⊥-elim ( <-irr z48 z32 ) where - z30 : * mc < * (cf nmx mc) - z30 = proj1 (cf-is-<-monotonic nmx mc (MinSUP.asm msp1)) - z31 : ( supf mc ≡ mc ) ∨ ( * (supf mc) < * mc ) - z31 = MinSUP.x≤sup msp1 (ZChain.csupf zc (z09 (ZChain.asupf zc) )) - z32 : * (supf mc) < * (cf nmx (cf nmx y)) - 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 : IsSUP A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc) (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 ) } - + -- supf a ≡ c o< d ≡ supf c o≤ supf (& A) - 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 - z30 : * d < * (cf nmx d) - z30 = proj1 (cf-is-<-monotonic nmx d (MinSUP.asm spd)) - z32 : ( cf nmx (cf nmx y) ≡ supf mc ) ∨ ( * (cf nmx (cf nmx y)) < * (supf mc) ) - z32 = ZChain.fcy<sup zc (o<→≤ mc<A) (fsuc _ (fsuc _ fc)) - z31 : ( * (cf nmx d) ≡ * d ) ∨ ( * (cf nmx d) < * d ) - z31 = case2 ( subst (λ k → * (cf nmx k) < * d ) (sym x=fy) ( ftrans<=-< z32 ( sc<<d {mc} asc spd ) )) - not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-is-sup u u<x is-sup1 fc ⟫; x=fy = x=fy } = ⊥-elim ( <-irr z46 z30 ) where - z45 : (* (cf nmx (cf nmx y)) ≡ * d) ∨ (* (cf nmx (cf nmx y)) < * d) → (* (cf nmx d) ≡ * d) ∨ (* (cf nmx d) < * d) - z45 p = subst (λ k → (* (cf nmx k) ≡ * d) ∨ (* (cf nmx k) < * d)) (sym x=fy) p - z48 : supf mc << d - z48 = sc<<d {mc} asc spd - 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)) ⟫ - z51 : supf u o≤ supf mc - z51 = or z52 (λ le → o≤-refl0 (z56 le) ) z57 where - 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 - z49 : supf u o< supf mc → (cf nmx (cf nmx y) ≡ supf mc) ∨ (* (cf nmx (cf nmx y)) < * (supf mc) ) - z49 su<smc = ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) mc<A su<smc (fsuc _ ( fsuc _ fc )) - z50 : (cf nmx (cf nmx y) ≡ supf d) ∨ (* (cf nmx (cf nmx y)) < * (supf d) ) - z50 = ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) d<A u<x (fsuc _ ( fsuc _ fc )) - z47 : {mc d1 : Ordinal } {asc : odef A (supf mc)} (spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc )) - → (cf nmx (cf nmx y) ≡ supf mc) ∨ (* (cf nmx (cf nmx y)) < * (supf mc) ) → supf mc << d1 - → * (cf nmx (cf nmx y)) < * d1 - z47 {mc} {d1} {asc} spd (case1 eq) smc<d = subst (λ k → k < * d1 ) (sym (cong (*) eq)) smc<d - z47 {mc} {d1} {asc} spd (case2 lt) smc<d = IsStrictPartialOrder.trans PO lt smc<d - z30 : * d < * (cf nmx d) - z30 = proj1 (cf-is-<-monotonic nmx d (MinSUP.asm spd)) - z46 : (* (cf nmx d) ≡ * d) ∨ (* (cf nmx d) < * d) - z46 = or (osuc-≡< z51) z55 z54 where - z55 : supf u ≡ supf mc → (* (cf nmx d) ≡ * d) ∨ (* (cf nmx d) < * d) - z55 eq = <=to≤ (MinSUP.x≤sup spd ( subst₂ (λ j k → FClosure A (cf nmx) j (cf nmx k) ) eq (sym x=fy ) (fsuc _ (fsuc _ fc)) ) ) - z54 : supf u o< supf mc → (* (cf nmx d) ≡ * d) ∨ (* (cf nmx d) < * d) - z54 lt = z45 (case2 (z47 {mc} {d} {asc} spd (z49 lt) z48 )) - -- z46 with osuc-≡< z51 - -- ... | 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 : IsSUP A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) (MinSUP.asm spd) - is-sup = record { x≤sup = z22 } 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 ⟫ - - sc<sd : {mc d : Ordinal } → supf mc << supf d → supf mc o< supf d - sc<sd {mc} {d} sc<<sd with osuc-≡< ( ZChain.supf-<= zc (case2 sc<<sd ) ) - ... | case1 eq = ⊥-elim ( <-irr (case1 (cong (*) (sym eq) )) sc<<sd ) - ... | case2 lt = lt - - sms<sa : supf mc o< supf (& A) - sms<sa with osuc-≡< ( ZChain.supf-mono zc (o<→≤ ( ∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫) )) - ... | case2 lt = lt - ... | case1 eq = ⊥-elim ( o<¬≡ eq ( ordtrans<-≤ (sc<sd (subst (λ k → supf mc << k ) (sym sd=d) (sc<<d {mc} asc spd)) ) - ( ZChain.supf-mono zc (o<→≤ d<A )))) - - ss<sa : supf c o< supf (& A) - ss<sa = subst (λ k → supf k o< supf (& A)) (sym c=mc) sms<sa + sa<sa : supf a o< supf (& A) + sa<sa = ? zorn00 : Maximal A zorn00 with is-o∅ ( & HasMaximal ) -- we have no Level (suc n) LEM