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

comparison src/zorn.agda @ 961:811135ad1904

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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