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

comparison src/zorn.agda @ 945:da156642b8d0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
memory exhaust work around
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 31 Oct 2022 02:08:52 +0900
parents e1d727251e25
children 3377379a1479
comparison
equal deleted inserted replaced
944:e1d727251e25 945:da156642b8d0
1491 z22 {a} ⟪ aa , ch-init fc ⟫ = ? 1491 z22 {a} ⟪ aa , ch-init fc ⟫ = ?
1492 z22 {a} ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ = ? 1492 z22 {a} ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ = ?
1493 -- u<x : ZChain.supf zc u o< ZChain.supf zc d 1493 -- u<x : ZChain.supf zc u o< ZChain.supf zc d
1494 -- supf u o< spuf c → order 1494 -- supf u o< spuf c → order
1495 1495
1496 z43 : (u w : Ordinal ) → ( u o< w ) ∨ ( u ≡ w ) ∨ ( w o< u )
1497 z43 u w with trio< u w
1498 ... | tri< a ¬b ¬c = case1 a
1499 ... | tri≈ ¬a b ¬c = case2 (case1 b)
1500 ... | tri> ¬a ¬b c = case2 (case2 c)
1501
1496 not-hasprev : ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) d (cf nmx) 1502 not-hasprev : ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) d (cf nmx)
1497 not-hasprev hp = ⊥-elim (z29 {mc} {asc} spd z31 hp ) where 1503 not-hasprev hp = ⊥-elim (z29 {mc} {asc} spd z31 hp ) where
1498 z31 : odef (ZChain.chain zc) (cf nmx d) 1504 z31 : odef (ZChain.chain zc) (cf nmx d)
1499 z31 = ZChain.f-next zc (subst (λ k → odef (ZChain.chain zc) k) (sym (HasPrev.x=fy hp)) 1505 z31 = ZChain.f-next zc (subst (λ k → odef (ZChain.chain zc) k) (sym (HasPrev.x=fy hp))
1500 (ZChain.f-next zc 1506 (ZChain.f-next zc
1506 z29 : {mc : Ordinal } {asc : odef A (supf mc)} (spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc )) 1512 z29 : {mc : Ordinal } {asc : odef A (supf mc)} (spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc ))
1507 → odef (ZChain.chain zc) (cf nmx (MinSUP.sup spd)) 1513 → odef (ZChain.chain zc) (cf nmx (MinSUP.sup spd))
1508 → HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) (MinSUP.sup spd)) (MinSUP.sup spd) (cf nmx) 1514 → HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) (MinSUP.sup spd)) (MinSUP.sup spd) (cf nmx)
1509 → ⊥ 1515 → ⊥
1510 z29 {mc} {asc} spd ⟪ aa , ch-init fc ⟫ hp = ? 1516 z29 {mc} {asc} spd ⟪ aa , ch-init fc ⟫ hp = ?
1511 z29 {mc} {asc} spd ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ hp = <-irr (z26 u mc d1) z30 where 1517 z29 {mc} {asc} spd ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ hp = <-irr z26 z30 where
1512 y : Ordinal 1518 y : Ordinal
1513 y = HasPrev.y hp -- cf nmx y ≡ d1 1519 y = HasPrev.y hp -- cf nmx y ≡ d1
1514 zy : odef (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) (MinSUP.sup spd)) y 1520 zy : odef (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) (MinSUP.sup spd)) y
1515 zy = HasPrev.ay hp 1521 zy = HasPrev.ay hp
1516 d1 : Ordinal 1522 d1 : Ordinal
1517 d1 = MinSUP.sup spd -- supf d1 ≡ d 1523 d1 = MinSUP.sup spd -- supf d1 ≡ d
1518 z30 : * d1 < * (cf nmx d1) 1524 z30 : * d1 < * (cf nmx d1)
1519 z30 = proj1 (cf-is-<-monotonic nmx d1 (MinSUP.asm spd)) 1525 z30 = proj1 (cf-is-<-monotonic nmx d1 (MinSUP.asm spd))
1520 z24 : y << d1 1526 z24 : y << d1
1521 z24 = subst (λ k → y << k) (sym (HasPrev.x=fy hp)) ( proj1 (cf-is-<-monotonic nmx y (proj1 (HasPrev.ay hp) ) )) 1527 z24 = subst (λ k → y << k) (sym (HasPrev.x=fy hp)) ( proj1 (cf-is-<-monotonic nmx y (proj1 (HasPrev.ay hp) ) ))
1522 z26 : (u mc d1 : Ordinal ) → (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1) 1528 z40 : ( u ≡ supf mc ) → (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1)
1523 z26 u mc d1 = ? -- with trio< u (supf mc) 1529 z40 = ?
1524 -- ... | tri< a ¬b ¬c = ? 1530 z41 : ( u o< supf mc ) → (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1)
1525 -- ... | tri> ¬a ¬b x<z = ? 1531 z41 = ?
1526 -- ... | tri≈ ¬a b ¬c = ? -- with MinSUP.x<sup spd fc 1532 z42 : ( supf mc o< u ) → (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1)
1527 -- ... | case1 eq = ? -- case1 (cong (*) eq) 1533 z42 = ?
1528 -- ... | case2 lt = ? -- case2 lt 1534 postulate
1535 z26 : (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1)
1536 -- z26 with z43 u (supf mc)
1537 -- ... | case1 lt = z41 lt
1538 -- ... | case2 (case1 eq) = z40 eq
1539 -- ... | case2 (case2 lt) = z42 lt
1529 1540
1530 sd=d : supf d ≡ d 1541 sd=d : supf d ≡ d
1531 sd=d = ZChain.sup=u zc (MinSUP.asm spd) (o<→≤ d<A) ⟪ is-sup , not-hasprev ⟫ 1542 sd=d = ZChain.sup=u zc (MinSUP.asm spd) (o<→≤ d<A) ⟪ is-sup , not-hasprev ⟫
1532 1543
1533 sc<sd : {mc d : Ordinal } → supf mc << supf d → supf mc o< supf d 1544 sc<sd : {mc d : Ordinal } → supf mc << supf d → supf mc o< supf d