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

comparison OD.agda @ 201:a1a7caa8b305

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 Tue, 30 Jul 2019 01:12:24 +0900
parents 57be355d1336
children ed88384b5102
comparison
equal deleted inserted replaced
200:57be355d1336 201:a1a7caa8b305
566 choice-func' X ∋-p not = lemma-ord (od→ord X) (subst (λ k → <-not {X} k ) (sym diso) lemma-init ) 566 choice-func' X ∋-p not = lemma-ord (od→ord X) (subst (λ k → <-not {X} k ) (sym diso) lemma-init )
567 where 567 where
568 <-not : {X : OD {suc n}} → ( ox : Ordinal {suc n}) → Set (suc n) 568 <-not : {X : OD {suc n}} → ( ox : Ordinal {suc n}) → Set (suc n)
569 <-not {X} ox = ( y : Ordinal {suc n}) → ox o< osuc y → ¬ (X ∋ (ord→od y)) 569 <-not {X} ox = ( y : Ordinal {suc n}) → ox o< osuc y → ¬ (X ∋ (ord→od y))
570 ind : {x : OD} → ({y : OD} → x ∋ y → <-not {X} (od→ord y) → choiced X) → <-not {X} (od→ord x) → choiced X 570 ind : {x : OD} → ({y : OD} → x ∋ y → <-not {X} (od→ord y) → choiced X) → <-not {X} (od→ord x) → choiced X
571 ind {y} ψ nox with ∋-p X y 571 ind {x} ψ nox = lemma (od→ord x) nox where
572 ind {y} ψ nox | yes p = record { a-choice = y ; is-in = p } 572 lemma : (ox : Ordinal {suc n}) → <-not {X} ox → choiced X
573 ind {y} ψ nox | no ¬p = {!!} 573 lemma ox nox with ∋-p X (ord→od ox)
574 ... | yes p = record { a-choice = ord→od ox ; is-in = p }
575 lemma record { lv = Zero ; ord = (Φ 0) } nox | no ¬p = {!!}
576 lemma record { lv = lx ; ord = (OSuc lx ox) } nox | no ¬p = lemma record { lv = lx ; ord = ox } {!!}
577 lemma record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } nox | no ¬p = lemma record { lv = lx ; ord = Φ lx } lemma2 where
578 lemma2 : ( y : Ordinal {suc n}) → record { lv = lx ; ord = Φ lx } o< osuc y → ¬ (X ∋ (ord→od y))
579 lemma2 y lt = {!!}
574 lemma-ord : ( x : Ordinal {suc n} ) → (<-not {X} (od→ord (ord→od x))) → choiced X 580 lemma-ord : ( x : Ordinal {suc n} ) → (<-not {X} (od→ord (ord→od x))) → choiced X
575 lemma-ord x = ε-induction {n} {suc (suc n)} { λ x → (<-not {X} (od→ord x)) → choiced X} ind (ord→od x) 581 lemma-ord x = ε-induction {n} {suc (suc n)} { λ x → (<-not {X} (od→ord x)) → choiced X} ind (ord→od x)
576 lemma-init : (y : Ordinal) → od→ord X o< osuc y → ¬ (X ∋ ord→od y) 582 lemma-init : (y : Ordinal) → od→ord X o< osuc y → ¬ (X ∋ ord→od y)
577 lemma-init y lt lt2 with osuc-≡< lt 583 lemma-init y lt lt2 with osuc-≡< lt
578 lemma-init y lt lt2 | case1 refl = o<¬≡ refl ( o<-subst (c<→o< {suc n} {_} {X} lt2) diso refl ) 584 lemma-init y lt lt2 | case1 refl = o<¬≡ refl ( o<-subst (c<→o< {suc n} {_} {X} lt2) diso refl )