Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 929:a6d97e6e5309
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 22 Oct 2022 18:26:16 +0900 |
| parents | 330303f0c688 |
| children | 0e0608b1953b |
| files | src/zorn.agda |
| diffstat | 1 files changed, 20 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Sat Oct 22 11:15:17 2022 +0900 +++ b/src/zorn.agda Sat Oct 22 18:26:16 2022 +0900 @@ -1423,10 +1423,29 @@ d = MinSUP.sup spd d<A : d o< & A d<A = ∈∧P→o< ⟪ MinSUP.asm spd , lift true ⟫ + msup : MinSUP A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 supf d) + msup = ZChain.minsup zc (o<→≤ d<A) sd=ms : supf d ≡ MinSUP.sup ( ZChain.minsup zc (o<→≤ d<A) ) sd=ms = ZChain.supf-is-minsup zc (o<→≤ d<A) + is-sup : IsSup A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) (MinSUP.asm spd) + is-sup = record { x<sup = z22 } where + -- + z23 : {z : Ordinal } → odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc) z → (z ≡ MinSUP.sup spd) ∨ (z << MinSUP.sup spd) + z23 lt = MinSUP.x<sup spd lt + z22 : {y : Ordinal} → odef (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) y → + (y ≡ MinSUP.sup spd) ∨ (y << MinSUP.sup spd) + z22 {y} zy = ? + -- with MinSUP.x<sup spd ? -- (subst (λ k → odef _ k ) (sym &iso) zy) + -- ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso y=p ) + -- ... | case2 y<p = case2 (subst (λ k → * y < k ) (sym *iso) y<p ) + not-hasprev : ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) d (cf nmx) + not-hasprev hp = ? where + y : Ordinal + y = HasPrev.y hp + z24 : y << d + z24 = subst (λ k → y << k) (sym (HasPrev.x=fy hp)) ( proj1 (cf-is-<-monotonic nmx y (proj1 (HasPrev.ay hp) ) )) sd=d : supf d ≡ d - sd=d = ? + sd=d = ZChain.sup=u zc (MinSUP.asm spd) (o<→≤ d<A) ⟪ is-sup , not-hasprev ⟫ sc<d : supf c << d sc<d = ? where z21 = proj1 ( cf-is-<-monotonic nmx ? ? )