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

changeset 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 74fd1073c5b7
files ordinal.agda
diffstat 1 files changed, 13 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/ordinal.agda	Tue Jul 14 09:00:24 2020 +0900
+++ b/ordinal.agda	Tue Jul 14 10:52:06 2020 +0900
@@ -244,8 +244,19 @@
          lemma2 (ordinal (Suc lx) (Φ (Suc lx))) (case1 x) (case1 (s≤s (s≤s lt))) not = lemma3 x lt where
              lemma3 : {n l : Nat} → (Suc (Suc n) ≤ Suc l) → l ≤ n → ⊥
              lemma3   (s≤s sn≤l) (s≤s l≤n) = lemma3 sn≤l l≤n
-         lemma2 (ordinal (Suc lx) (Φ (Suc lx))) (case1 lt) (case2 lt2) not = {!!}
-         lemma2 (ordinal (Suc lx) (OSuc (Suc lx) os)) lt (case2 lt2) not = {!!}
+         --- next y = ordinal (Suc (lv y)) (Φ (Suc (lv y)))
+         --  lt  : lv y < Suc lx
+         --  lt2 : Φ (Suc lx) d< OSuc (Suc (lv y)) (Φ (Suc (lv y))) -> Suc lx ≡ Suc (lv y) < Suc lx
+         lemma2 (ordinal (Suc lx) (Φ (Suc lx))) (case1 lt) (case2 lt2) not with <-∨ lt
+         ... | case1 refl = {!!} where   -- x = next y case
+              lemma4 : (ordinal (Suc lx) (Φ (Suc lx))) ≡ next y
+              lemma4 = refl
+         ... | case2 lt3 = nat-≡< (sym (d<→lv lt2)) (s≤s lt3) 
+         lemma2 (ordinal (Suc lx) (OSuc (Suc lx) os)) (case1 lt) (case2 lt2) not with <-∨ lt
+         ... | case2 lt3 = nat-≡< (sym (d<→lv lt2)) (s≤s lt3) 
+         ... | case1 refl with lt2
+         ... | s< ()
+         lemma2 (ordinal (Suc .(lv y)) (OSuc .(Suc (lv y)) os)) (case2 lt) (case2 (s< ())) not
 
      not-limit : (x : Ordinal) → Dec (¬ ((y : Ordinal) → ¬ (x ≡ osuc y)))
      not-limit (ordinal lv (Φ lv)) = no (λ not → not (λ y () ))