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

comparison OD.agda @ 321:a81824502ebd

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 Fri, 03 Jul 2020 22:22:59 +0900
parents 21203fe0342f
children a9d380378efd
comparison
equal deleted inserted replaced
320:21203fe0342f 321:a81824502ebd
309 309
310 infinite : HOD 310 infinite : HOD
311 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma } where 311 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma } where
312 lemma : {y : Ordinal} → infinite-d y → y o< next o∅ 312 lemma : {y : Ordinal} → infinite-d y → y o< next o∅
313 lemma {o∅} iφ = proj1 next-limit 313 lemma {o∅} iφ = proj1 next-limit
314 lemma {n} (isuc i) = {!!} where 314 lemma (isuc {x} i) = lemma1 where -- proj2 next-limit ? ( lemma i )
315 lemma1 = proj2 next-limit 315 lemma1 : od→ord (Union (ord→od x , (ord→od x , ord→od x))) o< next o∅
316 lemma1 = ?
317
316 318
317 319
318 _=h=_ : (x y : HOD) → Set n 320 _=h=_ : (x y : HOD) → Set n
319 x =h= y = od x == od y 321 x =h= y = od x == od y
320 322