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

comparison src/zorn.agda @ 946:3377379a1479

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 31 Oct 2022 11:28:47 +0900
parents da156642b8d0
children a028409f5ca2
comparison
equal deleted inserted replaced
945:da156642b8d0 946:3377379a1479
1463 z29 : (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1) 1463 z29 : (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1)
1464 z29 with z32 1464 z29 with z32
1465 ... | case1 eq1 = case1 (cong (*) (trans (cong (cf nmx) (sym eq)) eq1) ) 1465 ... | case1 eq1 = case1 (cong (*) (trans (cong (cf nmx) (sym eq)) eq1) )
1466 ... | 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)
1467 1467
1468 fsc<<d : {mc z : Ordinal } → (asc : odef A (supf mc)) → (spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc ))
1469 → (fc : FClosure A (cf nmx) (supf mc) z) → z << MinSUP.sup spd
1470 fsc<<d {mc} {z} asc spd fc = z25 where
1471 d1 : Ordinal
1472 d1 = MinSUP.sup spd -- supf d1 ≡ d
1473 z24 : (z ≡ d1) ∨ ( z << d1 )
1474 z24 = MinSUP.x<sup spd fc
1475 --
1476 -- f ( f .. ( supf mc ) <= d1
1477 -- f d1 <= d1
1478 --
1479 z25 : z << d1
1480 z25 with z24
1481 ... | case2 lt = lt
1482 ... | case1 eq = ⊥-elim ( <-irr z29 (proj1 (cf-is-<-monotonic nmx d1 (MinSUP.asm spd)) ) ) where
1483 -- supf mc ≡ d1
1484 z32 : ((cf nmx z) ≡ d1) ∨ ( (cf nmx z) << d1 )
1485 z32 = MinSUP.x<sup spd (fsuc _ fc)
1486 z29 : (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1)
1487 z29 with z32
1488 ... | case1 eq1 = case1 (cong (*) (trans (cong (cf nmx) (sym eq)) eq1) )
1489 ... | case2 lt = case2 (subst (λ k → * k < * d1 ) (cong (cf nmx) eq) lt)
1490
1468 smc<<d : supf mc << d 1491 smc<<d : supf mc << d
1469 smc<<d = sc<<d asc spd 1492 smc<<d = sc<<d asc spd
1470 1493
1471 sz<<c : {z : Ordinal } → z o< & A → supf z <= mc 1494 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) )) 1495 sz<<c z<A = MinSUP.x<sup msp1 (ZChain.csupf zc (z09 (ZChain.asupf zc) ))
1503 not-hasprev hp = ⊥-elim (z29 {mc} {asc} spd z31 hp ) where 1526 not-hasprev hp = ⊥-elim (z29 {mc} {asc} spd z31 hp ) where
1504 z31 : odef (ZChain.chain zc) (cf nmx d) 1527 z31 : odef (ZChain.chain zc) (cf nmx d)
1505 z31 = ZChain.f-next zc (subst (λ k → odef (ZChain.chain zc) k) (sym (HasPrev.x=fy hp)) 1528 z31 = ZChain.f-next zc (subst (λ k → odef (ZChain.chain zc) k) (sym (HasPrev.x=fy hp))
1506 (ZChain.f-next zc 1529 (ZChain.f-next zc
1507 (chain-mono (cf nmx) (cf-is-≤-monotonic nmx) as0 supf (ZChain.supf-mono zc) (o<→≤ d<A) ( HasPrev.ay hp )))) 1530 (chain-mono (cf nmx) (cf-is-≤-monotonic nmx) as0 supf (ZChain.supf-mono zc) (o<→≤ d<A) ( HasPrev.ay hp ))))
1531 z32 : odef (ZChain.chain zc) d
1532 z32 = subst (λ k → odef (ZChain.chain zc) k) (sym (HasPrev.x=fy hp))
1533 (ZChain.f-next zc
1534 (chain-mono (cf nmx) (cf-is-≤-monotonic nmx) as0 supf (ZChain.supf-mono zc) (o<→≤ d<A) ( HasPrev.ay hp )))
1508 -- case1 : FClosure of s 1535 -- case1 : FClosure of s
1509 -- case2 : u o< supf mc 1536 -- case2 : u o< supf mc
1510 -- case3 : u ≡ supf mc z31 1537 -- case3 : u ≡ supf mc z31
1511 -- case4 : supf mc o< u ⊥ ( why ? ) 1538 -- case4 : supf mc o< u ⊥ ( why ? )
1512 z29 : {mc : Ordinal } {asc : odef A (supf mc)} (spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc )) 1539 z29 : {mc : Ordinal } {asc : odef A (supf mc)} (spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc ))
1519 y = HasPrev.y hp -- cf nmx y ≡ d1 1546 y = HasPrev.y hp -- cf nmx y ≡ d1
1520 zy : odef (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) (MinSUP.sup spd)) y 1547 zy : odef (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) (MinSUP.sup spd)) y
1521 zy = HasPrev.ay hp 1548 zy = HasPrev.ay hp
1522 d1 : Ordinal 1549 d1 : Ordinal
1523 d1 = MinSUP.sup spd -- supf d1 ≡ d 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
1524 z30 : * d1 < * (cf nmx d1) 1553 z30 : * d1 < * (cf nmx d1)
1525 z30 = proj1 (cf-is-<-monotonic nmx d1 (MinSUP.asm spd)) 1554 z30 = proj1 (cf-is-<-monotonic nmx d1 (MinSUP.asm spd))
1526 z24 : y << d1 1555 z24 : y << d1
1527 z24 = subst (λ k → y << k) (sym (HasPrev.x=fy hp)) ( proj1 (cf-is-<-monotonic nmx y (proj1 (HasPrev.ay hp) ) )) 1556 z24 = subst (λ k → y << k) (sym (HasPrev.x=fy hp)) ( proj1 (cf-is-<-monotonic nmx y (proj1 (HasPrev.ay hp) ) ))
1528 z40 : ( u ≡ supf mc ) → (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1) 1557 z40 : ( u ≡ supf mc ) → (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1)
1529 z40 = ? 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
1530 z41 : ( u o< supf mc ) → (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1) 1564 z41 : ( u o< supf mc ) → (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1)
1531 z41 = ? 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 = ?
1532 z42 : ( supf mc o< u ) → (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1) 1568 z42 : ( supf mc o< u ) → (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1)
1533 z42 = ? 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 ? ? )
1534 postulate 1572 postulate
1535 z26 : (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1) 1573 z26 : (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1)
1536 -- z26 with z43 u (supf mc) 1574 -- z26 with z43 u (supf mc)
1537 -- ... | case1 lt = z41 lt 1575 -- ... | case1 lt = z41 lt
1538 -- ... | case2 (case1 eq) = z40 eq 1576 -- ... | case2 (case1 eq) = z40 eq