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

diff -r 639fbb6284d8 -r 27d2933c4bd7 OD.agda
--- a/OD.agda	Mon Jul 13 09:26:34 2020 +0900
+++ b/OD.agda	Mon Jul 13 13:29:38 2020 +0900
@@ -393,16 +393,22 @@
             lemma6 = <odmax (ord→od y , (ord→od y , ord→od y)) (subst ( λ k → def (od (ord→od y , (ord→od y , ord→od y))) k ) diso (case1 refl))
             lemma8 : od→ord (ord→od y , ord→od y) o< next (odmax (ord→od y , ord→od y))
             lemma8 = ho<
+            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 = {!!}
+               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) 
+            lemmac = {!!}
+            lemmaa : {x y : HOD} → od→ord x o< od→ord y → od→ord (x , y) o< next (od→ord y)
+            lemmaa x<y = ordtrans (lemmac x<y) lemmab
             lemma81 : od→ord (ord→od y , ord→od y) o< next (od→ord (ord→od y))
             lemma81 = nexto=n (subst (λ k →  od→ord (ord→od y , ord→od y) o< k ) (cong (λ k → next k) (omxx _)) lemma8)
-            lemma7 : od→ord (ord→od y , (ord→od y , ord→od y)) o< next (odmax (ord→od y , (ord→od y , ord→od y)))
             lemma91 : od→ord (ord→od y) o< od→ord (ord→od y , ord→od y)
             lemma91 = c<→o< (case1 refl) 
-            lemma92 : od→ord (ord→od y , (ord→od y , ord→od y)) o< next y
-            lemma92 = {!!}
             lemma9 : od→ord (ord→od y , (ord→od y , ord→od y)) o< next (od→ord (ord→od y , ord→od y))
-            lemma9 = next< {!!} lemma92
-            lemma7 = ho<
+            lemma9 = lemmaa {!!}
             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 639fbb6284d8 -r 27d2933c4bd7 Ordinals.agda
--- a/Ordinals.agda	Mon Jul 13 09:26:34 2020 +0900
+++ b/Ordinals.agda	Mon Jul 13 13:29:38 2020 +0900
@@ -231,6 +231,13 @@
         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 = {!!}
+        nexto≡ {x} | tri≈ ¬a b ¬c = b
+        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 {!!} )))))
+
         record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where
           field
             os→ : (x : Ordinal) → x o< maxordinal → Ordinal