Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison OD.agda @ 340:639fbb6284d8
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 13 Jul 2020 09:26:34 +0900 |
parents | feb0fcc430a9 |
children | 27d2933c4bd7 |
comparison
equal
deleted
inserted
replaced
339:feb0fcc430a9 | 340:639fbb6284d8 |
---|---|
385 lemma0 = lemma x | 385 lemma0 = lemma x |
386 lemma3 : odef (u y ) y | 386 lemma3 : odef (u y ) y |
387 lemma3 = FExists _ (λ {z} t not → not (od→ord (ord→od y , ord→od y)) record { proj1 = case2 refl ; proj2 = lemma4 }) (λ not → not y (infinite-d y)) where | 387 lemma3 = FExists _ (λ {z} t not → not (od→ord (ord→od y , ord→od y)) record { proj1 = case2 refl ; proj2 = lemma4 }) (λ not → not y (infinite-d y)) where |
388 lemma4 : def (od (ord→od (od→ord (ord→od y , ord→od y)))) y | 388 lemma4 : def (od (ord→od (od→ord (ord→od y , ord→od y)))) y |
389 lemma4 = subst₂ ( λ j k → def (od j) k ) (sym oiso) diso (case1 refl) | 389 lemma4 = subst₂ ( λ j k → def (od j) k ) (sym oiso) diso (case1 refl) |
390 lemma5 : y o< odmax (u y) | |
391 lemma5 = <odmax (u y) lemma3 | |
392 lemma6 : y o< odmax (ord→od y , (ord→od y , ord→od y)) | |
393 lemma6 = <odmax (ord→od y , (ord→od y , ord→od y)) (subst ( λ k → def (od (ord→od y , (ord→od y , ord→od y))) k ) diso (case1 refl)) | |
394 lemma8 : od→ord (ord→od y , ord→od y) o< next (odmax (ord→od y , ord→od y)) | |
395 lemma8 = ho< | |
396 lemma81 : od→ord (ord→od y , ord→od y) o< next (od→ord (ord→od y)) | |
397 lemma81 = nexto=n (subst (λ k → od→ord (ord→od y , ord→od y) o< k ) (cong (λ k → next k) (omxx _)) lemma8) | |
398 lemma7 : od→ord (ord→od y , (ord→od y , ord→od y)) o< next (odmax (ord→od y , (ord→od y , ord→od y))) | |
399 lemma91 : od→ord (ord→od y) o< od→ord (ord→od y , ord→od y) | |
400 lemma91 = c<→o< (case1 refl) | |
401 lemma92 : od→ord (ord→od y , (ord→od y , ord→od y)) o< next y | |
402 lemma92 = {!!} | |
403 lemma9 : od→ord (ord→od y , (ord→od y , ord→od y)) o< next (od→ord (ord→od y , ord→od y)) | |
404 lemma9 = next< {!!} lemma92 | |
405 lemma7 = ho< | |
406 lemma71 : od→ord (ord→od y , (ord→od y , ord→od y)) o< next (od→ord (ord→od y)) | |
407 lemma71 = next< lemma81 lemma9 | |
390 lemma1 : od→ord (u y) o< next (osuc (od→ord (ord→od y , (ord→od y , ord→od y)))) | 408 lemma1 : od→ord (u y) o< next (osuc (od→ord (ord→od y , (ord→od y , ord→od y)))) |
391 lemma1 = ho< | 409 lemma1 = ho< |
392 lemma2 : od→ord (u y) o< next o∅ | 410 lemma2 : od→ord (u y) o< next o∅ |
393 lemma2 = {!!} | 411 lemma2 = next< lemma0 (next< (subst (λ k → od→ord (ord→od y , (ord→od y , ord→od y)) o< next k) diso lemma71 ) (nexto=n lemma1)) |
394 | 412 |
395 | 413 |
396 _=h=_ : (x y : HOD) → Set n | 414 _=h=_ : (x y : HOD) → Set n |
397 x =h= y = od x == od y | 415 x =h= y = od x == od y |
398 | 416 |