Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff HOD.agda @ 180:11490a3170d4
new ordinal-definable
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 20 Jul 2019 14:05:32 +0900 |
parents | aa89d1b8ce96 |
children |
line wrap: on
line diff
--- a/HOD.agda Sat Jul 20 08:21:54 2019 +0900 +++ b/HOD.agda Sat Jul 20 14:05:32 2019 +0900 @@ -502,23 +502,20 @@ ≡⟨⟩ ly ∎ - lemma2 : { lx : Nat } → lx < Suc lx - lemma2 {Zero} = s≤s z≤n - lemma2 {Suc lx} = s≤s (lemma2 {lx}) lemma : (z : OD) → ord→od record { lv = ly ; ord = oy } ∋ z → ψ z lemma z lt with c<→o< {suc n} {z} {ord→od (record { lv = ly ; ord = oy })} lt lemma z lt | case1 lz<ly with <-cmp lx ly lemma z lt | case1 lz<ly | tri< a ¬b ¬c = ⊥-elim ( lemma0 y<sox a) -- can't happen - lemma z lt | case1 lz<ly | tri≈ ¬a refl ¬c = -- (1) + lemma z lt | case1 lz<ly | tri≈ ¬a refl ¬c = -- ly(1) subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (subst (λ k → lv (od→ord z) < k ) lemma1 lz<ly ) )) - lemma z lt | case1 lz<ly | tri> ¬a ¬b c = -- z(a) + lemma z lt | case1 lz<ly | tri> ¬a ¬b c = -- lz(a) subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (<-trans lz<ly (subst (λ k → k < lx ) (sym lemma1) c)))) lemma z lt | case2 lz=ly with <-cmp lx ly lemma z lt | case2 lz=ly | tri< a ¬b ¬c = ⊥-elim ( lemma0 y<sox a) -- can't happen - lemma z lt | case2 lz=ly | tri> ¬a ¬b c with d<→lv lz=ly -- z(b) + lemma z lt | case2 lz=ly | tri> ¬a ¬b c with d<→lv lz=ly -- lz(b) ... | eq = subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (subst (λ k → k < lx ) (trans (sym lemma1)(sym eq) ) c ))) - lemma z lt | case2 lz=ly | tri≈ ¬a lx=ly ¬c with d<→lv lz=ly -- z(c) + lemma z lt | case2 lz=ly | tri≈ ¬a lx=ly ¬c with d<→lv lz=ly -- lz(c) ... | eq = lemma6 {ly} {Φ lx} {oy} lx=ly (sym (subst (λ k → lv (od→ord z) ≡ k) lemma1 eq)) where lemma5 : (ox : OrdinalD lx) → (lv (od→ord z) < lx) ∨ (ord (od→ord z) d< ox) → ψ z lemma5 ox lt = subst (λ k → ψ k ) oiso (ε-induction-ord lx ox lt )