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

comparison ordinal.agda @ 350:7389120cd6c0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 14 Jul 2020 10:52:06 +0900
parents adc3c3a37308
children
comparison
equal deleted inserted replaced
349:adc3c3a37308 350:7389120cd6c0
242 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
243 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
244 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
245 lemma3 : {n l : Nat} → (Suc (Suc n) ≤ Suc l) → l ≤ n → ⊥ 245 lemma3 : {n l : Nat} → (Suc (Suc n) ≤ Suc l) → l ≤ n → ⊥
246 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 = {!!} 247 --- next y = ordinal (Suc (lv y)) (Φ (Suc (lv y)))
248 lemma2 (ordinal (Suc lx) (OSuc (Suc lx) os)) lt (case2 lt2) not = {!!} 248 -- lt : lv y < Suc lx
249 -- lt2 : Φ (Suc lx) d< OSuc (Suc (lv y)) (Φ (Suc (lv y))) -> Suc lx ≡ Suc (lv y) < Suc lx
250 lemma2 (ordinal (Suc lx) (Φ (Suc lx))) (case1 lt) (case2 lt2) not with <-∨ lt
251 ... | case1 refl = {!!} where -- x = next y case
252 lemma4 : (ordinal (Suc lx) (Φ (Suc lx))) ≡ next y
253 lemma4 = refl
254 ... | case2 lt3 = nat-≡< (sym (d<→lv lt2)) (s≤s lt3)
255 lemma2 (ordinal (Suc lx) (OSuc (Suc lx) os)) (case1 lt) (case2 lt2) not with <-∨ lt
256 ... | case2 lt3 = nat-≡< (sym (d<→lv lt2)) (s≤s lt3)
257 ... | case1 refl with lt2
258 ... | s< ()
259 lemma2 (ordinal (Suc .(lv y)) (OSuc .(Suc (lv y)) os)) (case2 lt) (case2 (s< ())) not
249 260
250 not-limit : (x : Ordinal) → Dec (¬ ((y : Ordinal) → ¬ (x ≡ osuc y))) 261 not-limit : (x : Ordinal) → Dec (¬ ((y : Ordinal) → ¬ (x ≡ osuc y)))
251 not-limit (ordinal lv (Φ lv)) = no (λ not → not (λ y () )) 262 not-limit (ordinal lv (Φ lv)) = no (λ not → not (λ y () ))
252 not-limit (ordinal lv (OSuc lv ox)) = yes (λ not → not (ordinal lv ox) refl ) 263 not-limit (ordinal lv (OSuc lv ox)) = yes (λ not → not (ordinal lv ox) refl )
253 ord1 : Set (suc n) 264 ord1 : Set (suc n)