Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison src/zorn.agda @ 943:df68bb333cd0
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 30 Oct 2022 18:19:33 +0900 |
parents | d396af76c559 |
children | e1d727251e25 |
comparison
equal
deleted
inserted
replaced
942:d396af76c559 | 943:df68bb333cd0 |
---|---|
1422 sp1 : SUP A (ZChain.chain zc) | 1422 sp1 : SUP A (ZChain.chain zc) |
1423 sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc | 1423 sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc |
1424 c : Ordinal | 1424 c : Ordinal |
1425 c = & ( SUP.sup sp1 ) | 1425 c = & ( SUP.sup sp1 ) |
1426 mc = MinSUP.sup msp1 | 1426 mc = MinSUP.sup msp1 |
1427 mc<A : mc o< & A | |
1428 mc<A = ∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫ | |
1427 c=mc : c ≡ mc | 1429 c=mc : c ≡ mc |
1428 c=mc = &iso | 1430 c=mc = &iso |
1429 z20 : mc << cf nmx mc | 1431 z20 : mc << cf nmx mc |
1430 z20 = proj1 (cf-is-<-monotonic nmx mc (MinSUP.asm msp1) ) | 1432 z20 = proj1 (cf-is-<-monotonic nmx mc (MinSUP.asm msp1) ) |
1431 asc : odef A (supf mc) | 1433 asc : odef A (supf mc) |
1438 msup : MinSUP A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 supf d) | 1440 msup : MinSUP A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 supf d) |
1439 msup = ZChain.minsup zc (o<→≤ d<A) | 1441 msup = ZChain.minsup zc (o<→≤ d<A) |
1440 sd=ms : supf d ≡ MinSUP.sup ( ZChain.minsup zc (o<→≤ d<A) ) | 1442 sd=ms : supf d ≡ MinSUP.sup ( ZChain.minsup zc (o<→≤ d<A) ) |
1441 sd=ms = ZChain.supf-is-minsup zc (o<→≤ d<A) | 1443 sd=ms = ZChain.supf-is-minsup zc (o<→≤ d<A) |
1442 | 1444 |
1443 sc<<d : {mc : Ordinal } → {asc : odef A (supf mc)} → (spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc )) | 1445 sc<<d : {mc : Ordinal } → (asc : odef A (supf mc)) → (spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc )) |
1444 → supf mc << MinSUP.sup spd | 1446 → supf mc << MinSUP.sup spd |
1445 sc<<d {mc} {asc} spd = z25 where | 1447 sc<<d {mc} asc spd = z25 where |
1446 d1 : Ordinal | 1448 d1 : Ordinal |
1447 d1 = MinSUP.sup spd -- supf d1 ≡ d | 1449 d1 = MinSUP.sup spd -- supf d1 ≡ d |
1448 z24 : (supf mc ≡ d1) ∨ ( supf mc << d1 ) | 1450 z24 : (supf mc ≡ d1) ∨ ( supf mc << d1 ) |
1449 z24 = MinSUP.x<sup spd (init asc refl) | 1451 z24 = MinSUP.x<sup spd (init asc refl) |
1450 -- | 1452 -- |
1461 z29 : (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1) | 1463 z29 : (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1) |
1462 z29 with z32 | 1464 z29 with z32 |
1463 ... | case1 eq1 = case1 (cong (*) (trans (cong (cf nmx) (sym eq)) eq1) ) | 1465 ... | case1 eq1 = case1 (cong (*) (trans (cong (cf nmx) (sym eq)) eq1) ) |
1464 ... | case2 lt = case2 (subst (λ k → * k < * d1 ) (cong (cf nmx) eq) lt) | 1466 ... | case2 lt = case2 (subst (λ k → * k < * d1 ) (cong (cf nmx) eq) lt) |
1465 | 1467 |
1468 smc<<d : supf mc << d | |
1469 smc<<d = sc<<d asc spd | |
1470 | |
1471 sz<<c : {z : Ordinal } → z o< & A → supf z <= mc | |
1472 sz<<c z<A = MinSUP.x<sup msp1 (ZChain.csupf zc (z09 (ZChain.asupf zc) )) | |
1473 | |
1474 sc=c : supf mc ≡ mc | |
1475 sc=c = ZChain.sup=u zc (MinSUP.asm msp1) (o<→≤ (∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫ )) ⟪ is-sup , not-hasprev ⟫ where | |
1476 is-sup : IsSup A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc) (MinSUP.asm msp1) | |
1477 is-sup = record { x<sup = λ zy → MinSUP.x<sup msp1 (chain-mono (cf nmx) (cf-is-≤-monotonic nmx) as0 supf (ZChain.supf-mono zc) (o<→≤ mc<A) zy )} | |
1478 not-hasprev : ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc) mc (cf nmx) | |
1479 not-hasprev hp = <-irr z26 z30 where | |
1480 z30 : * mc < * (cf nmx mc) | |
1481 z30 = proj1 (cf-is-<-monotonic nmx mc (MinSUP.asm msp1)) | |
1482 z26 : (* (cf nmx mc) ≡ * mc) ∨ (* (cf nmx mc) < * mc) | |
1483 z26 with MinSUP.x<sup msp1 ? | |
1484 ... | case1 eq = case1 (cong (*) eq) | |
1485 ... | case2 lt = case2 lt | |
1486 | |
1466 is-sup : IsSup A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) (MinSUP.asm spd) | 1487 is-sup : IsSup A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) (MinSUP.asm spd) |
1467 is-sup = record { x<sup = z22 } where | 1488 is-sup = record { x<sup = z22 } where |
1468 z23 : {z : Ordinal } → odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc) z → (z ≡ MinSUP.sup spd) ∨ (z << MinSUP.sup spd) | 1489 z23 : {z : Ordinal } → odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc) z → (z ≡ MinSUP.sup spd) ∨ (z << MinSUP.sup spd) |
1469 z23 lt = MinSUP.x<sup spd lt | 1490 z23 lt = MinSUP.x<sup spd lt |
1470 z22 : {y : Ordinal} → odef (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) y → | 1491 z22 : {y : Ordinal} → odef (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) y → |
1473 z22 {a} ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ = ? | 1494 z22 {a} ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ = ? |
1474 -- u<x : ZChain.supf zc u o< ZChain.supf zc d | 1495 -- u<x : ZChain.supf zc u o< ZChain.supf zc d |
1475 -- supf u o< spuf c → order | 1496 -- supf u o< spuf c → order |
1476 | 1497 |
1477 not-hasprev : ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) d (cf nmx) | 1498 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 {mc} {asc} spd hp) where | 1499 not-hasprev hp = ⊥-elim (z29 {mc} {asc} spd hp ) where |
1479 z29 : {mc : Ordinal } {asc : odef A (supf mc)} (spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc )) | 1500 z29 : {mc : Ordinal } {asc : odef A (supf mc)} (spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc )) |
1480 → HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) (MinSUP.sup spd)) (MinSUP.sup spd) (cf nmx) | 1501 → HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) (MinSUP.sup spd)) (MinSUP.sup spd) (cf nmx) |
1481 → ⊥ | 1502 → ⊥ |
1482 z29 {mc} {asc} spd hp = <-irr z26 z30 where | 1503 z29 {mc} {asc} spd hp = <-irr z26 z30 where |
1483 y : Ordinal | 1504 y : Ordinal |
1484 y = HasPrev.y hp | 1505 y = HasPrev.y hp |
1485 d1 : Ordinal | 1506 d1 : Ordinal |
1486 d1 = MinSUP.sup spd -- supf d1 ≡ d | 1507 d1 = MinSUP.sup spd -- supf d1 ≡ d |
1508 z31 : odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc) (cf nmx (MinSUP.sup spd)) | |
1509 z31 = ? | |
1487 z30 : * d1 < * (cf nmx d1) | 1510 z30 : * d1 < * (cf nmx d1) |
1488 z30 = proj1 (cf-is-<-monotonic nmx d1 (MinSUP.asm spd)) | 1511 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 = ? | |
1491 z24 : y << d1 | 1512 z24 : y << d1 |
1492 z24 = subst (λ k → y << k) (sym (HasPrev.x=fy hp)) ( proj1 (cf-is-<-monotonic nmx y (proj1 (HasPrev.ay hp) ) )) | 1513 z24 = subst (λ k → y << k) (sym (HasPrev.x=fy hp)) ( proj1 (cf-is-<-monotonic nmx y (proj1 (HasPrev.ay hp) ) )) |
1493 z26 : (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1) | 1514 z26 : (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1) |
1494 z26 with MinSUP.x<sup spd z31 | 1515 z26 with MinSUP.x<sup spd z31 |
1495 ... | case1 eq = case1 (cong (*) eq) | 1516 ... | case1 eq = case1 (cong (*) eq) |
1496 ... | case2 lt = case2 lt | 1517 ... | case2 lt = case2 lt |
1518 -- case1 : FClosure of y | |
1519 -- case2 : u o< supf mc | |
1520 -- case3 : u ≡ supf mc z31 | |
1521 -- case4 : supf mc o< u ⊥ ( why ? ) | |
1497 z25 : odef (ZChain.chain zc) (cf nmx d) | 1522 z25 : odef (ZChain.chain zc) (cf nmx d) |
1498 z25 = ZChain.f-next zc (subst (λ k → odef (ZChain.chain zc) k) (sym (HasPrev.x=fy hp)) | 1523 z25 = ZChain.f-next zc (subst (λ k → odef (ZChain.chain zc) k) (sym (HasPrev.x=fy hp)) |
1499 (ZChain.f-next zc | 1524 (ZChain.f-next zc |
1500 (chain-mono (cf nmx) (cf-is-≤-monotonic nmx) as0 supf (ZChain.supf-mono zc) (o<→≤ d<A) ( HasPrev.ay hp )))) | 1525 (chain-mono (cf nmx) (cf-is-≤-monotonic nmx) as0 supf (ZChain.supf-mono zc) (o<→≤ d<A) ( HasPrev.ay hp )))) |
1501 | 1526 |
1508 ... | case2 lt = lt | 1533 ... | case2 lt = lt |
1509 | 1534 |
1510 sms<sa : supf mc o< supf (& A) | 1535 sms<sa : supf mc o< supf (& A) |
1511 sms<sa with osuc-≡< ( ZChain.supf-mono zc (o<→≤ ( ∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫) )) | 1536 sms<sa with osuc-≡< ( ZChain.supf-mono zc (o<→≤ ( ∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫) )) |
1512 ... | case2 lt = lt | 1537 ... | case2 lt = lt |
1513 ... | case1 eq = ⊥-elim ( o<¬≡ eq ( ordtrans<-≤ (sc<sd (subst (λ k → supf mc << k ) (sym sd=d) (sc<<d {mc} {asc} spd)) ) | 1538 ... | case1 eq = ⊥-elim ( o<¬≡ eq ( ordtrans<-≤ (sc<sd (subst (λ k → supf mc << k ) (sym sd=d) (sc<<d {mc} asc spd)) ) |
1514 ( ZChain.supf-mono zc (o<→≤ d<A )))) | 1539 ( ZChain.supf-mono zc (o<→≤ d<A )))) |
1515 | 1540 |
1516 ss<sa : supf c o< supf (& A) | 1541 ss<sa : supf c o< supf (& A) |
1517 ss<sa = subst (λ k → supf k o< supf (& A)) (sym c=mc) sms<sa | 1542 ss<sa = subst (λ k → supf k o< supf (& A)) (sym c=mc) sms<sa |
1518 | 1543 |