# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1594691526 -32400
# Node ID 7389120cd6c014e914202a9cbb6ea1565e137c1c
# Parent  adc3c3a3730842f46358731fa154cea956ba499a
...

diff -r adc3c3a37308 -r 7389120cd6c0 ordinal.agda
--- 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 () ))