Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff Ordinals.agda @ 347:cfecd05a4061
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 13 Jul 2020 22:40:37 +0900 |
parents | 06f10815d0b3 |
children | 08d94fec239c |
line wrap: on
line diff
--- a/Ordinals.agda Mon Jul 13 19:19:02 2020 +0900 +++ b/Ordinals.agda Mon Jul 13 22:40:37 2020 +0900 @@ -244,18 +244,22 @@ nexto≡ {x} | tri> ¬a ¬b c = ⊥-elim ((proj2 (proj2 next-limit)) _ (ordtrans <-osuc (proj1 next-limit)) c (λ z eq → o<¬≡ (sym eq) ((proj1 (proj2 next-limit)) _ (osuc< (sym eq))))) + record prev-choiced ( x : Ordinal ) : Set (suc n) where + field + prev : Ordinal + is-prev : osuc prev ≡ x not-limit-p : ( x : Ordinal ) → Dec ( ¬ ((y : Ordinal) → ¬ (x ≡ osuc y) )) - not-limit-p x = TransFinite {λ x → Dec ( ¬ ((y : Ordinal) → ¬ (x ≡ osuc y)))} ind x where - ind : (x : Ordinal) → ((y : Ordinal) → y o< x → Dec (¬ ((y₁ : Ordinal) → ¬ y ≡ osuc y₁))) → Dec (¬ ((y : Ordinal) → ¬ x ≡ osuc y)) - ind x prev with trio< o∅ x - ind x prev | tri< a ¬b ¬c = ? - ind x prev | tri≈ ¬a refl ¬c = no (λ not → not lemma) where - lemma : (y : Ordinal) → o∅ ≡ osuc y → ⊥ - lemma y refl with trio< o∅ y - lemma y refl | tri< a ¬b ¬c = o<> a <-osuc - lemma y refl | tri≈ ¬a b ¬c = o<¬≡ (sym b) <-osuc - lemma y refl | tri> ¬a ¬b c = ¬x<0 c - ind x prev | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c ) + not-limit-p x = {!!} where + ψ : ( ox : Ordinal ) → Set (suc n) + ψ ox = (( y : Ordinal ) → y o< ox → ( ¬ (osuc y ≡ x) )) ∨ prev-choiced x + ind : (ox : Ordinal) → ((y : Ordinal) → y o< ox → ψ y) → ψ ox + ind ox prev with trio< (osuc ox) x + ind ox prev | tri≈ ¬a b ¬c = case2 (record { prev = ox ; is-prev = b }) + ind ox prev | tri< a ¬b ¬c = case1 (λ y y<ox oy=x → o<> (subst (λ k → k o< osuc ox) oy=x (osucc y<ox )) a ) + -- osuc y = x < osuc ox, y < ox + ind ox prev | tri> ¬a ¬b c = {!!} + find : (y : Ordinal) → ψ y + find ox = TransFinite1 {ψ} ind ox record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where field