Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison src/ordinal.agda @ 653:4186c0331abb
sind again
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 30 Jun 2022 06:57:05 +0900 |
parents | 099ca2fea51c |
children | a3b7f1e0ca60 |
comparison
equal
deleted
inserted
replaced
641:cf5af048db99 | 653:4186c0331abb |
---|---|
1 open import Level | 1 open import Level |
2 module ordinal where | 2 module ordinal where |
3 | 3 |
4 open import logic | 4 open import logic |
5 open import nat | 5 open import nat |
6 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) | 6 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; _⊔_ to _n⊔_ ) |
7 open import Data.Empty | 7 open import Data.Empty |
8 open import Relation.Binary.PropositionalEquality | 8 open import Relation.Binary.PropositionalEquality |
9 open import Relation.Binary.Definitions | 9 open import Relation.Binary.Definitions |
10 open import Data.Nat.Properties | 10 open import Data.Nat.Properties as NP |
11 open import Relation.Nullary | 11 open import Relation.Nullary |
12 open import Relation.Binary.Core | 12 open import Relation.Binary.Core |
13 | 13 |
14 ---- | 14 ---- |
15 -- | 15 -- |
16 -- Countable Ordinals | 16 -- Countable Ordinals |
17 -- | 17 -- |
18 | 18 |
19 data OrdinalD {n : Level} : (lv : Nat) → Set n where | 19 data OrdinalD {n : Level} : (lv : ℕ) → Set n where |
20 Φ : (lv : Nat) → OrdinalD lv | 20 Φ : (lv : ℕ) → OrdinalD lv |
21 OSuc : (lv : Nat) → OrdinalD {n} lv → OrdinalD lv | 21 OSuc : (lv : ℕ) → OrdinalD {n} lv → OrdinalD lv |
22 | 22 |
23 record Ordinal {n : Level} : Set n where | 23 record Ordinal {n : Level} : Set n where |
24 constructor ordinal | 24 constructor ordinal |
25 field | 25 field |
26 lv : Nat | 26 lv : ℕ |
27 ord : OrdinalD {n} lv | 27 ord : OrdinalD {n} lv |
28 | 28 |
29 data _d<_ {n : Level} : {lx ly : Nat} → OrdinalD {n} lx → OrdinalD {n} ly → Set n where | 29 data _d<_ {n : Level} : {lx ly : ℕ} → OrdinalD {n} lx → OrdinalD {n} ly → Set n where |
30 Φ< : {lx : Nat} → {x : OrdinalD {n} lx} → Φ lx d< OSuc lx x | 30 Φ< : {lx : ℕ} → {x : OrdinalD {n} lx} → Φ lx d< OSuc lx x |
31 s< : {lx : Nat} → {x y : OrdinalD {n} lx} → x d< y → OSuc lx x d< OSuc lx y | 31 s< : {lx : ℕ} → {x y : OrdinalD {n} lx} → x d< y → OSuc lx x d< OSuc lx y |
32 | 32 |
33 open Ordinal | 33 open Ordinal |
34 | 34 |
35 _o<_ : {n : Level} ( x y : Ordinal ) → Set n | 35 _o<_ : {n : Level} ( x y : Ordinal ) → Set n |
36 _o<_ x y = (lv x < lv y ) ∨ ( ord x d< ord y ) | 36 _o<_ x y = (lv x < lv y ) ∨ ( ord x d< ord y ) |
37 | 37 |
38 s<refl : {n : Level } {lx : Nat } { x : OrdinalD {n} lx } → x d< OSuc lx x | 38 s<refl : {n : Level } {lx : ℕ } { x : OrdinalD {n} lx } → x d< OSuc lx x |
39 s<refl {n} {lv} {Φ lv} = Φ< | 39 s<refl {n} {lv} {Φ lv} = Φ< |
40 s<refl {n} {lv} {OSuc lv x} = s< s<refl | 40 s<refl {n} {lv} {OSuc lv x} = s< s<refl |
41 | 41 |
42 trio<> : {n : Level} → {lx : Nat} {x : OrdinalD {n} lx } { y : OrdinalD lx } → y d< x → x d< y → ⊥ | 42 trio<> : {n : Level} → {lx : ℕ} {x : OrdinalD {n} lx } { y : OrdinalD lx } → y d< x → x d< y → ⊥ |
43 trio<> {n} {lx} {.(OSuc lx _)} {.(OSuc lx _)} (s< s) (s< t) = trio<> s t | 43 trio<> {n} {lx} {.(OSuc lx _)} {.(OSuc lx _)} (s< s) (s< t) = trio<> s t |
44 trio<> {n} {lx} {.(OSuc lx _)} {.(Φ lx)} Φ< () | 44 trio<> {n} {lx} {.(OSuc lx _)} {.(Φ lx)} Φ< () |
45 | 45 |
46 d<→lv : {n : Level} {x y : Ordinal {n}} → ord x d< ord y → lv x ≡ lv y | 46 d<→lv : {n : Level} {x y : Ordinal {n}} → ord x d< ord y → lv x ≡ lv y |
47 d<→lv Φ< = refl | 47 d<→lv Φ< = refl |
54 | 54 |
55 ordinal-cong : {n : Level} {x y : Ordinal {n}} → | 55 ordinal-cong : {n : Level} {x y : Ordinal {n}} → |
56 lv x ≡ lv y → ord x ≅ ord y → x ≡ y | 56 lv x ≡ lv y → ord x ≅ ord y → x ≡ y |
57 ordinal-cong refl refl = refl | 57 ordinal-cong refl refl = refl |
58 | 58 |
59 ≡→¬d< : {n : Level} → {lv : Nat} → {x : OrdinalD {n} lv } → x d< x → ⊥ | 59 ≡→¬d< : {n : Level} → {lv : ℕ} → {x : OrdinalD {n} lv } → x d< x → ⊥ |
60 ≡→¬d< {n} {lx} {OSuc lx y} (s< t) = ≡→¬d< t | 60 ≡→¬d< {n} {lx} {OSuc lx y} (s< t) = ≡→¬d< t |
61 | 61 |
62 trio<≡ : {n : Level} → {lx : Nat} {x : OrdinalD {n} lx } { y : OrdinalD lx } → x ≡ y → x d< y → ⊥ | 62 trio<≡ : {n : Level} → {lx : ℕ} {x : OrdinalD {n} lx } { y : OrdinalD lx } → x ≡ y → x d< y → ⊥ |
63 trio<≡ refl = ≡→¬d< | 63 trio<≡ refl = ≡→¬d< |
64 | 64 |
65 trio>≡ : {n : Level} → {lx : Nat} {x : OrdinalD {n} lx } { y : OrdinalD lx } → x ≡ y → y d< x → ⊥ | 65 trio>≡ : {n : Level} → {lx : ℕ} {x : OrdinalD {n} lx } { y : OrdinalD lx } → x ≡ y → y d< x → ⊥ |
66 trio>≡ refl = ≡→¬d< | 66 trio>≡ refl = ≡→¬d< |
67 | 67 |
68 triOrdd : {n : Level} → {lx : Nat} → Trichotomous _≡_ ( _d<_ {n} {lx} {lx} ) | 68 triOrdd : {n : Level} → {lx : ℕ} → Trichotomous _≡_ ( _d<_ {n} {lx} {lx} ) |
69 triOrdd {_} {lv} (Φ lv) (Φ lv) = tri≈ ≡→¬d< refl ≡→¬d< | 69 triOrdd {_} {lv} (Φ lv) (Φ lv) = tri≈ ≡→¬d< refl ≡→¬d< |
70 triOrdd {_} {lv} (Φ lv) (OSuc lv y) = tri< Φ< (λ ()) ( λ lt → trio<> lt Φ< ) | 70 triOrdd {_} {lv} (Φ lv) (OSuc lv y) = tri< Φ< (λ ()) ( λ lt → trio<> lt Φ< ) |
71 triOrdd {_} {lv} (OSuc lv x) (Φ lv) = tri> (λ lt → trio<> lt Φ<) (λ ()) Φ< | 71 triOrdd {_} {lv} (OSuc lv x) (Φ lv) = tri> (λ lt → trio<> lt Φ<) (λ ()) Φ< |
72 triOrdd {_} {lv} (OSuc lv x) (OSuc lv y) with triOrdd x y | 72 triOrdd {_} {lv} (OSuc lv x) (OSuc lv y) with triOrdd x y |
73 triOrdd {_} {lv} (OSuc lv x) (OSuc lv y) | tri< a ¬b ¬c = tri< (s< a) (λ tx=ty → trio<≡ tx=ty (s< a) ) ( λ lt → trio<> lt (s< a) ) | 73 triOrdd {_} {lv} (OSuc lv x) (OSuc lv y) | tri< a ¬b ¬c = tri< (s< a) (λ tx=ty → trio<≡ tx=ty (s< a) ) ( λ lt → trio<> lt (s< a) ) |
95 o<> {n} {x} {y} (case2 x₁) (case1 x₂) = nat-≡< (sym (d<→lv x₁)) x₂ | 95 o<> {n} {x} {y} (case2 x₁) (case1 x₂) = nat-≡< (sym (d<→lv x₁)) x₂ |
96 o<> {n} {record { lv = lv₁ ; ord = .(OSuc lv₁ _) }} {record { lv = .lv₁ ; ord = .(Φ lv₁) }} (case2 Φ<) (case2 ()) | 96 o<> {n} {record { lv = lv₁ ; ord = .(OSuc lv₁ _) }} {record { lv = .lv₁ ; ord = .(Φ lv₁) }} (case2 Φ<) (case2 ()) |
97 o<> {n} {record { lv = lv₁ ; ord = .(OSuc lv₁ _) }} {record { lv = .lv₁ ; ord = .(OSuc lv₁ _) }} (case2 (s< y<x)) (case2 (s< x<y)) = | 97 o<> {n} {record { lv = lv₁ ; ord = .(OSuc lv₁ _) }} {record { lv = .lv₁ ; ord = .(OSuc lv₁ _) }} (case2 (s< y<x)) (case2 (s< x<y)) = |
98 o<> (case2 y<x) (case2 x<y) | 98 o<> (case2 y<x) (case2 x<y) |
99 | 99 |
100 orddtrans : {n : Level} {lx : Nat} {x y z : OrdinalD {n} lx } → x d< y → y d< z → x d< z | 100 orddtrans : {n : Level} {lx : ℕ} {x y z : OrdinalD {n} lx } → x d< y → y d< z → x d< z |
101 orddtrans {_} {lx} {.(Φ lx)} {.(OSuc lx _)} {.(OSuc lx _)} Φ< (s< y<z) = Φ< | 101 orddtrans {_} {lx} {.(Φ lx)} {.(OSuc lx _)} {.(OSuc lx _)} Φ< (s< y<z) = Φ< |
102 orddtrans {_} {lx} {.(OSuc lx _)} {.(OSuc lx _)} {.(OSuc lx _)} (s< x<y) (s< y<z) = s< ( orddtrans x<y y<z ) | 102 orddtrans {_} {lx} {.(OSuc lx _)} {.(OSuc lx _)} {.(OSuc lx _)} (s< x<y) (s< y<z) = s< ( orddtrans x<y y<z ) |
103 | 103 |
104 osuc-≡< : {n : Level} { a x : Ordinal {n} } → x o< osuc a → (x ≡ a ) ∨ (x o< a) | 104 osuc-≡< : {n : Level} { a x : Ordinal {n} } → x o< osuc a → (x ≡ a ) ∨ (x o< a) |
105 osuc-≡< {n} {a} {x} (case1 lt) = case2 (case1 lt) | 105 osuc-≡< {n} {a} {x} (case1 lt) = case2 (case1 lt) |
161 | 161 |
162 | 162 |
163 open _∧_ | 163 open _∧_ |
164 | 164 |
165 TransFinite : {n m : Level} → { ψ : Ordinal {suc n} → Set m } | 165 TransFinite : {n m : Level} → { ψ : Ordinal {suc n} → Set m } |
166 → ( ∀ (lx : Nat ) → ( (x : Ordinal {suc n} ) → x o< ordinal lx (Φ lx) → ψ x ) → ψ ( record { lv = lx ; ord = Φ lx } ) ) | 166 → ( ∀ (lx : ℕ ) → ( (x : Ordinal {suc n} ) → x o< ordinal lx (Φ lx) → ψ x ) → ψ ( record { lv = lx ; ord = Φ lx } ) ) |
167 → ( ∀ (lx : Nat ) → (x : OrdinalD lx ) → ( (y : Ordinal {suc n} ) → y o< ordinal lx (OSuc lx x) → ψ y ) → ψ ( record { lv = lx ; ord = OSuc lx x } ) ) | 167 → ( ∀ (lx : ℕ ) → (x : OrdinalD lx ) → ( (y : Ordinal {suc n} ) → y o< ordinal lx (OSuc lx x) → ψ y ) → ψ ( record { lv = lx ; ord = OSuc lx x } ) ) |
168 → ∀ (x : Ordinal) → ψ x | 168 → ∀ (x : Ordinal) → ψ x |
169 TransFinite {n} {m} {ψ} caseΦ caseOSuc x = proj1 (TransFinite1 (lv x) (ord x) ) where | 169 TransFinite {n} {m} {ψ} caseΦ caseOSuc x = proj1 (TransFinite1 (lv x) (ord x) ) where |
170 TransFinite1 : (lx : Nat) (ox : OrdinalD lx ) → ψ (ordinal lx ox) ∧ ( ( (x : Ordinal {suc n} ) → x o< ordinal lx ox → ψ x ) ) | 170 TransFinite1 : (lx : ℕ) (ox : OrdinalD lx ) → ψ (ordinal lx ox) ∧ ( ( (x : Ordinal {suc n} ) → x o< ordinal lx ox → ψ x ) ) |
171 TransFinite1 Zero (Φ 0) = ⟪ caseΦ Zero lemma , lemma1 ⟫ where | 171 TransFinite1 Zero (Φ 0) = ⟪ caseΦ Zero lemma , lemma1 ⟫ where |
172 lemma : (x : Ordinal) → x o< ordinal Zero (Φ Zero) → ψ x | 172 lemma : (x : Ordinal) → x o< ordinal Zero (Φ Zero) → ψ x |
173 lemma x (case1 ()) | 173 lemma x (case1 ()) |
174 lemma x (case2 ()) | 174 lemma x (case2 ()) |
175 lemma1 : (x : Ordinal) → x o< ordinal Zero (Φ Zero) → ψ x | 175 lemma1 : (x : Ordinal) → x o< ordinal Zero (Φ Zero) → ψ x |
176 lemma1 x (case1 ()) | 176 lemma1 x (case1 ()) |
177 lemma1 x (case2 ()) | 177 lemma1 x (case2 ()) |
178 TransFinite1 (Suc lx) (Φ (Suc lx)) = ⟪ caseΦ (Suc lx) (λ x → lemma (lv x) (ord x)) , (λ x → lemma (lv x) (ord x)) ⟫ where | 178 TransFinite1 (Suc lx) (Φ (Suc lx)) = ⟪ caseΦ (Suc lx) (λ x → lemma (lv x) (ord x)) , (λ x → lemma (lv x) (ord x)) ⟫ where |
179 lemma0 : (ly : Nat) (oy : OrdinalD ly ) → ordinal ly oy o< ordinal lx (Φ lx) → ψ (ordinal ly oy) | 179 lemma0 : (ly : ℕ) (oy : OrdinalD ly ) → ordinal ly oy o< ordinal lx (Φ lx) → ψ (ordinal ly oy) |
180 lemma0 ly oy lt = proj2 ( TransFinite1 lx (Φ lx) ) (ordinal ly oy) lt | 180 lemma0 ly oy lt = proj2 ( TransFinite1 lx (Φ lx) ) (ordinal ly oy) lt |
181 lemma : (ly : Nat) (oy : OrdinalD ly ) → ordinal ly oy o< ordinal (Suc lx) (Φ (Suc lx)) → ψ (ordinal ly oy) | 181 lemma : (ly : ℕ) (oy : OrdinalD ly ) → ordinal ly oy o< ordinal (Suc lx) (Φ (Suc lx)) → ψ (ordinal ly oy) |
182 lemma lx1 ox1 (case1 lt) with <-∨ lt | 182 lemma lx1 ox1 (case1 lt) with <-∨ lt |
183 lemma lx (Φ lx) (case1 lt) | case1 refl = proj1 ( TransFinite1 lx (Φ lx) ) | 183 lemma lx (Φ lx) (case1 lt) | case1 refl = proj1 ( TransFinite1 lx (Φ lx) ) |
184 lemma lx (Φ lx) (case1 lt) | case2 lt1 = lemma0 lx (Φ lx) (case1 lt1) | 184 lemma lx (Φ lx) (case1 lt) | case2 lt1 = lemma0 lx (Φ lx) (case1 lt1) |
185 lemma lx (OSuc lx ox1) (case1 lt) | case1 refl = caseOSuc lx ox1 lemma2 where | 185 lemma lx (OSuc lx ox1) (case1 lt) | case1 refl = caseOSuc lx ox1 lemma2 where |
186 lemma2 : (y : Ordinal) → (Suc (lv y) ≤ lx) ∨ (ord y d< OSuc lx ox1) → ψ y | 186 lemma2 : (y : Ordinal) → (Suc (lv y) ≤ lx) ∨ (ord y d< OSuc lx ox1) → ψ y |
198 lemma : (y : Ordinal) → y o< ordinal lx (OSuc lx ox) → ψ y | 198 lemma : (y : Ordinal) → y o< ordinal lx (OSuc lx ox) → ψ y |
199 lemma y lt with osuc-≡< lt | 199 lemma y lt with osuc-≡< lt |
200 lemma y lt | case1 refl = proj1 ( TransFinite1 lx ox ) | 200 lemma y lt | case1 refl = proj1 ( TransFinite1 lx ox ) |
201 lemma y lt | case2 lt1 = proj2 ( TransFinite1 lx ox ) y lt1 | 201 lemma y lt | case2 lt1 = proj2 ( TransFinite1 lx ox ) y lt1 |
202 | 202 |
203 open import Data.Nat.Properties as DP | |
204 OrdIrr : {n : Level } {x y : Ordinal {suc n} } {lt lt1 : x o< y} → lt ≡ lt1 | 203 OrdIrr : {n : Level } {x y : Ordinal {suc n} } {lt lt1 : x o< y} → lt ≡ lt1 |
205 OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} {case1 x} {case1 x₁} = cong case1 (DP.<-irrelevant _ _ ) | 204 OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} {case1 x} {case1 x₁} = cong case1 (NP.<-irrelevant _ _ ) |
206 OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} {case1 x} {case2 x₁} = ⊥-elim ( nat-≡< ( d<→lv x₁ ) x ) | 205 OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} {case1 x} {case2 x₁} = ⊥-elim ( nat-≡< ( d<→lv x₁ ) x ) |
207 OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} {case2 x} {case1 x₁} = ⊥-elim ( nat-≡< ( d<→lv x ) x₁ ) | 206 OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} {case2 x} {case1 x₁} = ⊥-elim ( nat-≡< ( d<→lv x ) x₁ ) |
208 OrdIrr {n} {ordinal lv₁ .(Φ lv₁)} {ordinal .lv₁ .(OSuc lv₁ _)} {case2 Φ<} {case2 Φ<} = refl | 207 OrdIrr {n} {ordinal lv₁ .(Φ lv₁)} {ordinal .lv₁ .(OSuc lv₁ _)} {case2 Φ<} {case2 Φ<} = refl |
209 OrdIrr {n} {ordinal lv₁ (OSuc lv₁ a)} {ordinal .lv₁ (OSuc lv₁ b)} {case2 (s< x)} {case2 (s< x₁)} = cong (λ k → case2 (s< k)) (lemma1 _ _ x x₁) where | 208 OrdIrr {n} {ordinal lv₁ (OSuc lv₁ a)} {ordinal .lv₁ (OSuc lv₁ b)} {case2 (s< x)} {case2 (s< x₁)} = cong (λ k → case2 (s< k)) (lemma1 _ _ x x₁) where |
210 lemma1 : {lx : Nat} (a b : OrdinalD {suc n} lx) → (x y : a d< b ) → x ≡ y | 209 lemma1 : {lx : ℕ} (a b : OrdinalD {suc n} lx) → (x y : a d< b ) → x ≡ y |
211 lemma1 {lx} .(Φ lx) .(OSuc lx _) Φ< Φ< = refl | 210 lemma1 {lx} .(Φ lx) .(OSuc lx _) Φ< Φ< = refl |
212 lemma1 {lx} (OSuc lx a) (OSuc lx b) (s< x) (s< y) = cong s< (lemma1 {lx} a b x y ) | 211 lemma1 {lx} (OSuc lx a) (OSuc lx b) (s< x) (s< y) = cong s< (lemma1 {lx} a b x y ) |
212 | |
213 TransFinite3 : {n m : Level} { ψ : Ordinal {suc n} → Set m } | |
214 → ( (x : Ordinal {suc n}) → ( (y : Ordinal {suc n} ) → y o< x → ψ y ) → ψ x ) | |
215 → ∀ (x : Ordinal {suc n} ) → ψ x | |
216 TransFinite3 {n} {m} {ψ} ind x = TransFinite {n} {m} {ψ} caseΦ caseOSuc x where | |
217 caseΦ : (lx : ℕ) → ((x₁ : Ordinal {suc n}) → x₁ o< ordinal lx (Φ lx) → ψ x₁) → | |
218 ψ (record { lv = lx ; ord = Φ lx }) | |
219 caseΦ lx prev = ind (ordinal lx (Φ lx) ) prev | |
220 caseOSuc : (lx : ℕ) (x₁ : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x₁) → ψ y) → | |
221 ψ (record { lv = lx ; ord = OSuc lx x₁ }) | |
222 caseOSuc lx ox prev = ind (ordinal lx (OSuc lx ox)) prev | |
223 | |
224 -- TP : {n m l : Level} → {Q : Ordinal {suc n} → Set m} {P : { x y : Ordinal {suc n} } → Q x → Q y → Set l} | |
225 -- → ( ind : (x : Ordinal {suc n}) → ( (y : Ordinal {suc n} ) → y o< x → Q y ) → Q x ) | |
226 -- → ( (x : Ordinal {suc n} ) → ( prev : (y : Ordinal {suc n} ) → y o< x → Q y ) → {y : Ordinal {suc n}} → (y<x : y o< x) → P (prev y y<x) (ind x prev) ) | |
227 -- → {x z : Ordinal {suc n} } → (z≤x : z o< osuc x ) → P (TransFinite3 {n} {m} { λ x → Q x } {!!} x ) {!!} -- P (TransFinite {?} ind z) (TransFinite {?} ind x ) | |
228 -- TP = ? | |
213 | 229 |
230 | |
214 open import Ordinals | 231 open import Ordinals |
215 | 232 |
216 C-Ordinal : {n : Level} → Ordinals {suc n} | 233 C-Ordinal : {n : Level} → Ordinals {suc n} |
217 C-Ordinal {n} = record { | 234 C-Ordinal {n} = record { |
218 Ordinal = Ordinal {suc n} | 235 Ordinal = Ordinal {suc n} |
248 lemma2 (ordinal Zero (Φ 0)) (case2 ()) (case1 (s≤s z≤n)) not | 265 lemma2 (ordinal Zero (Φ 0)) (case2 ()) (case1 (s≤s z≤n)) not |
249 lemma2 (ordinal Zero (OSuc 0 dx)) (case2 Φ<) (case1 (s≤s z≤n)) not = not _ refl | 266 lemma2 (ordinal Zero (OSuc 0 dx)) (case2 Φ<) (case1 (s≤s z≤n)) not = not _ refl |
250 lemma2 (ordinal Zero (OSuc 0 dx)) (case2 (s< x)) (case1 (s≤s z≤n)) not = not _ refl | 267 lemma2 (ordinal Zero (OSuc 0 dx)) (case2 (s< x)) (case1 (s≤s z≤n)) not = not _ refl |
251 lemma2 (ordinal (Suc lx) (OSuc (Suc lx) ox)) y<x (case1 (s≤s (s≤s lt))) not = not _ refl | 268 lemma2 (ordinal (Suc lx) (OSuc (Suc lx) ox)) y<x (case1 (s≤s (s≤s lt))) not = not _ refl |
252 lemma2 (ordinal (Suc lx) (Φ (Suc lx))) (case1 x) (case1 (s≤s (s≤s lt))) not = lemma3 x lt where | 269 lemma2 (ordinal (Suc lx) (Φ (Suc lx))) (case1 x) (case1 (s≤s (s≤s lt))) not = lemma3 x lt where |
253 lemma3 : {n l : Nat} → (Suc (Suc n) ≤ Suc l) → l ≤ n → ⊥ | 270 lemma3 : {n l : ℕ} → (Suc (Suc n) ≤ Suc l) → l ≤ n → ⊥ |
254 lemma3 (s≤s sn≤l) (s≤s l≤n) = lemma3 sn≤l l≤n | 271 lemma3 (s≤s sn≤l) (s≤s l≤n) = lemma3 sn≤l l≤n |
255 open Oprev | 272 open Oprev |
256 Oprev-p : (x : Ordinal) → Dec ( Oprev (Ordinal {suc n}) osuc x ) | 273 Oprev-p : (x : Ordinal) → Dec ( Oprev (Ordinal {suc n}) osuc x ) |
257 Oprev-p (ordinal lv (Φ lv)) = no (λ not → lemma (oprev not) (oprev=x not) ) where | 274 Oprev-p (ordinal lv (Φ lv)) = no (λ not → lemma (oprev not) (oprev=x not) ) where |
258 lemma : (x : Ordinal) → osuc x ≡ (ordinal lv (Φ lv)) → ⊥ | 275 lemma : (x : Ordinal) → osuc x ≡ (ordinal lv (Φ lv)) → ⊥ |
261 ord1 : Set (suc n) | 278 ord1 : Set (suc n) |
262 ord1 = Ordinal {suc n} | 279 ord1 = Ordinal {suc n} |
263 TransFinite2 : { ψ : ord1 → Set (suc (suc n)) } | 280 TransFinite2 : { ψ : ord1 → Set (suc (suc n)) } |
264 → ( (x : ord1) → ( (y : ord1 ) → y o< x → ψ y ) → ψ x ) | 281 → ( (x : ord1) → ( (y : ord1 ) → y o< x → ψ y ) → ψ x ) |
265 → ∀ (x : ord1) → ψ x | 282 → ∀ (x : ord1) → ψ x |
266 TransFinite2 {ψ} lt x = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc x where | 283 TransFinite2 {ψ} ind x = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc x where |
267 caseΦ : (lx : Nat) → ((x₁ : Ordinal) → x₁ o< ordinal lx (Φ lx) → ψ x₁) → | 284 caseΦ : (lx : ℕ) → ((x₁ : Ordinal) → x₁ o< ordinal lx (Φ lx) → ψ x₁) → |
268 ψ (record { lv = lx ; ord = Φ lx }) | 285 ψ (record { lv = lx ; ord = Φ lx }) |
269 caseΦ lx prev = lt (ordinal lx (Φ lx) ) prev | 286 caseΦ lx prev = ind (ordinal lx (Φ lx) ) prev |
270 caseOSuc : (lx : Nat) (x₁ : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x₁) → ψ y) → | 287 caseOSuc : (lx : ℕ) (x₁ : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x₁) → ψ y) → |
271 ψ (record { lv = lx ; ord = OSuc lx x₁ }) | 288 ψ (record { lv = lx ; ord = OSuc lx x₁ }) |
272 caseOSuc lx ox prev = lt (ordinal lx (OSuc lx ox)) prev | 289 caseOSuc lx ox prev = ind (ordinal lx (OSuc lx ox)) prev |
273 | 290 |
274 | 291 |
275 -- H-Ordinal : {n : Level} → Ordinals {suc n} → Ordinals {suc n} → Ordinals {suc n} | 292 -- H-Ordinal : {n : Level} → Ordinals {suc n} → Ordinals {suc n} → Ordinals {suc n} |
276 -- H-Ordinal {n} O1 O2 = record { | 293 -- H-Ordinal {n} O1 O2 = record { |
277 -- Ordinal = Ordinals.Ordinal O1 ∧ Ordinals.Ordinal O2 | 294 -- Ordinal = Ordinals.Ordinal O1 ∧ Ordinals.Ordinal O2 |