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

comparison OD.agda @ 343:34e71402d579

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 Mon, 13 Jul 2020 14:30:37 +0900
parents b1ccdbb14c92
children e0916a632971
comparison
equal deleted inserted replaced
342:b1ccdbb14c92 343:34e71402d579
220 x , y = record { od = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } ; odmax = omax (od→ord x) (od→ord y) ; <odmax = lemma } where 220 x , y = record { od = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } ; odmax = omax (od→ord x) (od→ord y) ; <odmax = lemma } where
221 lemma : {t : Ordinal} → (t ≡ od→ord x) ∨ (t ≡ od→ord y) → t o< omax (od→ord x) (od→ord y) 221 lemma : {t : Ordinal} → (t ≡ od→ord x) ∨ (t ≡ od→ord y) → t o< omax (od→ord x) (od→ord y)
222 lemma {t} (case1 refl) = omax-x _ _ 222 lemma {t} (case1 refl) = omax-x _ _
223 lemma {t} (case2 refl) = omax-y _ _ 223 lemma {t} (case2 refl) = omax-y _ _
224 224
225 pair-xx<xy : {x y : HOD} → od→ord (x , x) o< osuc (od→ord (x , y) )
226 pair-xx<xy {x} {y} = ⊆→o≤ lemma where
227 lemma : {z : Ordinal} → def (od (x , x)) z → def (od (x , y)) z
228 lemma {z} (case1 refl) = case1 refl
229 lemma {z} (case2 refl) = case1 refl
230
225 -- another form of infinite 231 -- another form of infinite
226 pair-ord< : {x : Ordinal } → Set n 232 -- pair-ord< : {x : Ordinal } → Set n
227 pair-ord< {x} = od→ord ( ord→od x , ord→od x ) o< next x 233 pair-ord< : {x : HOD } → ( {y : HOD } → od→ord y o< next (odmax y) ) → od→ord ( x , x ) o< next (od→ord x)
234 pair-ord< {x} ho< = subst (λ k → od→ord (x , x) o< k ) lemmab0 lemmab1 where
235 lemmab0 : next (odmax (x , x)) ≡ next (od→ord x)
236 lemmab0 = trans (cong (λ k → next k) (omxx _)) (sym nexto≡)
237 lemmab1 : od→ord (x , x) o< next ( odmax (x , x))
238 lemmab1 = ho<
228 239
229 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 240 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
230 -- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n (suc n) 241 -- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n (suc n)
231 242
232 in-codomain : (X : HOD ) → ( ψ : HOD → HOD ) → OD 243 in-codomain : (X : HOD ) → ( ψ : HOD → HOD ) → OD
391 lemma5 = <odmax (u y) lemma3 402 lemma5 = <odmax (u y) lemma3
392 lemma6 : y o< odmax (ord→od y , (ord→od y , ord→od y)) 403 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)) 404 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)) 405 lemma8 : od→ord (ord→od y , ord→od y) o< next (odmax (ord→od y , ord→od y))
395 lemma8 = ho< 406 lemma8 = ho<
396 lemmab : {x : HOD} → od→ord (x , x) o< next (od→ord x) 407 --- (x,y) < next (omax x y) < next (osuc y) = next y
397 lemmab {x} = subst (λ k → od→ord (x , x) o< k ) lemmab0 lemmab1 where
398 lemmab0 : next (odmax (x , x)) ≡ next (od→ord x)
399 lemmab0 = trans (cong (λ k → next k) (omxx _)) (sym nexto≡)
400 lemmab1 : od→ord (x , x) o< next ( odmax (x , x))
401 lemmab1 = ho<
402 lemmac : {x y : HOD} → od→ord x o< od→ord y → od→ord (x , y) o< od→ord (y , y)
403 lemmac = {!!}
404 lemmaa : {x y : HOD} → od→ord x o< od→ord y → od→ord (x , y) o< next (od→ord y) 408 lemmaa : {x y : HOD} → od→ord x o< od→ord y → od→ord (x , y) o< next (od→ord y)
405 lemmaa x<y = ordtrans (lemmac x<y) lemmab 409 lemmaa {x} {y} x<y = subst (λ k → od→ord (x , y) o< k ) (sym nexto≡) (subst (λ k → od→ord (x , y) o< next k ) (sym (omax< _ _ x<y)) ho< )
406 lemma81 : od→ord (ord→od y , ord→od y) o< next (od→ord (ord→od y)) 410 lemma81 : od→ord (ord→od y , ord→od y) o< next (od→ord (ord→od y))
407 lemma81 = nexto=n (subst (λ k → od→ord (ord→od y , ord→od y) o< k ) (cong (λ k → next k) (omxx _)) lemma8) 411 lemma81 = nexto=n (subst (λ k → od→ord (ord→od y , ord→od y) o< k ) (cong (λ k → next k) (omxx _)) lemma8)
408 lemma91 : od→ord (ord→od y) o< od→ord (ord→od y , ord→od y) 412 lemma91 : od→ord (ord→od y) o< od→ord (ord→od y , ord→od y)
409 lemma91 = c<→o< (case1 refl) 413 lemma91 = c<→o< (case1 refl)
410 lemma9 : od→ord (ord→od y , (ord→od y , ord→od y)) o< next (od→ord (ord→od y , ord→od y)) 414 lemma9 : od→ord (ord→od y , (ord→od y , ord→od y)) o< next (od→ord (ord→od y , ord→od y))