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

comparison src/zorn.agda @ 930:0e0608b1953b

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 Sun, 23 Oct 2022 23:29:30 +0900
parents a6d97e6e5309
children ebcad8e5ae55
comparison
equal deleted inserted replaced
929:a6d97e6e5309 930:0e0608b1953b
1425 d<A = ∈∧P→o< ⟪ MinSUP.asm spd , lift true ⟫ 1425 d<A = ∈∧P→o< ⟪ MinSUP.asm spd , lift true ⟫
1426 msup : MinSUP A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 supf d) 1426 msup : MinSUP A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 supf d)
1427 msup = ZChain.minsup zc (o<→≤ d<A) 1427 msup = ZChain.minsup zc (o<→≤ d<A)
1428 sd=ms : supf d ≡ MinSUP.sup ( ZChain.minsup zc (o<→≤ d<A) ) 1428 sd=ms : supf d ≡ MinSUP.sup ( ZChain.minsup zc (o<→≤ d<A) )
1429 sd=ms = ZChain.supf-is-minsup zc (o<→≤ d<A) 1429 sd=ms = ZChain.supf-is-minsup zc (o<→≤ d<A)
1430 -- z26 : {x : Ordinal } → odef (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) x
1431 -- → 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
1432 -- z26 = ?
1430 is-sup : IsSup A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) (MinSUP.asm spd) 1433 is-sup : IsSup A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) (MinSUP.asm spd)
1431 is-sup = record { x<sup = z22 } where 1434 is-sup = record { x<sup = z22 } where
1432 --
1433 z23 : {z : Ordinal } → odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc) z → (z ≡ MinSUP.sup spd) ∨ (z << MinSUP.sup spd) 1435 z23 : {z : Ordinal } → odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc) z → (z ≡ MinSUP.sup spd) ∨ (z << MinSUP.sup spd)
1434 z23 lt = MinSUP.x<sup spd lt 1436 z23 lt = MinSUP.x<sup spd lt
1435 z22 : {y : Ordinal} → odef (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) y → 1437 z22 : {y : Ordinal} → odef (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) y →
1436 (y ≡ MinSUP.sup spd) ∨ (y << MinSUP.sup spd) 1438 (y ≡ MinSUP.sup spd) ∨ (y << MinSUP.sup spd)
1437 z22 {y} zy = ? 1439 z22 {a} ⟪ aa , ch-init fc ⟫ = ?
1438 -- with MinSUP.x<sup spd ? -- (subst (λ k → odef _ k ) (sym &iso) zy) 1440 z22 {a} ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ = ?
1439 -- ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso y=p ) 1441 -- u<x : ZChain.supf zc u o< ZChain.supf zc d
1440 -- ... | case2 y<p = case2 (subst (λ k → * y < k ) (sym *iso) y<p ) 1442 -- supf u o< spuf c → order
1441 not-hasprev : ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) d (cf nmx) 1443 not-hasprev : ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) d (cf nmx)
1442 not-hasprev hp = ? where 1444 not-hasprev hp = ? where
1443 y : Ordinal 1445 y : Ordinal
1444 y = HasPrev.y hp 1446 y = HasPrev.y hp
1445 z24 : y << d 1447 z24 : y << d
1446 z24 = subst (λ k → y << k) (sym (HasPrev.x=fy hp)) ( proj1 (cf-is-<-monotonic nmx y (proj1 (HasPrev.ay hp) ) )) 1448 z24 = subst (λ k → y << k) (sym (HasPrev.x=fy hp)) ( proj1 (cf-is-<-monotonic nmx y (proj1 (HasPrev.ay hp) ) ))
1449 -- z26 : {x : Ordinal } → odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc ) x → (x ≡ d ) ∨ (x << d )
1450 -- z26 lt with MinSUP.x<sup spd (subst (λ k → odef _ k ) ? lt)
1451 -- ... | case1 eq = ?
1452 -- ... | case2 lt = ?
1453 -- z25 : {x : Ordinal } → odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc ) x → (x ≡ y ) ∨ (x << y )
1454 -- z25 {x} (init au eq ) = ? -- sup c = x, cf y ≡ d, sup c =< d
1455 -- z25 (fsuc x lt) = ? -- cf (sup c)
1447 sd=d : supf d ≡ d 1456 sd=d : supf d ≡ d
1448 sd=d = ZChain.sup=u zc (MinSUP.asm spd) (o<→≤ d<A) ⟪ is-sup , not-hasprev ⟫ 1457 sd=d = ZChain.sup=u zc (MinSUP.asm spd) (o<→≤ d<A) ⟪ is-sup , not-hasprev ⟫
1449 sc<d : supf c << d 1458 sc<sd : supf c << supf d
1450 sc<d = ? where 1459 sc<sd = ?
1451 z21 = proj1 ( cf-is-<-monotonic nmx ? ? ) 1460 -- z21 = proj1 ( cf-is-<-monotonic nmx ? ? )
1452 sco<d : supf c o< supf d 1461 -- sco<d : supf c o< supf d
1453 sco<d = ? 1462 -- sco<d with osuc-≡< ( ZChain.supf-<= zc (case2 sc<sd ) )
1463 -- ... | case1 eq = ⊥-elim ( <-irr eq sc<sd )
1464 -- ... | case2 lt = lt
1454 1465
1455 ss<sa : supf c o< supf (& A) 1466 ss<sa : supf c o< supf (& A)
1456 ss<sa with osuc-≡< ( ZChain.supf-mono zc ? ) 1467 ss<sa = ? -- with osuc-≡< ( ZChain.supf-mono zc (o<→≤ ( ∈∧P→o< ⟪ SUP.as sp0 , lift true ⟫) ))
1457 ... | case2 lt = lt 1468 -- ... | case2 lt = lt
1458 ... | case1 eq = ? -- where 1469 -- ... | case1 eq = ? -- where
1459 zorn00 : Maximal A 1470 zorn00 : Maximal A
1460 zorn00 with is-o∅ ( & HasMaximal ) -- we have no Level (suc n) LEM 1471 zorn00 with is-o∅ ( & HasMaximal ) -- we have no Level (suc n) LEM
1461 ... | no not = record { maximal = ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) ; as = zorn01 ; ¬maximal<x = zorn02 } where 1472 ... | no not = record { maximal = ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) ; as = zorn01 ; ¬maximal<x = zorn02 } where
1462 -- yes we have the maximal 1473 -- yes we have the maximal
1463 zorn03 : odef HasMaximal ( & ( ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) ) ) 1474 zorn03 : odef HasMaximal ( & ( ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) ) )