Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison src/zorn.agda @ 942:d396af76c559
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 29 Oct 2022 17:26:17 +0900 |
parents | 6f342473f298 |
children | df68bb333cd0 |
comparison
equal
deleted
inserted
replaced
941:6f342473f298 | 942:d396af76c559 |
---|---|
1473 z22 {a} ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ = ? | 1473 z22 {a} ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ = ? |
1474 -- u<x : ZChain.supf zc u o< ZChain.supf zc d | 1474 -- u<x : ZChain.supf zc u o< ZChain.supf zc d |
1475 -- supf u o< spuf c → order | 1475 -- supf u o< spuf c → order |
1476 | 1476 |
1477 not-hasprev : ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) d (cf nmx) | 1477 not-hasprev : ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) d (cf nmx) |
1478 not-hasprev hp = ⊥-elim (z29 spd ? hp) where | 1478 not-hasprev hp = ⊥-elim (z29 {mc} {asc} spd hp) where |
1479 -- z31 : odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc) (cf nmx d) | |
1480 -- z31 = ? | |
1481 z29 : {mc : Ordinal } {asc : odef A (supf mc)} (spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc )) | 1479 z29 : {mc : Ordinal } {asc : odef A (supf mc)} (spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc )) |
1482 → odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc) (cf nmx (MinSUP.sup spd)) | |
1483 → HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) (MinSUP.sup spd)) (MinSUP.sup spd) (cf nmx) | 1480 → HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) (MinSUP.sup spd)) (MinSUP.sup spd) (cf nmx) |
1484 → ⊥ | 1481 → ⊥ |
1485 z29 {mc} {asc} spd ufd hp = <-irr ? z30 where | 1482 z29 {mc} {asc} spd hp = <-irr z26 z30 where |
1486 y : Ordinal | 1483 y : Ordinal |
1487 y = HasPrev.y hp | 1484 y = HasPrev.y hp |
1488 d1 : Ordinal | 1485 d1 : Ordinal |
1489 d1 = MinSUP.sup spd -- supf d1 ≡ d | 1486 d1 = MinSUP.sup spd -- supf d1 ≡ d |
1490 z30 : * d1 < * (cf nmx d1) | 1487 z30 : * d1 < * (cf nmx d1) |
1491 z30 = ? | 1488 z30 = proj1 (cf-is-<-monotonic nmx d1 (MinSUP.asm spd)) |
1489 z31 : odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc) (cf nmx d1) | |
1490 z31 = ? | |
1492 z24 : y << d1 | 1491 z24 : y << d1 |
1493 z24 = subst (λ k → y << k) (sym (HasPrev.x=fy hp)) ( proj1 (cf-is-<-monotonic nmx y (proj1 (HasPrev.ay hp) ) )) | 1492 z24 = subst (λ k → y << k) (sym (HasPrev.x=fy hp)) ( proj1 (cf-is-<-monotonic nmx y (proj1 (HasPrev.ay hp) ) )) |
1494 -- z26 : (* (cf nmx (MinSUP.sup spd)) ≡ * (MinSUP.sup spd)) ∨ (* (cf nmx (MinSUP.sup spd)) < * (MinSUP.sup spd)) | 1493 z26 : (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1) |
1495 -- z26 with MinSUP.x<sup spd ? | 1494 z26 with MinSUP.x<sup spd z31 |
1496 -- ... | case1 eq = ? | 1495 ... | case1 eq = case1 (cong (*) eq) |
1497 -- ... | case2 lt = ? | 1496 ... | case2 lt = case2 lt |
1498 z25 : odef (ZChain.chain zc) (cf nmx d) | 1497 z25 : odef (ZChain.chain zc) (cf nmx d) |
1499 z25 = ZChain.f-next zc (subst (λ k → odef (ZChain.chain zc) k) (sym (HasPrev.x=fy hp)) | 1498 z25 = ZChain.f-next zc (subst (λ k → odef (ZChain.chain zc) k) (sym (HasPrev.x=fy hp)) |
1500 (ZChain.f-next zc | 1499 (ZChain.f-next zc |
1501 (chain-mono (cf nmx) (cf-is-≤-monotonic nmx) as0 supf (ZChain.supf-mono zc) (o<→≤ d<A) ( HasPrev.ay hp )))) | 1500 (chain-mono (cf nmx) (cf-is-≤-monotonic nmx) as0 supf (ZChain.supf-mono zc) (o<→≤ d<A) ( HasPrev.ay hp )))) |
1502 | 1501 |