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

diff -r b1ccdbb14c92 -r 34e71402d579 OD.agda
--- a/OD.agda	Mon Jul 13 13:55:46 2020 +0900
+++ b/OD.agda	Mon Jul 13 14:30:37 2020 +0900
@@ -222,9 +222,20 @@
     lemma {t} (case1 refl) = omax-x  _ _
     lemma {t} (case2 refl) = omax-y  _ _
 
+pair-xx<xy : {x y : HOD} → od→ord (x , x) o< osuc (od→ord (x , y) )
+pair-xx<xy {x} {y} = ⊆→o≤  lemma where
+   lemma : {z : Ordinal} → def (od (x , x)) z → def (od (x , y)) z
+   lemma {z} (case1 refl) = case1 refl
+   lemma {z} (case2 refl) = case1 refl
+
 --  another form of infinite
-pair-ord< :  {x : Ordinal } → Set n
-pair-ord< {x} =  od→ord ( ord→od x , ord→od x ) o< next x
+-- pair-ord< :  {x : Ordinal } → Set n
+pair-ord< : {x : HOD } → ( {y : HOD } → od→ord y o< next (odmax y) ) → od→ord ( x , x ) o< next (od→ord x)
+pair-ord< {x} ho< = subst (λ k → od→ord (x , x) o< k ) lemmab0 lemmab1  where
+       lemmab0 : next (odmax (x , x)) ≡ next (od→ord x)
+       lemmab0 = trans (cong (λ k → next k) (omxx _)) (sym nexto≡)
+       lemmab1 : od→ord (x , x) o< next ( odmax (x , x))
+       lemmab1 = ho<
 
 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 -- postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality n (suc n)
@@ -393,16 +404,9 @@
             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 = 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) 
-            lemmac = {!!}
+            ---           (x,y) < next (omax x y) < next (osuc y) = next y 
             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
+            lemmaa {x} {y} x<y = subst (λ k → od→ord (x , y) o< k ) (sym nexto≡) (subst (λ k → od→ord (x , y) o< next k ) (sym (omax< _ _ x<y)) ho< )
             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)
             lemma91 : od→ord (ord→od y) o< od→ord (ord→od y , ord→od y)