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

comparison OD.agda @ 358:811152bf2f47

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, 14 Jul 2020 12:39:21 +0900
parents 08d94fec239c
children 2a8a51375e49
comparison
equal deleted inserted replaced
357:d74a5a4df1b7 358:811152bf2f47
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φ = x<nx 393 lemma {o∅} iφ = x<nx
394 lemma (isuc {y} x) = lemma2 where 394 lemma (isuc {y} x) = lemma2 where
395 -- next< : {x y z : Ordinal} → x o< next z → y o< next x → y o< next z
395 lemma0 : y o< next o∅ 396 lemma0 : y o< next o∅
396 lemma0 = lemma x 397 lemma0 = lemma x
397 lemma8 : od→ord (ord→od y , ord→od y) o< next (odmax (ord→od y , ord→od y)) 398 lemma8 : od→ord (ord→od y , ord→od y) o< next (odmax (ord→od y , ord→od y))
398 lemma8 = ho< 399 lemma8 = ho<
399 --- (x,y) < next (omax x y) < next (osuc y) = next y 400 --- (x,y) < next (omax x y) < next (osuc y) = next y