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