Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison src/zorn.agda @ 948:51556591c879
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 31 Oct 2022 18:34:06 +0900 |
| parents | a028409f5ca2 |
| children | efc833407350 |
comparison
equal
deleted
inserted
replaced
| 947:a028409f5ca2 | 948:51556591c879 |
|---|---|
| 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 supf 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 record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-init fc ⟫ ; x=fy = x=fy } = ? | 1526 not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-init fc ⟫ ; x=fy = x=fy } = ? |
| 1527 not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-is-sup u u<x is-sup1 fc ⟫; x=fy = x=fy } = ? | 1527 not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-is-sup u u<x is-sup1 fc ⟫; x=fy = x=fy } = ⊥-elim ( <-irr z46 z30 ) where |
| 1528 -- z29 : {mc d1 : Ordinal } {asc : odef A (supf mc)} (spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc )) | 1528 z45 : (* (cf nmx (cf nmx y)) ≡ * d) ∨ (* (cf nmx (cf nmx y)) < * d) → (* (cf nmx d) ≡ * d) ∨ (* (cf nmx d) < * d) |
| 1529 -- → d1 ≡ MinSUP.sup spd | 1529 z45 p = subst (λ k → (* (cf nmx k) ≡ * d) ∨ (* (cf nmx k) < * d)) (sym x=fy) p |
| 1530 -- → HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 supf d1) d1 (cf nmx) | 1530 z48 : supf mc << d |
| 1531 -- → ⊥ | 1531 z48 = sc<<d {mc} asc spd |
| 1532 -- z29 {mc} {asc} spd d1=spd hp with HasPrev.ay hp | 1532 z47 : {mc d1 : Ordinal } {asc : odef A (supf mc)} (spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc )) |
| 1533 -- ... | ⟪ ua1 , ch-init fc ⟫ = ? | 1533 → * (cf nmx (cf nmx y)) < * d1 |
| 1534 -- ... | ⟪ ua1 , ch-is-sup u u<x is-sup1 fc ⟫ = ? | 1534 z47 {mc} {d1} {asc} spd = ? |
| 1535 -- y : Ordinal | 1535 z30 : * d < * (cf nmx d) |
| 1536 -- y = HasPrev.y hp | 1536 z30 = proj1 (cf-is-<-monotonic nmx d (MinSUP.asm spd)) |
| 1537 -- d1 : Ordinal | 1537 z46 : (* (cf nmx d) ≡ * d) ∨ (* (cf nmx d) < * d) |
| 1538 -- d1 = MinSUP.sup spd -- supf d1 ≡ d | 1538 z46 = z45 (case2 (z47 {mc} {d} {asc} spd )) |
| 1539 -- z45 : (* (cf nmx (cf nmx y)) ≡ * d1) ∨ (* (cf nmx (cf nmx y)) < * d1) → (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1) | 1539 |
| 1540 -- z45 p = subst (λ k → (* (cf nmx k) ≡ * d1) ∨ (* (cf nmx k) < * d1)) (sym (HasPrev.x=fy hp)) p | 1540 -- ax : odef A d |
| 1541 -- z30 : * d1 < * (cf nmx d1) | 1541 -- y : Ordinal |
| 1542 -- z30 = proj1 (cf-is-<-monotonic nmx d1 (MinSUP.asm spd)) | 1542 -- ua1 : odef A y |
| 1543 -- z47 : * (cf nmx (cf nmx y)) < * d1 | 1543 -- u : Ordinal |
| 1544 -- z47 = ? | 1544 -- u<x : supf u o< supf d |
| 1545 -- z24 : y << d1 | 1545 -- is-sup1 : ChainP A (cf nmx) (cf-is-≤-monotonic nmx) as0 supf u |
| 1546 -- z24 = subst (λ k → y << k) (sym (HasPrev.x=fy hp)) ( proj1 (cf-is-<-monotonic nmx y (proj1 (HasPrev.ay hp) ) )) | 1546 -- fc : FClosure A (cf nmx) (supf u) y |
| 1547 -- z46 : (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1) | 1547 -- x=fy : d ≡ cf nmx y |
| 1548 -- z46 = z45 (case2 z47 ) | |
| 1549 | 1548 |
| 1550 sd=d : supf d ≡ d | 1549 sd=d : supf d ≡ d |
| 1551 sd=d = ZChain.sup=u zc (MinSUP.asm spd) (o<→≤ d<A) ⟪ is-sup , not-hasprev ⟫ | 1550 sd=d = ZChain.sup=u zc (MinSUP.asm spd) (o<→≤ d<A) ⟪ is-sup , not-hasprev ⟫ |
| 1552 | 1551 |
| 1553 sc<sd : {mc d : Ordinal } → supf mc << supf d → supf mc o< supf d | 1552 sc<sd : {mc d : Ordinal } → supf mc << supf d → supf mc o< supf d |