# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1594616146 -32400
# Node ID b1ccdbb14c921c96ed827d9004a17c1cd20316f1
# Parent  27d2933c4bd79348048dcc9af9b945fd4879f9de
...

diff -r 27d2933c4bd7 -r b1ccdbb14c92 OD.agda
--- a/OD.agda	Mon Jul 13 13:29:38 2020 +0900
+++ b/OD.agda	Mon Jul 13 13:55:46 2020 +0900
@@ -396,7 +396,7 @@
             lemmab : {x  : HOD} → od→ord (x , x) o< next (od→ord x)
             lemmab {x} = subst (λ k → od→ord (x , x) o< k ) lemmab0 lemmab1  where
                lemmab0 : next (odmax (x , x)) ≡ next (od→ord x)
-               lemmab0 = {!!}
+               lemmab0 = trans (cong (λ k → next k) (omxx _)) (sym nexto≡)
                lemmab1 : od→ord (x , x) o< next ( odmax (x , x))
                lemmab1 = ho< 
             lemmac : {x y : HOD} → od→ord x o< od→ord y → od→ord (x , y) o< od→ord (y , y) 
@@ -408,7 +408,7 @@
             lemma91 : od→ord (ord→od y) o< od→ord (ord→od y , ord→od y)
             lemma91 = c<→o< (case1 refl) 
             lemma9 : od→ord (ord→od y , (ord→od y , ord→od y)) o< next (od→ord (ord→od y , ord→od y))
-            lemma9 = lemmaa {!!}
+            lemma9 = lemmaa (c<→o< (case1 refl))
             lemma71 : od→ord (ord→od y , (ord→od y , ord→od y)) o< next (od→ord (ord→od y))
             lemma71 = next< lemma81 lemma9
             lemma1 : od→ord (u y) o< next (osuc (od→ord (ord→od y , (ord→od y , ord→od y))))
diff -r 27d2933c4bd7 -r b1ccdbb14c92 Ordinals.agda
--- a/Ordinals.agda	Mon Jul 13 13:29:38 2020 +0900
+++ b/Ordinals.agda	Mon Jul 13 13:55:46 2020 +0900
@@ -228,15 +228,21 @@
         next< {x} {y} {z} x<nz y<nx | tri> ¬a ¬b c = ⊥-elim (proj2 (proj2 next-limit) (next z) x<nz (ordtrans c y<nx )
            (λ w nz=ow → o<¬≡ (sym nz=ow) (proj1 (proj2 next-limit) _ (subst (λ k → w o< k ) (sym nz=ow) <-osuc ))))
 
+        osuc< : {x y : Ordinal} → osuc x ≡ y → x o< y
+        osuc< {x} {y} refl = <-osuc 
+
         nexto=n : {x y : Ordinal} → x o< next (osuc y)  → x o< next y 
         nexto=n {x} {y} x<noy = next< (proj1 (proj2 next-limit) _ (proj1 next-limit)) x<noy
 
         nexto≡ : {x : Ordinal} → next x ≡ next (osuc x)  
         nexto≡ {x} with trio< (next x) (next (osuc x) ) 
-        nexto≡ {x} | tri< a ¬b ¬c = {!!}
+        --    next x o< next (osuc x ) ->  osuc x o< next x o< next (osuc x) -> next x ≡ osuc z -> z o o< next x -> osuc z o< next x -> next x o< next x
+        nexto≡ {x} | tri< a ¬b ¬c = ⊥-elim ((proj2 (proj2 next-limit)) _ (proj1 (proj2 next-limit) _ (proj1 next-limit) ) a
+           (λ z eq → o<¬≡ (sym eq) ((proj1 (proj2 next-limit)) _ (osuc< (sym eq)))))
         nexto≡ {x} | tri≈ ¬a b ¬c = b
+        --    next (osuc x) o< next x ->  osuc x o< next (osuc x) o< next x -> next (osuc x) ≡ osuc z -> z o o< next (osuc x) ...
         nexto≡ {x} | tri> ¬a ¬b c = ⊥-elim ((proj2 (proj2 next-limit)) _ (ordtrans <-osuc (proj1 next-limit)) c
-           (λ z eq → o<¬≡ (sym eq) (proj1 (proj2 next-limit) _ (ordtrans <-osuc (subst (λ k → k o< next (osuc x)) eq {!!} )))))
+           (λ z eq → o<¬≡ (sym eq) ((proj1 (proj2 next-limit)) _ (osuc< (sym eq)))))
 
         record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where
           field