--- a/ordinal.agda	Wed Jun 05 02:58:17 2019 +0900
+++ b/ordinal.agda	Wed Jun 05 03:21:47 2019 +0900
@@ -211,21 +211,6 @@
 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-induction : {n : Level} ( x y : Ordinal {suc n} ) → { ψ : ( m : Ordinal {suc n} ) → m ≡ omax x y  → Set (suc n) }
-   → (  lv x < lv y → ( m : Ordinal {suc n} ) → (eq : m ≡ omax x y ) → ψ m eq )
-   → (  lv y < lv x → ( m : Ordinal {suc n} ) → (eq : m ≡ omax x y ) → ψ m eq )
-   → (  lv y ≡ lv x → ord x ≅ ord y  → ( m : Ordinal {suc n} ) → (eq : m ≡ omax x y ) → ψ m eq )
-   → (  lv y ≡ lv x → ord x d< ord y  → ( m : Ordinal {suc n} ) → (eq : m ≡ omax x y ) → ψ m eq )
-   → (  lv y ≡ lv x → ord y d< ord x  → ( m : Ordinal {suc n} ) → (eq : m ≡ omax x y ) → ψ m eq )
-   → ψ ( omax x y ) refl
-omax-induction {n} x y c1 c2 c3 c4 c5 with <-cmp (lv x) (lv y)
-omax-induction {n} x y c1 c2 c3 c4 c5 | tri< a ¬b ¬c = c1 a (osuc y) refl
-omax-induction {n} x y c1 c2 c3 c4 c5 | tri> ¬a ¬b c = c2 c (osuc x) refl
-omax-induction {n} x y c1 c2 c3 c4 c5 | tri≈ ¬a refl ¬c with triOrdd (ord x) (ord y)
-omax-induction {n} x y c1 c2 c3 c4 c5 | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = c4 refl a (osuc y) refl
-omax-induction {n} x y c1 c2 c3 c4 c5 | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = c3 refl refl (osuc x) refl
-omax-induction {n} x y c1 c2 c3 c4 c5 | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = c5 refl c (osuc x) refl
-
 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
@@ -237,13 +222,42 @@
 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 = omax-induction {n} x y {λ om refl → x o< om }
-     ( λ lx<ly omax refl → ordtrans (case1 lx<ly) <-osuc )
-     ( λ lx>ly omax → {!!} ) -- ordtrans (case1 lx>ly) <-osuc )
-     ( λ refl refl omax refl → {!!} ) -- <-osuc )
-     ( λ refl ox<oy omax → {!!} ) -- ordtrans (case2 ox<oy) <-osuc )
-     ( λ refl ox>oy omax → {!!} ) -- ordtrans (case2 ox>oy) <-osuc )
+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 | 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-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 | 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
+
+omxx : {n : Level} ( x : Ordinal {suc n} ) → omax x x ≡ osuc x
+omxx {n} x with <-cmp (lv x) (lv x)
+omxx {n} x | tri< a ¬b ¬c = refl
+omxx {n} x | tri> ¬a ¬b c = refl
+omxx {n} x | tri≈ ¬a refl ¬c with triOrdd (ord x) (ord x)
+omxx {n} x | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = refl
+omxx {n} x | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = refl
+omxx {n} x | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b 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 = refl
+omxxx {n} x | tri> ¬a ¬b c = refl
+omxxx {n} x | tri≈ ¬a refl ¬c with triOrdd (ord x) (ord x)
+omxxx {n} x | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = refl
+omxxx {n} x | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = refl
+omxxx {n} x | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = refl
+
 
 OrdTrans : {n : Level} → Transitive {suc n} _o≤_
 OrdTrans (case1 refl) (case1 refl) = case1 refl