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

comparison OD.agda @ 320:21203fe0342f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
infinite ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 03 Jul 2020 21:58:01 +0900
parents eef432aa8dfb
children a81824502ebd
comparison
equal deleted inserted replaced
319:eef432aa8dfb 320:21203fe0342f
306 iφ : infinite-d o∅ 306 iφ : infinite-d o∅
307 isuc : {x : Ordinal } → infinite-d x → 307 isuc : {x : Ordinal } → infinite-d x →
308 infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) )) 308 infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) ))
309 309
310 infinite : HOD 310 infinite : HOD
311 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = {!!} ; <odmax = {!!} } 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∅
313 lemma {o∅} iφ = proj1 next-limit
314 lemma {n} (isuc i) = {!!} where
315 lemma1 = proj2 next-limit
316
312 317
313 _=h=_ : (x y : HOD) → Set n 318 _=h=_ : (x y : HOD) → Set n
314 x =h= y = od x == od y 319 x =h= y = od x == od y
315 320
316 infixr 200 _∈_ 321 infixr 200 _∈_