--- a/ordinal.agda	Wed Jun 05 07:05:48 2019 +0900
+++ b/ordinal.agda	Wed Jun 05 09:10:33 2019 +0900
@@ -202,57 +202,47 @@
 --
 --  max ( osuc x , osuc 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 with trio< x 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} x y | tri≈ ¬a refl ¬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 with trio< x 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) )
+omax< {n} x y lt | tri≈ ¬a b ¬c = ⊥-elim (¬a lt )
+omax< {n} x y lt | tri> ¬a ¬b c = ⊥-elim (¬a lt )
+
+omax≡ : {n : Level} ( x y : Ordinal {suc n} ) → x ≡ y → osuc y ≡ omax x y
+omax≡ {n} x y eq with trio< x y
+omax≡ {n} x y eq | tri< a ¬b ¬c = ⊥-elim (¬b eq )
+omax≡ {n} x y eq | tri≈ ¬a refl ¬c = refl
+omax≡ {n} x y eq | tri> ¬a ¬b c = ⊥-elim (¬b eq )
 
 omax-x : {n : Level} ( x y : Ordinal {suc n} ) → x o< omax x y
-omax-x {n} x y with <-cmp (lv x) (lv y)
-omax-x {n} x y | tri< a ¬b ¬c = ordtrans (case1 a) <-osuc
+omax-x {n} x y with trio< x y
+omax-x {n} x y | tri< a ¬b ¬c = ordtrans a <-osuc
 omax-x {n} x y | tri> ¬a ¬b c = <-osuc
-omax-x {n} x y | tri≈ ¬a refl ¬c with triOrdd (ord x) (ord y)
-omax-x {n} x y | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = ordtrans (case2 a) <-osuc
-omax-x {n} x y | tri≈ ¬a refl ¬c | tri≈ ¬a₁ b ¬c₁ = <-osuc
-omax-x {n} x y | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = <-osuc
+omax-x {n} x y | tri≈ ¬a refl ¬c = <-osuc
 
 omax-y : {n : Level} ( x y : Ordinal {suc n} ) → y o< omax x y
-omax-y {n} x y with <-cmp (lv x) (lv y)
+omax-y {n} x y with  trio< x y
 omax-y {n} x y | tri< a ¬b ¬c = <-osuc
-omax-y {n} x y | tri> ¬a ¬b c = ordtrans (case1 c) <-osuc
-omax-y {n} x y | tri≈ ¬a refl ¬c with triOrdd (ord x) (ord y)
-omax-y {n} x y | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = <-osuc
-omax-y {n} x y | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = <-osuc
-omax-y {n} x y | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = ordtrans (case2 c) <-osuc
+omax-y {n} x y | tri> ¬a ¬b c = ordtrans c <-osuc
+omax-y {n} x y | tri≈ ¬a refl ¬c = <-osuc
 
--- omxx : {n : Level} ( x : Ordinal {suc n} ) → omax x x ≡ osuc x
--- omxx {n} record { lv = Zero ; ord = (Φ .0) } = refl
--- omxx {n} record { lv = Zero ; ord = (OSuc .0 (Φ .0)) } = refl
--- omxx {n} record { lv = Zero ; ord = (OSuc .0 (OSuc .0 ord₁)) } = ?
--- omxx {n} record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) } = {!!}
--- omxx {n} record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) } = {!!}
+omxx : {n : Level} ( x : Ordinal {suc n} ) → omax x x ≡ osuc x
+omxx {n} x with  trio< x x
+omxx {n} x | tri< a ¬b ¬c = ⊥-elim (¬b refl )
+omxx {n} x | tri> ¬a ¬b c = ⊥-elim (¬b refl )
+omxx {n} x | tri≈ ¬a refl ¬c = refl
 
 omxxx : {n : Level} ( x : Ordinal {suc n} ) → omax x (omax x x ) ≡ osuc (osuc x)
-omxxx {n} x with <-cmp (lv x) (lv x)
-omxxx {n} x | tri< a ¬b ¬c = ? -- ⊥-elim (¬b refl)
-omxxx {n} x | tri> ¬a ¬b c = ? -- ⊥-elim (¬b refl) 
-omxxx {n} x | tri≈ ¬a refl ¬c = ?
+omxxx {n} x = trans ( cong ( λ k → omax x k ) (omxx x )) (sym ( omax< x (osuc x) <-osuc ))
 
+-- omax≡ (omax x x ) (osuc x) (omxx x)
 
 OrdTrans : {n : Level} → Transitive {suc n} _o≤_
 OrdTrans (case1 refl) (case1 refl) = case1 refl