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

comparison OD.agda @ 316:c030a9655e79

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 Fri, 03 Jul 2020 16:51:44 +0900
parents 35e1214fa093
children 57df07b63cae
comparison
equal deleted inserted replaced
315:35e1214fa093 316:c030a9655e79
443 lemma9 : def (od (Ord (Ordinals.osuc O (od→ord (Ord (od→ord A)))))) (od→ord (Ord (od→ord A))) 443 lemma9 : def (od (Ord (Ordinals.osuc O (od→ord (Ord (od→ord A)))))) (od→ord (Ord (od→ord A)))
444 lemma9 = <-osuc 444 lemma9 = <-osuc
445 lemmab : od→ord (ZFSubset (Ord (od→ord A)) (ord→od (od→ord (Ord (od→ord A) )))) o< sup1 445 lemmab : od→ord (ZFSubset (Ord (od→ord A)) (ord→od (od→ord (Ord (od→ord A) )))) o< sup1
446 lemmab = sup-o< (Ord (osuc (od→ord (Ord (od→ord A))))) lemma9 446 lemmab = sup-o< (Ord (osuc (od→ord (Ord (od→ord A))))) lemma9
447 lemmad : Ord (osuc (od→ord A)) ∋ t 447 lemmad : Ord (osuc (od→ord A)) ∋ t
448 lemmad = subst (λ k → k o< osuc (od→ord A)) {!!} {!!} -- ( ⊆→o≤ {ord→od (od→ord t)} {ord→od (od→ord (Ord (od→ord t)))} (λ {x} lt → {!!} ) ) 448 lemmad = {!!}
449 lemmac : ZFSubset (Ord (od→ord A)) (ord→od (od→ord (Ord (od→ord A) ))) =h= Ord (od→ord A) 449 lemmac : ZFSubset (Ord (od→ord A)) (ord→od (od→ord (Ord (od→ord A) ))) =h= Ord (od→ord A)
450 lemmac = record { eq→ = {!!} ; eq← = {!!} } 450 lemmac = record { eq→ = {!!} ; eq← = {!!} }
451 lemmae : od→ord (ZFSubset (Ord (od→ord A)) (ord→od (od→ord (Ord (od→ord A))))) ≡ od→ord (Ord (od→ord A)) 451 lemmae : od→ord (ZFSubset (Ord (od→ord A)) (ord→od (od→ord (Ord (od→ord A))))) ≡ od→ord (Ord (od→ord A))
452 lemmae = cong (λ k → od→ord k ) ( ==→o≡ lemmac) 452 lemmae = cong (λ k → od→ord k ) ( ==→o≡ lemmac)
453 lemma7 : def (od (OPwr (Ord (od→ord A)))) (od→ord t) 453 lemma7 : def (od (OPwr (Ord (od→ord A)))) (od→ord t)
454 lemma7 with osuc-≡< lemmad 454 lemma7 with osuc-≡< lemmad
455 lemma7 | case2 lt = ordtrans (c<→o< lt) (subst (λ k → k o< sup1) lemmae lemmab ) 455 lemma7 | case2 lt = ordtrans (c<→o< lt) (subst (λ k → k o< sup1) lemmae lemmab )
456 lemma7 | case1 eq with osuc-≡< lemmad 456 lemma7 | case1 eq with osuc-≡< (⊆→o≤ {ord→od (od→ord t)} {ord→od (od→ord (Ord (od→ord t)))} (λ {x} lt → {!!} ))
457 lemma7 | case1 eq | case1 eq1 = subst (λ k → k o< sup1) (trans lemmae {!!}) lemmab -- od→ord (Ord (od→ord A)) ≡ od→ord t 457 lemma7 | case1 eq | case1 eq1 = subst (λ k → k o< sup1) (trans lemmae {!!}) lemmab -- od→ord (Ord (od→ord A)) ≡ od→ord t
458 lemma7 | case1 eq | case2 lt = ordtrans {!!} (subst (λ k → k o< sup1) lemmae lemmab ) 458 lemma7 | case1 eq | case2 lt = ordtrans {!!} (subst (λ k → k o< sup1) lemmae lemmab )
459 lemma1 : od→ord t o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x))) 459 lemma1 : od→ord t o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x)))
460 lemma1 = subst (λ k → od→ord k o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x)))) 460 lemma1 = subst (λ k → od→ord k o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x))))
461 lemma4 (sup-o< (OPwr (Ord (od→ord A))) lemma7 ) 461 lemma4 (sup-o< (OPwr (Ord (od→ord A))) lemma7 )