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

comparison OD.agda @ 348:08d94fec239c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Limit ordinal and possible OD bound
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 14 Jul 2020 07:59:17 +0900
parents 06f10815d0b3
children 811152bf2f47
comparison
equal deleted inserted replaced
347:cfecd05a4061 348:08d94fec239c
388 infinite' : ({x : HOD} → od→ord x o< next (odmax x)) → HOD 388 infinite' : ({x : HOD} → od→ord x o< next (odmax x)) → HOD
389 infinite' ho< = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma } where 389 infinite' ho< = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma } where
390 u : (y : Ordinal ) → HOD 390 u : (y : Ordinal ) → HOD
391 u y = Union (ord→od y , (ord→od y , ord→od y)) 391 u y = Union (ord→od y , (ord→od y , ord→od y))
392 lemma : {y : Ordinal} → infinite-d y → y o< next o∅ 392 lemma : {y : Ordinal} → infinite-d y → y o< next o∅
393 lemma {o∅} iφ = proj1 next-limit 393 lemma {o∅} iφ = x<nx
394 lemma (isuc {y} x) = lemma2 where 394 lemma (isuc {y} x) = lemma2 where
395 lemma0 : y o< next o∅ 395 lemma0 : y o< next o∅
396 lemma0 = lemma x 396 lemma0 = lemma x
397 lemma8 : od→ord (ord→od y , ord→od y) o< next (odmax (ord→od y , ord→od y)) 397 lemma8 : od→ord (ord→od y , ord→od y) o< next (odmax (ord→od y , ord→od y))
398 lemma8 = ho< 398 lemma8 = ho<