Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison src/zorn.agda @ 961:811135ad1904
supf sp = sp ?
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 04 Nov 2022 18:55:44 +0900 |
parents | b7370c39769e |
children | d594a8439174 |
comparison
equal
deleted
inserted
replaced
960:b7370c39769e | 961:811135ad1904 |
---|---|
480 pr = HasPrev.y hp | 480 pr = HasPrev.y hp |
481 im00 : f (f pr) <= sp | 481 im00 : f (f pr) <= sp |
482 im00 = is-sup ( f-next (f-next (HasPrev.ay hp))) | 482 im00 = is-sup ( f-next (f-next (HasPrev.ay hp))) |
483 fsp≤sp : f sp <= sp | 483 fsp≤sp : f sp <= sp |
484 fsp≤sp = subst (λ k → f k <= sp ) (sym (HasPrev.x=fy hp)) im00 | 484 fsp≤sp = subst (λ k → f k <= sp ) (sym (HasPrev.x=fy hp)) im00 |
485 | |
486 IsMinSUP< : ( {a : Ordinal } → a << f a ) | |
487 → {b x : Ordinal } → {ab : odef A b} → x o≤ z → b o< x | |
488 → IsMinSUP A (UnionCF A f mf ay supf x) f ab → IsMinSUP A (UnionCF A f mf ay supf b) f ab | |
489 IsMinSUP< <-mono-f {b} {x} {ab} x≤z b<x record { x≤sup = x≤sup ; minsup = minsup ; not-hp = nhp } | |
490 = record { x≤sup = m02 ; minsup = m07 ; not-hp = IsMinSUP→NotHasPrev ab m02 <-mono-f } where | |
491 m02 : {z : Ordinal} → odef (UnionCF A f mf ay supf b) z → (z ≡ b) ∨ (z << b) | |
492 m02 {z} uz = x≤sup (chain-mono f mf ay supf supf-mono (o<→≤ b<x) uz) | |
493 m10 : {s : Ordinal } → (odef A s ) | |
494 → ( {w : Ordinal} → odef (UnionCF A f mf ay supf b) w → (w ≡ s) ∨ (w << s) ) | |
495 → {w : Ordinal} → odef (UnionCF A f mf ay supf x) w → (w ≡ s) ∨ (w << s) | |
496 m10 {s} as b-is-sup ⟪ aa , ch-init fc ⟫ = ? | |
497 m10 {s} as b-is-sup ⟪ aa , ch-is-sup u {w} u<x is-sup-z fc ⟫ = m01 where | |
498 m01 : w <= s | |
499 m01 with trio< (supf u) (supf b) | |
500 ... | tri< a ¬b ¬c = b-is-sup ⟪ aa , ch-is-sup u {w} a is-sup-z fc ⟫ | |
501 ... | tri≈ ¬a b ¬c = ? | |
502 ... | tri> ¬a ¬b c = ? | |
503 m07 : {s : Ordinal} → odef A s → ({z : Ordinal} → | |
504 odef (UnionCF A f mf ay supf b) z → (z ≡ s) ∨ (z << s)) → b o≤ s | |
505 m07 {s} as b-is-sup = minsup as (m10 as b-is-sup ) | |
506 | 485 |
507 record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) | 486 record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) |
508 {y : Ordinal} (ay : odef A y) (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where | 487 {y : Ordinal} (ay : odef A y) (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where |
509 supf = ZChain.supf zc | 488 supf = ZChain.supf zc |
510 field | 489 field |
1397 z22 : sp o< & A | 1376 z22 : sp o< & A |
1398 z22 = z09 asp | 1377 z22 = z09 asp |
1399 z12 : odef chain sp | 1378 z12 : odef chain sp |
1400 z12 with o≡? (& s) sp | 1379 z12 with o≡? (& s) sp |
1401 ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc ) | 1380 ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc ) |
1402 ... | no ne = ZChain1.is-max (SZ1 f mf as0 zc (& A)) {& s} {sp} ( ZChain.chain∋init zc ) ssp<as asp | 1381 ... | no ne = ZChain1.is-max (SZ1 f mf as0 zc (& A)) {& s} {sp} ( ZChain.chain∋init zc ) ssp<as asp (case2 z19 ) z13 where |
1403 (case2 z19 ) z13 where | |
1404 z13 : * (& s) < * sp | 1382 z13 : * (& s) < * sp |
1405 z13 with MinSUP.x≤sup sp1 ( ZChain.chain∋init zc ) | 1383 z13 with MinSUP.x≤sup sp1 ( ZChain.chain∋init zc ) |
1406 ... | case1 eq = ⊥-elim ( ne eq ) | 1384 ... | case1 eq = ⊥-elim ( ne eq ) |
1407 ... | case2 lt = lt -- subst₂ (λ j k → j < k ) (sym *iso) (sym *iso) lt | 1385 ... | case2 lt = lt |
1408 z19 : IsMinSUP A (UnionCF A f mf as0 (ZChain.supf zc) sp) f asp | 1386 z19 : IsMinSUP A (UnionCF A f mf as0 (ZChain.supf zc) sp) f asp |
1409 z19 = record { x≤sup = z20 ; minsup = ? ; not-hp = ZChain.IsMinSUP→NotHasPrev zc ? z20 ? } where | 1387 z19 = record { x≤sup = z20 ; minsup = z21 ; not-hp = ZChain.IsMinSUP→NotHasPrev zc ? z20 ? } where |
1388 z23 : {z : Ordinal } → odef chain z → odef (UnionCF A f mf as0 (ZChain.supf zc) sp) z | |
1389 z23 {z} ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ | |
1390 z23 {z} ⟪ au , ch-is-sup u u<x is-sup fc ⟫ = ⟪ au , ch-is-sup u z24 is-sup fc ⟫ where | |
1391 z26 : supf sp <= sp | |
1392 z26 = MinSUP.x≤sup sp1 ⟪ ? | |
1393 , ch-is-sup sp ? ? (init (ZChain.asupf zc) ? ) ⟫ | |
1394 z25 : u <= sp | |
1395 z25 = MinSUP.x≤sup sp1 ⟪ subst (λ k → odef A k) (ChainP.supu=u is-sup) (ZChain.asupf zc) | |
1396 , ch-is-sup u u<x is-sup (init (ZChain.asupf zc) (ChainP.supu=u is-sup)) ⟫ | |
1397 z24 : supf u o< supf sp | |
1398 z24 = ? -- with ZChain.supf-<= zc z25 | |
1399 z21 : {sup1 : Ordinal} → odef A sup1 | |
1400 → ({z : Ordinal} → odef (UnionCF A f mf as0 (ZChain.supf zc) sp) z → (z ≡ sup1) ∨ (z << sup1)) | |
1401 → sp o≤ sup1 | |
1402 z21 {s} as s-sup = MinSUP.minsup sp1 as ( λ uz → s-sup (z23 uz) ) | |
1410 z20 : {y : Ordinal} → odef (UnionCF A f mf as0 (ZChain.supf zc) sp) y → (y ≡ sp) ∨ (y << sp) | 1403 z20 : {y : Ordinal} → odef (UnionCF A f mf as0 (ZChain.supf zc) sp) y → (y ≡ sp) ∨ (y << sp) |
1411 z20 {y} zy with MinSUP.x≤sup sp1 (subst (λ k → odef chain k ) (sym &iso) (chain-mono f mf as0 supf (ZChain.supf-mono zc) (o<→≤ z22) zy )) | 1404 z20 {y} zy with MinSUP.x≤sup sp1 |
1405 (subst (λ k → odef chain k ) (sym &iso) (chain-mono f mf as0 supf (ZChain.supf-mono zc) (o<→≤ z22) zy )) | |
1412 ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso y=p ) | 1406 ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso y=p ) |
1413 ... | case2 y<p = case2 (subst (λ k → * k < _ ) &iso y<p ) | 1407 ... | case2 y<p = case2 (subst (λ k → * k < _ ) &iso y<p ) |
1414 z14 : f sp ≡ sp | 1408 z14 : f sp ≡ sp |
1415 z14 with ZChain.f-total zc (subst (λ k → odef chain k) (sym &iso) (ZChain.f-next zc z12 )) (subst (λ k → odef chain k) (sym &iso) z12 ) | 1409 z14 with ZChain.f-total zc (subst (λ k → odef chain k) (sym &iso) (ZChain.f-next zc z12 )) (subst (λ k → odef chain k) (sym &iso) z12 ) |
1416 ... | tri< a ¬b ¬c = ⊥-elim z16 where | 1410 ... | tri< a ¬b ¬c = ⊥-elim z16 where |