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

comparison src/zorn.agda @ 947:a028409f5ca2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
comparison
equal deleted inserted replaced
946:3377379a1479 947:a028409f5ca2
1520 z43 u w with trio< u w 1520 z43 u w with trio< u w
1521 ... | tri< a ¬b ¬c = case1 a 1521 ... | tri< a ¬b ¬c = case1 a
1522 ... | tri≈ ¬a b ¬c = case2 (case1 b) 1522 ... | tri≈ ¬a b ¬c = case2 (case1 b)
1523 ... | tri> ¬a ¬b c = case2 (case2 c) 1523 ... | tri> ¬a ¬b c = case2 (case2 c)
1524 1524
1525 not-hasprev : ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) d (cf nmx) 1525 not-hasprev : ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 supf d) d (cf nmx)
1526 not-hasprev hp = ⊥-elim (z29 {mc} {asc} spd z31 hp ) where 1526 not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-init fc ⟫ ; x=fy = x=fy } = ?
1527 z31 : odef (ZChain.chain zc) (cf nmx d) 1527 not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-is-sup u u<x is-sup1 fc ⟫; x=fy = x=fy } = ?
1528 z31 = ZChain.f-next zc (subst (λ k → odef (ZChain.chain zc) k) (sym (HasPrev.x=fy hp)) 1528 -- z29 : {mc d1 : Ordinal } {asc : odef A (supf mc)} (spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc ))
1529 (ZChain.f-next zc 1529 -- → d1 ≡ MinSUP.sup spd
1530 (chain-mono (cf nmx) (cf-is-≤-monotonic nmx) as0 supf (ZChain.supf-mono zc) (o<→≤ d<A) ( HasPrev.ay hp )))) 1530 -- → HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 supf d1) d1 (cf nmx)
1531 z32 : odef (ZChain.chain zc) d 1531 -- → ⊥
1532 z32 = subst (λ k → odef (ZChain.chain zc) k) (sym (HasPrev.x=fy hp)) 1532 -- z29 {mc} {asc} spd d1=spd hp with HasPrev.ay hp
1533 (ZChain.f-next zc 1533 -- ... | ⟪ ua1 , ch-init fc ⟫ = ?
1534 (chain-mono (cf nmx) (cf-is-≤-monotonic nmx) as0 supf (ZChain.supf-mono zc) (o<→≤ d<A) ( HasPrev.ay hp ))) 1534 -- ... | ⟪ ua1 , ch-is-sup u u<x is-sup1 fc ⟫ = ?
1535 -- case1 : FClosure of s 1535 -- y : Ordinal
1536 -- case2 : u o< supf mc 1536 -- y = HasPrev.y hp
1537 -- case3 : u ≡ supf mc z31 1537 -- d1 : Ordinal
1538 -- case4 : supf mc o< u ⊥ ( why ? ) 1538 -- d1 = MinSUP.sup spd -- supf d1 ≡ d
1539 z29 : {mc : Ordinal } {asc : odef A (supf mc)} (spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc )) 1539 -- z45 : (* (cf nmx (cf nmx y)) ≡ * d1) ∨ (* (cf nmx (cf nmx y)) < * d1) → (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1)
1540 → odef (ZChain.chain zc) (cf nmx (MinSUP.sup spd)) 1540 -- z45 p = subst (λ k → (* (cf nmx k) ≡ * d1) ∨ (* (cf nmx k) < * d1)) (sym (HasPrev.x=fy hp)) p
1541 → HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) (MinSUP.sup spd)) (MinSUP.sup spd) (cf nmx) 1541 -- z30 : * d1 < * (cf nmx d1)
1542 → ⊥ 1542 -- z30 = proj1 (cf-is-<-monotonic nmx d1 (MinSUP.asm spd))
1543 z29 {mc} {asc} spd ⟪ aa , ch-init fc ⟫ hp = ? 1543 -- z47 : * (cf nmx (cf nmx y)) < * d1
1544 z29 {mc} {asc} spd ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ hp = <-irr z26 z30 where 1544 -- z47 = ?
1545 y : Ordinal 1545 -- z24 : y << d1
1546 y = HasPrev.y hp -- cf nmx y ≡ d1 1546 -- z24 = subst (λ k → y << k) (sym (HasPrev.x=fy hp)) ( proj1 (cf-is-<-monotonic nmx y (proj1 (HasPrev.ay hp) ) ))
1547 zy : odef (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) (MinSUP.sup spd)) y 1547 -- z46 : (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1)
1548 zy = HasPrev.ay hp 1548 -- z46 = z45 (case2 z47 )
1549 d1 : Ordinal
1550 d1 = MinSUP.sup spd -- supf d1 ≡ d
1551 z45 : (* (cf nmx (cf nmx y)) ≡ * d1) ∨ (* (cf nmx (cf nmx y)) < * d1) → (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1)
1552 z45 p = subst (λ k → (* (cf nmx k) ≡ * d1) ∨ (* (cf nmx k) < * d1)) (sym (HasPrev.x=fy hp)) p
1553 z30 : * d1 < * (cf nmx d1)
1554 z30 = proj1 (cf-is-<-monotonic nmx d1 (MinSUP.asm spd))
1555 z24 : y << d1
1556 z24 = subst (λ k → y << k) (sym (HasPrev.x=fy hp)) ( proj1 (cf-is-<-monotonic nmx y (proj1 (HasPrev.ay hp) ) ))
1557 z40 : ( u ≡ supf mc ) → (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1)
1558 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 )
1559 ... | case1 eq = case1 (cong (*) eq)
1560 ... | case2 lt = case2 lt
1561 postulate
1562 sc : Ordinal
1563 sc=sc : supf mc ≡ sc
1564 z41 : ( u o< supf mc ) → (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1)
1565 z41 u<sc with MinSUP.x<sup spd {sc} (init asc sc=sc )
1566 ... | case2 lt = ? -- sc << d1, u o< mc, supf u ≤ sc, spuf u << d1
1567 ... | case1 eq = ?
1568 z42 : ( supf mc o< u ) → (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1)
1569 z42 sc<u = ? where -- spuf mc o< spuf u, mc o< u, ,l
1570 z44 : ( cf nmx d1 ≡ supf u ) ∨ ( cf nmx d1 << supf u )
1571 z44 = ChainP.order is-sup (subst (λ k → supf mc o< k ) ? sc<u ) (init ? ? )
1572 postulate
1573 z26 : (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1)
1574 -- z26 with z43 u (supf mc)
1575 -- ... | case1 lt = z41 lt
1576 -- ... | case2 (case1 eq) = z40 eq
1577 -- ... | case2 (case2 lt) = z42 lt
1578 1549
1579 sd=d : supf d ≡ d 1550 sd=d : supf d ≡ d
1580 sd=d = ZChain.sup=u zc (MinSUP.asm spd) (o<→≤ d<A) ⟪ is-sup , not-hasprev ⟫ 1551 sd=d = ZChain.sup=u zc (MinSUP.asm spd) (o<→≤ d<A) ⟪ is-sup , not-hasprev ⟫
1581 1552
1582 sc<sd : {mc d : Ordinal } → supf mc << supf d → supf mc o< supf d 1553 sc<sd : {mc d : Ordinal } → supf mc << supf d → supf mc o< supf d