Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison ordinal.agda @ 349:adc3c3a37308
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 14 Jul 2020 09:00:24 +0900 |
parents | feb0fcc430a9 |
children | 7389120cd6c0 |
comparison
equal
deleted
inserted
replaced
348:08d94fec239c | 349:adc3c3a37308 |
---|---|
218 ; ¬x<0 = ¬x<0 | 218 ; ¬x<0 = ¬x<0 |
219 ; <-osuc = <-osuc | 219 ; <-osuc = <-osuc |
220 ; osuc-≡< = osuc-≡< | 220 ; osuc-≡< = osuc-≡< |
221 ; TransFinite = TransFinite1 | 221 ; TransFinite = TransFinite1 |
222 ; TransFinite1 = TransFinite2 | 222 ; TransFinite1 = TransFinite2 |
223 ; not-limit = not-limit | 223 ; not-limit-p = not-limit |
224 ; next-limit = next-limit | 224 } ; |
225 isNext = record { | |
226 x<nx = x<nx | |
227 ; osuc<nx = λ {x} {y} → osuc<nx {x} {y} | |
228 ; ¬nx<nx = ¬nx<nx | |
225 } | 229 } |
226 } where | 230 } where |
227 next : Ordinal {suc n} → Ordinal {suc n} | 231 next : Ordinal {suc n} → Ordinal {suc n} |
228 next (ordinal lv ord) = ordinal (Suc lv) (Φ (Suc lv)) | 232 next (ordinal lv ord) = ordinal (Suc lv) (Φ (Suc lv)) |
229 next-limit : {y : Ordinal} → (y o< next y) ∧ ((x : Ordinal) → x o< next y → osuc x o< next y) ∧ | 233 x<nx : { y : Ordinal } → (y o< next y ) |
230 ( (x : Ordinal) → y o< x → x o< next y → ¬ ((z : Ordinal) → ¬ (x ≡ osuc z) )) | 234 x<nx = case1 a<sa |
231 next-limit {y} = record { proj1 = case1 a<sa ; proj2 = record { proj1 = lemma ; proj2 = lemma2 } } where | 235 osuc<nx : { x y : Ordinal } → x o< next y → osuc x o< next y |
232 lemma : (x : Ordinal) → x o< next y → osuc x o< next y | 236 osuc<nx (case1 lt) = case1 lt |
233 lemma x (case1 lt) = case1 lt | 237 ¬nx<nx : {x y : Ordinal} → y o< x → x o< osuc (next y) → ¬ ((z : Ordinal) → ¬ (x ≡ osuc z)) |
234 lemma2 : (x : Ordinal) → y o< x → x o< next y → ¬ ((z : Ordinal) → ¬ x ≡ osuc z) | 238 ¬nx<nx {x} {y} = lemma2 x where |
239 lemma2 : (x : Ordinal) → y o< x → x o< osuc (next y) → ¬ ((z : Ordinal) → ¬ x ≡ osuc z) | |
235 lemma2 (ordinal Zero (Φ 0)) (case2 ()) (case1 (s≤s z≤n)) not | 240 lemma2 (ordinal Zero (Φ 0)) (case2 ()) (case1 (s≤s z≤n)) not |
236 lemma2 (ordinal Zero (OSuc 0 dx)) (case2 Φ<) (case1 (s≤s z≤n)) not = not _ refl | 241 lemma2 (ordinal Zero (OSuc 0 dx)) (case2 Φ<) (case1 (s≤s z≤n)) not = not _ refl |
237 lemma2 (ordinal Zero (OSuc 0 dx)) (case2 (s< x)) (case1 (s≤s z≤n)) not = not _ refl | 242 lemma2 (ordinal Zero (OSuc 0 dx)) (case2 (s< x)) (case1 (s≤s z≤n)) not = not _ refl |
238 lemma2 (ordinal (Suc lx) (OSuc (Suc lx) ox)) y<x (case1 (s≤s (s≤s lt))) not = not _ refl | 243 lemma2 (ordinal (Suc lx) (OSuc (Suc lx) ox)) y<x (case1 (s≤s (s≤s lt))) not = not _ refl |
239 lemma2 (ordinal (Suc lx) (Φ (Suc lx))) (case1 x) (case1 (s≤s (s≤s lt))) not = lemma3 x lt where | 244 lemma2 (ordinal (Suc lx) (Φ (Suc lx))) (case1 x) (case1 (s≤s (s≤s lt))) not = lemma3 x lt where |
240 lemma3 : {n l : Nat} → (Suc (Suc n) ≤ Suc l) → l ≤ n → ⊥ | 245 lemma3 : {n l : Nat} → (Suc (Suc n) ≤ Suc l) → l ≤ n → ⊥ |
241 lemma3 (s≤s sn≤l) (s≤s l≤n) = lemma3 sn≤l l≤n | 246 lemma3 (s≤s sn≤l) (s≤s l≤n) = lemma3 sn≤l l≤n |
247 lemma2 (ordinal (Suc lx) (Φ (Suc lx))) (case1 lt) (case2 lt2) not = {!!} | |
248 lemma2 (ordinal (Suc lx) (OSuc (Suc lx) os)) lt (case2 lt2) not = {!!} | |
249 | |
242 not-limit : (x : Ordinal) → Dec (¬ ((y : Ordinal) → ¬ (x ≡ osuc y))) | 250 not-limit : (x : Ordinal) → Dec (¬ ((y : Ordinal) → ¬ (x ≡ osuc y))) |
243 not-limit (ordinal lv (Φ lv)) = no (λ not → not (λ y () )) | 251 not-limit (ordinal lv (Φ lv)) = no (λ not → not (λ y () )) |
244 not-limit (ordinal lv (OSuc lv ox)) = yes (λ not → not (ordinal lv ox) refl ) | 252 not-limit (ordinal lv (OSuc lv ox)) = yes (λ not → not (ordinal lv ox) refl ) |
245 ord1 : Set (suc n) | 253 ord1 : Set (suc n) |
246 ord1 = Ordinal {suc n} | 254 ord1 = Ordinal {suc n} |