Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison 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 |
comparison
equal
deleted
inserted
replaced
| 338:bca043423554 | 339:feb0fcc430a9 |
|---|---|
| 19 OTri : Trichotomous {n} _≡_ _o<_ | 19 OTri : Trichotomous {n} _≡_ _o<_ |
| 20 ¬x<0 : { x : ord } → ¬ ( x o< o∅ ) | 20 ¬x<0 : { x : ord } → ¬ ( x o< o∅ ) |
| 21 <-osuc : { x : ord } → x o< osuc x | 21 <-osuc : { x : ord } → x o< osuc x |
| 22 osuc-≡< : { a x : ord } → x o< osuc a → (x ≡ a ) ∨ (x o< a) | 22 osuc-≡< : { a x : ord } → x o< osuc a → (x ≡ a ) ∨ (x o< a) |
| 23 not-limit : ( x : ord ) → Dec ( ¬ ((y : ord) → ¬ (x ≡ osuc y) )) | 23 not-limit : ( x : ord ) → Dec ( ¬ ((y : ord) → ¬ (x ≡ osuc y) )) |
| 24 next-limit : { y : ord } → (y o< next y ) ∧ ((x : ord) → x o< next y → osuc x o< next y ) | 24 next-limit : { y : ord } → (y o< next y ) ∧ ((x : ord) → x o< next y → osuc x o< next y ) ∧ |
| 25 ( (x : ord) → y o< x → x o< next y → ¬ ((z : ord) → ¬ (x ≡ osuc z) )) | |
| 25 TransFinite : { ψ : ord → Set n } | 26 TransFinite : { ψ : ord → Set n } |
| 26 → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x ) | 27 → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x ) |
| 27 → ∀ (x : ord) → ψ x | 28 → ∀ (x : ord) → ψ x |
| 28 TransFinite1 : { ψ : ord → Set (suc n) } | 29 TransFinite1 : { ψ : ord → Set (suc n) } |
| 29 → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x ) | 30 → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x ) |
| 217 → {p : Set l} ( P : { y : Ordinal } → ψ y → ¬ p ) | 218 → {p : Set l} ( P : { y : Ordinal } → ψ y → ¬ p ) |
| 218 → (exists : ¬ (∀ y → ¬ ( ψ y ) )) | 219 → (exists : ¬ (∀ y → ¬ ( ψ y ) )) |
| 219 → ¬ p | 220 → ¬ p |
| 220 FExists {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) | 221 FExists {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) |
| 221 | 222 |
| 223 next< : {x y z : Ordinal} → x o< next z → y o< next x → y o< next z | |
| 224 next< {x} {y} {z} x<nz y<nx with trio< y (next z) | |
| 225 next< {x} {y} {z} x<nz y<nx | tri< a ¬b ¬c = a | |
| 226 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) | |
| 227 (λ 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) )))) | |
| 228 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 ) | |
| 229 (λ w nz=ow → o<¬≡ (sym nz=ow) (proj1 (proj2 next-limit) _ (subst (λ k → w o< k ) (sym nz=ow) <-osuc )))) | |
| 230 | |
| 222 record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where | 231 record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where |
| 223 field | 232 field |
| 224 os→ : (x : Ordinal) → x o< maxordinal → Ordinal | 233 os→ : (x : Ordinal) → x o< maxordinal → Ordinal |
| 225 os← : Ordinal → Ordinal | 234 os← : Ordinal → Ordinal |
| 226 os←limit : (x : Ordinal) → os← x o< maxordinal | 235 os←limit : (x : Ordinal) → os← x o< maxordinal |