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

comparison src/ordinal.agda @ 653:4186c0331abb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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