Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff Ordinals.agda @ 339:feb0fcc430a9
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 12 Jul 2020 19:55:37 +0900 |
parents | bca043423554 |
children | 639fbb6284d8 |
line wrap: on
line diff
--- a/Ordinals.agda Sun Jul 12 12:32:42 2020 +0900 +++ b/Ordinals.agda Sun Jul 12 19:55:37 2020 +0900 @@ -21,7 +21,8 @@ <-osuc : { x : ord } → x o< osuc x osuc-≡< : { a x : ord } → x o< osuc a → (x ≡ a ) ∨ (x o< a) not-limit : ( x : ord ) → Dec ( ¬ ((y : ord) → ¬ (x ≡ osuc y) )) - next-limit : { y : ord } → (y o< next y ) ∧ ((x : ord) → x o< next y → osuc x o< next y ) + next-limit : { y : ord } → (y o< next y ) ∧ ((x : ord) → x o< next y → osuc x o< next y ) ∧ + ( (x : ord) → y o< x → x o< next y → ¬ ((z : ord) → ¬ (x ≡ osuc z) )) TransFinite : { ψ : ord → Set n } → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x ) → ∀ (x : ord) → ψ x @@ -219,6 +220,14 @@ → ¬ p FExists {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) + next< : {x y z : Ordinal} → x o< next z → y o< next x → y o< next z + next< {x} {y} {z} x<nz y<nx with trio< y (next z) + next< {x} {y} {z} x<nz y<nx | tri< a ¬b ¬c = a + next< {x} {y} {z} x<nz y<nx | tri≈ ¬a b ¬c = ⊥-elim ((proj2 (proj2 next-limit)) (next z) x<nz (subst (λ k → k o< next x) b y<nx) + (λ w nz=ow → o<¬≡ nz=ow (subst₂ (λ j k → j o< k ) (sym nz=ow) nz=ow (proj1 (proj2 next-limit) w (subst (λ k → w o< k ) (sym nz=ow) <-osuc) )))) + next< {x} {y} {z} x<nz y<nx | tri> ¬a ¬b c = ⊥-elim (proj2 (proj2 next-limit) (next z) x<nz (ordtrans c y<nx ) + (λ w nz=ow → o<¬≡ (sym nz=ow) (proj1 (proj2 next-limit) _ (subst (λ k → w o< k ) (sym nz=ow) <-osuc )))) + record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where field os→ : (x : Ordinal) → x o< maxordinal → Ordinal