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

changeset 403:ce2ce3f62023

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 28 Jul 2020 10:51:08 +0900
parents d87492ae4040
children f7b844af9a50
files OD.agda
diffstat 1 files changed, 4 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/OD.agda	Tue Jul 28 10:32:33 2020 +0900
+++ b/OD.agda	Tue Jul 28 10:51:08 2020 +0900
@@ -519,9 +519,11 @@
                   (od→ord (ord→od x₁ , ord→od x₁))  record {proj1 = pair2 ; proj2 = subst (λ k → odef k (od→ord (ord→od x₁))) (sym oiso) pair1 } )
                lemma1 : infinite ∋ ord→od x₁
                lemma1 = subst (λ k → odef infinite k) (sym diso) ltd
+               lemma2 : {x₁ : Ordinal} → {ltd : infinite-d x₁ } → ω→nato ltd ≡ ω→nat (ord→od x₁) (subst (λ k → odef infinite k) (sym diso) ltd)
+               lemma2 {o∅} {iφ} = {!!}
+               lemma2 {x₁}  {isuc ltd} = cong (λ k → Suc k ) ( lemma2 {_} {ltd} )
                lemma :  nat→ω (ω→nato ltd) ≡ ord→od x₁
-               lemma with prev {ord→od x₁} lemma0 lemma1
-               ... | t = {!!}
+               lemma = trans  (cong (λ k →  nat→ω  k) lemma2) ( prev {ord→od x₁} lemma0 lemma1 )
 
 ψiso :  {ψ : HOD  → Set n} {x y : HOD } → ψ x → x ≡ y   → ψ y
 ψiso {ψ} t refl = t