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

comparison src/zorn.agda @ 929:a6d97e6e5309

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 Sat, 22 Oct 2022 18:26:16 +0900
parents 330303f0c688
children 0e0608b1953b
comparison
equal deleted inserted replaced
928:330303f0c688 929:a6d97e6e5309
1421 spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc ) 1421 spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc )
1422 spd = ysup (cf nmx) (cf-is-≤-monotonic nmx) asc 1422 spd = ysup (cf nmx) (cf-is-≤-monotonic nmx) asc
1423 d = MinSUP.sup spd 1423 d = MinSUP.sup spd
1424 d<A : d o< & A 1424 d<A : d o< & A
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)
1427 msup = ZChain.minsup zc (o<→≤ d<A)
1426 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) )
1427 sd=ms = ZChain.supf-is-minsup zc (o<→≤ d<A) 1429 sd=ms = ZChain.supf-is-minsup zc (o<→≤ d<A)
1430 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
1432 --
1433 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
1435 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)
1437 z22 {y} zy = ?
1438 -- with MinSUP.x<sup spd ? -- (subst (λ k → odef _ k ) (sym &iso) zy)
1439 -- ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso y=p )
1440 -- ... | case2 y<p = case2 (subst (λ k → * y < k ) (sym *iso) y<p )
1441 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
1443 y : Ordinal
1444 y = HasPrev.y hp
1445 z24 : y << d
1446 z24 = subst (λ k → y << k) (sym (HasPrev.x=fy hp)) ( proj1 (cf-is-<-monotonic nmx y (proj1 (HasPrev.ay hp) ) ))
1428 sd=d : supf d ≡ d 1447 sd=d : supf d ≡ d
1429 sd=d = ? 1448 sd=d = ZChain.sup=u zc (MinSUP.asm spd) (o<→≤ d<A) ⟪ is-sup , not-hasprev ⟫
1430 sc<d : supf c << d 1449 sc<d : supf c << d
1431 sc<d = ? where 1450 sc<d = ? where
1432 z21 = proj1 ( cf-is-<-monotonic nmx ? ? ) 1451 z21 = proj1 ( cf-is-<-monotonic nmx ? ? )
1433 sco<d : supf c o< supf d 1452 sco<d : supf c o< supf d
1434 sco<d = ? 1453 sco<d = ?