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

comparison HOD.agda @ 137:c7c9f3efc428

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
replace using Select
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 07 Jul 2019 08:56:25 +0900
parents 3cc848664a86
children 567084f2278f
comparison
equal deleted inserted replaced
136:3cc848664a86 137:c7c9f3efc428
306 in-codomain {n} X ψ = record { def = λ x → ¬ ( (y : Ordinal {suc n}) → ¬ ( def X y ∧ ( x ≡ od→ord (ψ (Ord y ))))) 306 in-codomain {n} X ψ = record { def = λ x → ¬ ( (y : Ordinal {suc n}) → ¬ ( def X y ∧ ( x ≡ od→ord (ψ (Ord y )))))
307 ; otrans = lemma } where 307 ; otrans = lemma } where
308 lemma : {x : Ordinal} → ¬ ((y : Ordinal) → ¬ def X y ∧ (x ≡ od→ord (ψ (Ord y)))) → 308 lemma : {x : Ordinal} → ¬ ((y : Ordinal) → ¬ def X y ∧ (x ≡ od→ord (ψ (Ord y)))) →
309 {y : Ordinal} → y o< x → ¬ ((y₁ : Ordinal) → ¬ def X y₁ ∧ (y ≡ od→ord (ψ (Ord y₁)))) 309 {y : Ordinal} → y o< x → ¬ ((y₁ : Ordinal) → ¬ def X y₁ ∧ (y ≡ od→ord (ψ (Ord y₁))))
310 lemma {x} notx {y} y<x noty = notx ( λ z prod → noty z ( record { proj1 = proj1 prod ; proj2 = {!!} } )) 310 lemma {x} notx {y} y<x noty = notx ( λ z prod → noty z ( record { proj1 = proj1 prod ; proj2 = {!!} } ))
311 Replace' : HOD {suc n} → (HOD {suc n} → HOD {suc n} ) → HOD {suc n}
312 Replace' X ψ = Select ( Ord (sup-o ( λ x → od→ord (ψ (ord→od x ))))) ( λ x → ¬ (∀ (y : Ordinal ) → ¬ ( def X y ∧ ( x == ψ (Ord y) ))))
311 Replace : HOD {suc n} → (HOD {suc n} → HOD {suc n} ) → HOD {suc n} 313 Replace : HOD {suc n} → (HOD {suc n} → HOD {suc n} ) → HOD {suc n}
312 Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x ; 314 Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x ;
313 otrans = lemma } where 315 otrans = lemma } where
314 lemma : {x : Ordinal} → (x o< sup-o (λ x₁ → od→ord (ψ (ord→od x₁)))) ∧ def (in-codomain X ψ) x → 316 lemma : {x : Ordinal} → (x o< sup-o (λ x₁ → od→ord (ψ (ord→od x₁)))) ∧ def (in-codomain X ψ) x →
315 {y : Ordinal} → y o< x → (y o< sup-o (λ x₁ → od→ord (ψ (ord→od x₁)))) ∧ def (in-codomain X ψ) y 317 {y : Ordinal} → y o< x → (y o< sup-o (λ x₁ → od→ord (ψ (ord→od x₁)))) ∧ def (in-codomain X ψ) y