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

comparison src/zorn.agda @ 937:3a511519bd10

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, 24 Oct 2022 19:11:19 +0900
parents f160556a7c9a
children 93a49ffa9183
comparison
equal deleted inserted replaced
936:f160556a7c9a 937:3a511519bd10
1413 z04 nmx zc = <-irr0 {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.as sp1 )))) 1413 z04 nmx zc = <-irr0 {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.as sp1 ))))
1414 (subst (λ k → odef A (& k)) (sym *iso) (SUP.as sp1) ) 1414 (subst (λ k → odef A (& k)) (sym *iso) (SUP.as sp1) )
1415 (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc 1415 (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc
1416 (sp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc ) ss<sa ))) -- x ≡ f x ̄ 1416 (sp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc ) ss<sa ))) -- x ≡ f x ̄
1417 (proj1 (cf-is-<-monotonic nmx c (SUP.as sp1 ))) where -- x < f x 1417 (proj1 (cf-is-<-monotonic nmx c (SUP.as sp1 ))) where -- x < f x
1418
1418 supf = ZChain.supf zc 1419 supf = ZChain.supf zc
1419 msp1 : MinSUP A (ZChain.chain zc) 1420 msp1 : MinSUP A (ZChain.chain zc)
1420 msp1 = msp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc 1421 msp1 = msp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc
1421 sp1 : SUP A (ZChain.chain zc) 1422 sp1 : SUP A (ZChain.chain zc)
1422 sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc 1423 sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc
1436 d<A = ∈∧P→o< ⟪ MinSUP.asm spd , lift true ⟫ 1437 d<A = ∈∧P→o< ⟪ MinSUP.asm spd , lift true ⟫
1437 msup : MinSUP A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 supf d) 1438 msup : MinSUP A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 supf d)
1438 msup = ZChain.minsup zc (o<→≤ d<A) 1439 msup = ZChain.minsup zc (o<→≤ d<A)
1439 sd=ms : supf d ≡ MinSUP.sup ( ZChain.minsup zc (o<→≤ d<A) ) 1440 sd=ms : supf d ≡ MinSUP.sup ( ZChain.minsup zc (o<→≤ d<A) )
1440 sd=ms = ZChain.supf-is-minsup zc (o<→≤ d<A) 1441 sd=ms = ZChain.supf-is-minsup zc (o<→≤ d<A)
1441 -- z26 : {x : Ordinal } → odef (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) x 1442
1442 -- → odef (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) c) x ∨ odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc ) x
1443 -- z26 = ?
1444 is-sup : IsSup A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) (MinSUP.asm spd) 1443 is-sup : IsSup A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) (MinSUP.asm spd)
1445 is-sup = record { x<sup = z22 } where 1444 is-sup = record { x<sup = z22 } where
1446 z23 : {z : Ordinal } → odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc) z → (z ≡ MinSUP.sup spd) ∨ (z << MinSUP.sup spd) 1445 z23 : {z : Ordinal } → odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc) z → (z ≡ MinSUP.sup spd) ∨ (z << MinSUP.sup spd)
1447 z23 lt = MinSUP.x<sup spd lt 1446 z23 lt = MinSUP.x<sup spd lt
1448 z22 : {y : Ordinal} → odef (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) y → 1447 z22 : {y : Ordinal} → odef (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) y →
1449 (y ≡ MinSUP.sup spd) ∨ (y << MinSUP.sup spd) 1448 (y ≡ MinSUP.sup spd) ∨ (y << MinSUP.sup spd)
1450 z22 {a} ⟪ aa , ch-init fc ⟫ = ? 1449 z22 {a} ⟪ aa , ch-init fc ⟫ = ?
1451 z22 {a} ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ = ? 1450 z22 {a} ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ = ?
1452 -- u<x : ZChain.supf zc u o< ZChain.supf zc d 1451 -- u<x : ZChain.supf zc u o< ZChain.supf zc d
1453 -- supf u o< spuf c → order 1452 -- supf u o< spuf c → order
1453
1454 not-hasprev : ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) d (cf nmx) 1454 not-hasprev : ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) d (cf nmx)
1455 not-hasprev hp = ? where 1455 not-hasprev hp = ? where
1456 y : Ordinal 1456 y : Ordinal
1457 y = HasPrev.y hp 1457 y = HasPrev.y hp
1458 z24 : y << d 1458 z24 : y << d
1459 z24 = subst (λ k → y << k) (sym (HasPrev.x=fy hp)) ( proj1 (cf-is-<-monotonic nmx y (proj1 (HasPrev.ay hp) ) )) 1459 z24 = subst (λ k → y << k) (sym (HasPrev.x=fy hp)) ( proj1 (cf-is-<-monotonic nmx y (proj1 (HasPrev.ay hp) ) ))
1460 -- z26 : {x : Ordinal } → odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc ) x → (x ≡ d ) ∨ (x << d ) 1460 z25 : odef (ZChain.chain zc) (cf nmx d)
1461 -- z26 lt with MinSUP.x<sup spd (subst (λ k → odef _ k ) ? lt) 1461 z25 = ZChain.f-next zc (subst (λ k → odef (ZChain.chain zc) k) (sym (HasPrev.x=fy hp))
1462 -- ... | case1 eq = ? 1462 (ZChain.f-next zc
1463 -- ... | case2 lt = ? 1463 (chain-mono (cf nmx) (cf-is-≤-monotonic nmx) as0 supf (ZChain.supf-mono zc) (o<→≤ d<A) ( HasPrev.ay hp ))))
1464 -- z25 : {x : Ordinal } → odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc ) x → (x ≡ y ) ∨ (x << y )
1465 -- z25 {x} (init au eq ) = ? -- sup c = x, cf y ≡ d, sup c =< d
1466 -- z25 (fsuc x lt) = ? -- cf (sup c)
1467 1464
1468 sd=d : supf d ≡ d 1465 sd=d : supf d ≡ d
1469 sd=d = ZChain.sup=u zc (MinSUP.asm spd) (o<→≤ d<A) ⟪ is-sup , not-hasprev ⟫ 1466 sd=d = ZChain.sup=u zc (MinSUP.asm spd) (o<→≤ d<A) ⟪ is-sup , not-hasprev ⟫
1470 1467
1471 sc<<d : {mc : Ordinal } → {asc : odef A (supf mc)} → (spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc )) 1468 sc<<d : {mc : Ordinal } → {asc : odef A (supf mc)} → (spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc ))
1473 sc<<d {mc} {asc} spd = z25 where 1470 sc<<d {mc} {asc} spd = z25 where
1474 d1 : Ordinal 1471 d1 : Ordinal
1475 d1 = MinSUP.sup spd 1472 d1 = MinSUP.sup spd
1476 z24 : (supf mc ≡ d1) ∨ ( supf mc << d1 ) 1473 z24 : (supf mc ≡ d1) ∨ ( supf mc << d1 )
1477 z24 = MinSUP.x<sup spd (init asc refl) 1474 z24 = MinSUP.x<sup spd (init asc refl)
1475 z26 : odef (ZChain.chain zc) (supf mc)
1476 z26 = ?
1477 z28 : supf mc o< & A
1478 z28 = z09 (ZChain.asupf zc)
1478 z25 : supf mc << d1 1479 z25 : supf mc << d1
1479 z25 with z24 1480 z25 with z24
1480 ... | case2 lt = lt 1481 ... | case2 lt = lt
1481 ... | case1 eq = ? 1482 ... | case1 eq = ? where
1483 z27 : odef (ZChain.chain zc) (cf nmx d1)
1484 z27 = ZChain.f-next zc (subst (λ k → odef (ZChain.chain zc) k ) eq (ZChain.csupf zc z28))
1482 1485
1483 sc<sd : {mc d : Ordinal } → supf mc << supf d → supf mc o< supf d 1486 sc<sd : {mc d : Ordinal } → supf mc << supf d → supf mc o< supf d
1484 sc<sd {mc} {d} sc<<sd with osuc-≡< ( ZChain.supf-<= zc (case2 sc<<sd ) ) 1487 sc<sd {mc} {d} sc<<sd with osuc-≡< ( ZChain.supf-<= zc (case2 sc<<sd ) )
1485 ... | case1 eq = ⊥-elim ( <-irr (case1 (cong (*) (sym eq) )) sc<<sd ) 1488 ... | case1 eq = ⊥-elim ( <-irr (case1 (cong (*) (sym eq) )) sc<<sd )
1486 ... | case2 lt = lt 1489 ... | case2 lt = lt