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

comparison HOD.agda @ 180:11490a3170d4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
new ordinal-definable
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 20 Jul 2019 14:05:32 +0900
parents aa89d1b8ce96
children
comparison
equal deleted inserted replaced
179:aa89d1b8ce96 180:11490a3170d4
500 ≡⟨ cong ( λ k → lv k ) diso ⟩ 500 ≡⟨ cong ( λ k → lv k ) diso ⟩
501 lv (record { lv = ly ; ord = oy }) 501 lv (record { lv = ly ; ord = oy })
502 ≡⟨⟩ 502 ≡⟨⟩
503 ly 503 ly
504 ∎ 504 ∎
505 lemma2 : { lx : Nat } → lx < Suc lx
506 lemma2 {Zero} = s≤s z≤n
507 lemma2 {Suc lx} = s≤s (lemma2 {lx})
508 lemma : (z : OD) → ord→od record { lv = ly ; ord = oy } ∋ z → ψ z 505 lemma : (z : OD) → ord→od record { lv = ly ; ord = oy } ∋ z → ψ z
509 lemma z lt with c<→o< {suc n} {z} {ord→od (record { lv = ly ; ord = oy })} lt 506 lemma z lt with c<→o< {suc n} {z} {ord→od (record { lv = ly ; ord = oy })} lt
510 lemma z lt | case1 lz<ly with <-cmp lx ly 507 lemma z lt | case1 lz<ly with <-cmp lx ly
511 lemma z lt | case1 lz<ly | tri< a ¬b ¬c = ⊥-elim ( lemma0 y<sox a) -- can't happen 508 lemma z lt | case1 lz<ly | tri< a ¬b ¬c = ⊥-elim ( lemma0 y<sox a) -- can't happen
512 lemma z lt | case1 lz<ly | tri≈ ¬a refl ¬c = -- (1) 509 lemma z lt | case1 lz<ly | tri≈ ¬a refl ¬c = -- ly(1)
513 subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (subst (λ k → lv (od→ord z) < k ) lemma1 lz<ly ) )) 510 subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (subst (λ k → lv (od→ord z) < k ) lemma1 lz<ly ) ))
514 lemma z lt | case1 lz<ly | tri> ¬a ¬b c = -- z(a) 511 lemma z lt | case1 lz<ly | tri> ¬a ¬b c = -- lz(a)
515 subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (<-trans lz<ly (subst (λ k → k < lx ) (sym lemma1) c)))) 512 subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (<-trans lz<ly (subst (λ k → k < lx ) (sym lemma1) c))))
516 lemma z lt | case2 lz=ly with <-cmp lx ly 513 lemma z lt | case2 lz=ly with <-cmp lx ly
517 lemma z lt | case2 lz=ly | tri< a ¬b ¬c = ⊥-elim ( lemma0 y<sox a) -- can't happen 514 lemma z lt | case2 lz=ly | tri< a ¬b ¬c = ⊥-elim ( lemma0 y<sox a) -- can't happen
518 lemma z lt | case2 lz=ly | tri> ¬a ¬b c with d<→lv lz=ly -- z(b) 515 lemma z lt | case2 lz=ly | tri> ¬a ¬b c with d<→lv lz=ly -- lz(b)
519 ... | eq = subst (λ k → ψ k ) oiso 516 ... | eq = subst (λ k → ψ k ) oiso
520 (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (subst (λ k → k < lx ) (trans (sym lemma1)(sym eq) ) c ))) 517 (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (subst (λ k → k < lx ) (trans (sym lemma1)(sym eq) ) c )))
521 lemma z lt | case2 lz=ly | tri≈ ¬a lx=ly ¬c with d<→lv lz=ly -- z(c) 518 lemma z lt | case2 lz=ly | tri≈ ¬a lx=ly ¬c with d<→lv lz=ly -- lz(c)
522 ... | eq = lemma6 {ly} {Φ lx} {oy} lx=ly (sym (subst (λ k → lv (od→ord z) ≡ k) lemma1 eq)) where 519 ... | eq = lemma6 {ly} {Φ lx} {oy} lx=ly (sym (subst (λ k → lv (od→ord z) ≡ k) lemma1 eq)) where
523 lemma5 : (ox : OrdinalD lx) → (lv (od→ord z) < lx) ∨ (ord (od→ord z) d< ox) → ψ z 520 lemma5 : (ox : OrdinalD lx) → (lv (od→ord z) < lx) ∨ (ord (od→ord z) d< ox) → ψ z
524 lemma5 ox lt = subst (λ k → ψ k ) oiso (ε-induction-ord lx ox lt ) 521 lemma5 ox lt = subst (λ k → ψ k ) oiso (ε-induction-ord lx ox lt )
525 lemma6 : { ly : Nat } { ox : OrdinalD {suc n} lx } { oy : OrdinalD {suc n} ly } → 522 lemma6 : { ly : Nat } { ox : OrdinalD {suc n} lx } { oy : OrdinalD {suc n} ly } →
526 lx ≡ ly → ly ≡ lv (od→ord z) → ψ z 523 lx ≡ ly → ly ≡ lv (od→ord z) → ψ z