--- a/ordinal.agda	Tue Jun 04 12:28:43 2019 +0900
+++ b/ordinal.agda	Tue Jun 04 23:58:58 2019 +0900
@@ -153,12 +153,6 @@
 maxαd x y | tri≈ ¬a b ¬c = x
 maxαd x y | tri> ¬a ¬b c = x
 
-maxα : {n : Level} →  Ordinal {n} →  Ordinal  → Ordinal
-maxα x y with <-cmp (lv x) (lv y)
-maxα x y | tri< a ¬b ¬c = x
-maxα x y | tri> ¬a ¬b c = y
-maxα x y | tri≈ ¬a refl ¬c = record { lv = lv x ; ord = maxαd (ord x) (ord y) }
-
 _o≤_ : {n : Level} → Ordinal → Ordinal → Set (suc n)
 a o≤ b  = (a ≡ b)  ∨ ( a o< b )
 
@@ -199,6 +193,38 @@
    lemma1 (case1 x) = ¬a x
    lemma1 (case2 x) = ≡→¬d< x
 
+maxα : {n : Level} →  Ordinal {n} →  Ordinal  → Ordinal
+maxα x y with <-cmp (lv x) (lv y)
+maxα x y | tri< a ¬b ¬c = x
+maxα x y | tri> ¬a ¬b c = y
+maxα x y | tri≈ ¬a refl ¬c = record { lv = lv x ; ord = maxαd (ord x) (ord y) }
+
+omax : {n : Level} ( x y : Ordinal {suc n} ) → Ordinal {suc n}
+omax {n} x y with <-cmp (lv x) (lv y)
+omax {n} x y | tri< a ¬b ¬c = osuc y
+omax {n} x y | tri> ¬a ¬b c = osuc x
+omax {n} x y | tri≈ ¬a refl ¬c with triOrdd (ord x) (ord y)
+omax {n} x y | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = osuc y
+omax {n} x y | tri≈ ¬a refl ¬c | tri≈ ¬a₁ b ¬c₁ = osuc x
+omax {n} x y | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = osuc x
+
+omax< : {n : Level} ( x y : Ordinal {suc n} ) → x o< y → osuc y ≡ omax x y
+omax< {n} x y lt with <-cmp (lv x) (lv y)
+omax< {n} x y lt | tri< a ¬b ¬c = refl
+omax< {n} x y (case1 lt) | tri> ¬a ¬b c = ⊥-elim (¬a lt)
+omax< {n} x y (case2 lt) | tri> ¬a ¬b c = ⊥-elim (¬b (d<→lv lt ))
+omax< {n} x y (case1 lt) | tri≈ ¬a b ¬c = ⊥-elim (¬a lt)
+omax< {n} x y (case2 lt) | tri≈ ¬a refl ¬c with triOrdd (ord x) (ord y)
+omax< {n} x y (case2 lt) | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = refl
+omax< {n} x y (case2 lt) | tri≈ ¬a refl ¬c | tri≈ ¬a₁ b ¬c₁ = ⊥-elim ( trio<≡ b lt )
+omax< {n} x y (case2 lt) | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = ⊥-elim ( o<> (case2 lt) (case2 c) )
+
+omaxx : {n : Level} ( x y : Ordinal {suc n} ) → x o< omax x y
+omaxx {n} x y with trio< x y 
+omaxx {n} x y | tri< a ¬b ¬c = {!!}
+omaxx {n} x y | tri> ¬a ¬b c = {!!}
+omaxx {n} x y | tri≈ ¬a b ¬c = {!!}
+
 OrdTrans : {n : Level} → Transitive {suc n} _o≤_
 OrdTrans (case1 refl) (case1 refl) = case1 refl
 OrdTrans (case1 refl) (case2 lt2) = case2 lt2