Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 947:a028409f5ca2
avoid memory exhaust
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 31 Oct 2022 15:36:58 +0900 |
| parents | 3377379a1479 |
| children | 51556591c879 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 24 insertions(+), 53 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Mon Oct 31 11:28:47 2022 +0900 +++ b/src/zorn.agda Mon Oct 31 15:36:58 2022 +0900 @@ -1522,59 +1522,30 @@ ... | tri≈ ¬a b ¬c = case2 (case1 b) ... | tri> ¬a ¬b c = case2 (case2 c) - not-hasprev : ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) d (cf nmx) - not-hasprev hp = ⊥-elim (z29 {mc} {asc} spd z31 hp ) where - z31 : odef (ZChain.chain zc) (cf nmx d) - z31 = ZChain.f-next zc (subst (λ k → odef (ZChain.chain zc) k) (sym (HasPrev.x=fy hp)) - (ZChain.f-next zc - (chain-mono (cf nmx) (cf-is-≤-monotonic nmx) as0 supf (ZChain.supf-mono zc) (o<→≤ d<A) ( HasPrev.ay hp )))) - z32 : odef (ZChain.chain zc) d - z32 = subst (λ k → odef (ZChain.chain zc) k) (sym (HasPrev.x=fy hp)) - (ZChain.f-next zc - (chain-mono (cf nmx) (cf-is-≤-monotonic nmx) as0 supf (ZChain.supf-mono zc) (o<→≤ d<A) ( HasPrev.ay hp ))) - -- case1 : FClosure of s - -- case2 : u o< supf mc - -- case3 : u ≡ supf mc z31 - -- case4 : supf mc o< u ⊥ ( why ? ) - z29 : {mc : Ordinal } {asc : odef A (supf mc)} (spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc )) - → odef (ZChain.chain zc) (cf nmx (MinSUP.sup spd)) - → HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) (MinSUP.sup spd)) (MinSUP.sup spd) (cf nmx) - → ⊥ - z29 {mc} {asc} spd ⟪ aa , ch-init fc ⟫ hp = ? - z29 {mc} {asc} spd ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ hp = <-irr z26 z30 where - y : Ordinal - y = HasPrev.y hp -- cf nmx y ≡ d1 - zy : odef (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) (MinSUP.sup spd)) y - zy = HasPrev.ay hp - d1 : Ordinal - d1 = MinSUP.sup spd -- supf d1 ≡ d - z45 : (* (cf nmx (cf nmx y)) ≡ * d1) ∨ (* (cf nmx (cf nmx y)) < * d1) → (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1) - z45 p = subst (λ k → (* (cf nmx k) ≡ * d1) ∨ (* (cf nmx k) < * d1)) (sym (HasPrev.x=fy hp)) p - z30 : * d1 < * (cf nmx d1) - z30 = proj1 (cf-is-<-monotonic nmx d1 (MinSUP.asm spd)) - z24 : y << d1 - z24 = subst (λ k → y << k) (sym (HasPrev.x=fy hp)) ( proj1 (cf-is-<-monotonic nmx y (proj1 (HasPrev.ay hp) ) )) - z40 : ( u ≡ supf mc ) → (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1) - z40 eq1 with MinSUP.x<sup spd (subst (λ k → FClosure A (cf nmx) k (cf nmx d1) ) (trans (ChainP.supu=u is-sup) eq1 ) fc ) - ... | case1 eq = case1 (cong (*) eq) - ... | case2 lt = case2 lt - postulate - sc : Ordinal - sc=sc : supf mc ≡ sc - z41 : ( u o< supf mc ) → (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1) - z41 u<sc with MinSUP.x<sup spd {sc} (init asc sc=sc ) - ... | case2 lt = ? -- sc << d1, u o< mc, supf u ≤ sc, spuf u << d1 - ... | case1 eq = ? - z42 : ( supf mc o< u ) → (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1) - z42 sc<u = ? where -- spuf mc o< spuf u, mc o< u, ,l - z44 : ( cf nmx d1 ≡ supf u ) ∨ ( cf nmx d1 << supf u ) - z44 = ChainP.order is-sup (subst (λ k → supf mc o< k ) ? sc<u ) (init ? ? ) - postulate - z26 : (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1) - -- z26 with z43 u (supf mc) - -- ... | case1 lt = z41 lt - -- ... | case2 (case1 eq) = z40 eq - -- ... | case2 (case2 lt) = z42 lt + not-hasprev : ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 supf d) d (cf nmx) + not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-init fc ⟫ ; x=fy = x=fy } = ? + not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-is-sup u u<x is-sup1 fc ⟫; x=fy = x=fy } = ? +-- z29 : {mc d1 : Ordinal } {asc : odef A (supf mc)} (spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc )) +-- → d1 ≡ MinSUP.sup spd +-- → HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 supf d1) d1 (cf nmx) +-- → ⊥ +-- z29 {mc} {asc} spd d1=spd hp with HasPrev.ay hp +-- ... | ⟪ ua1 , ch-init fc ⟫ = ? +-- ... | ⟪ ua1 , ch-is-sup u u<x is-sup1 fc ⟫ = ? +-- y : Ordinal +-- y = HasPrev.y hp +-- d1 : Ordinal +-- d1 = MinSUP.sup spd -- supf d1 ≡ d +-- z45 : (* (cf nmx (cf nmx y)) ≡ * d1) ∨ (* (cf nmx (cf nmx y)) < * d1) → (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1) +-- z45 p = subst (λ k → (* (cf nmx k) ≡ * d1) ∨ (* (cf nmx k) < * d1)) (sym (HasPrev.x=fy hp)) p +-- z30 : * d1 < * (cf nmx d1) +-- z30 = proj1 (cf-is-<-monotonic nmx d1 (MinSUP.asm spd)) +-- z47 : * (cf nmx (cf nmx y)) < * d1 +-- z47 = ? +-- z24 : y << d1 +-- z24 = subst (λ k → y << k) (sym (HasPrev.x=fy hp)) ( proj1 (cf-is-<-monotonic nmx y (proj1 (HasPrev.ay hp) ) )) +-- z46 : (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1) +-- z46 = z45 (case2 z47 ) sd=d : supf d ≡ d sd=d = ZChain.sup=u zc (MinSUP.asm spd) (o<→≤ d<A) ⟪ is-sup , not-hasprev ⟫