Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 940:aee83a7f9f57
not-hasprev z29 and z31 cause memory exhaust
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 29 Oct 2022 13:55:18 +0900 |
| parents | 187594116449 |
| children | 6f342473f298 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 35 insertions(+), 27 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Fri Oct 28 19:16:34 2022 +0900 +++ b/src/zorn.agda Sat Oct 29 13:55:18 2022 +0900 @@ -1440,31 +1440,6 @@ sd=ms : supf d ≡ MinSUP.sup ( ZChain.minsup zc (o<→≤ d<A) ) sd=ms = ZChain.supf-is-minsup zc (o<→≤ d<A) - 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 ⟫ = ? - z22 {a} ⟪ aa , ch-is-sup u u<x is-sup 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 (ZChain.supf zc) d) d (cf nmx) - not-hasprev hp = ? where - y : Ordinal - y = HasPrev.y hp - z24 : y << d - z24 = subst (λ k → y << k) (sym (HasPrev.x=fy hp)) ( proj1 (cf-is-<-monotonic nmx y (proj1 (HasPrev.ay hp) ) )) - z25 : odef (ZChain.chain zc) (cf nmx d) - z25 = 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 )))) - - sd=d : supf d ≡ d - sd=d = ZChain.sup=u zc (MinSUP.asm spd) (o<→≤ d<A) ⟪ is-sup , not-hasprev ⟫ - 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 sc<<d {mc} {asc} spd = z25 where @@ -1472,8 +1447,6 @@ d1 = MinSUP.sup spd -- supf d1 ≡ d z24 : (supf mc ≡ d1) ∨ ( supf mc << d1 ) z24 = MinSUP.x<sup spd (init asc refl) - z28 : supf mc o< & A - z28 = z09 (ZChain.asupf zc) -- -- f ( f .. ( supf mc ) <= d1 -- f d1 <= d1 @@ -1490,6 +1463,41 @@ ... | case1 eq1 = case1 (cong (*) (trans (cong (cf nmx) (sym eq)) eq1) ) ... | case2 lt = case2 (subst (λ k → * k < * d1 ) (cong (cf nmx) eq) lt) + 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 ⟫ = ? + z22 {a} ⟪ aa , ch-is-sup u u<x is-sup 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 (ZChain.supf zc) d) d (cf nmx) + not-hasprev hp = ⊥-elim ( <-irr ? z30 ) where + y : Ordinal + y = HasPrev.y hp + -- z31 : odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc) (cf nmx d) + -- z31 = ? + -- z29 : {mc : Ordinal } {asc : odef A (supf mc)} (spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc )) + -- → odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc) (cf nmx (MinSUP.sup spd)) + -- → (* (cf nmx (MinSUP.sup spd)) ≡ * (MinSUP.sup spd)) ∨ (* (cf nmx (MinSUP.sup spd)) < * (MinSUP.sup spd)) + -- z29 {mc} {asc} spd afd with MinSUP.x<sup spd afd + -- ... | case1 eq = ? + -- ... | case2 lt = ? + z30 : * d < * (cf nmx d) + z30 = ? + z24 : y << d + z24 = subst (λ k → y << k) (sym (HasPrev.x=fy hp)) ( proj1 (cf-is-<-monotonic nmx y (proj1 (HasPrev.ay hp) ) )) + z25 : odef (ZChain.chain zc) (cf nmx d) + z25 = 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 )))) + + 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 )