YES
O(n)
TRS:
 {
        \(x, x) -> e(),
  \(x, .(x, y)) -> y,
      \(e(), x) -> x,
  \(/(x, y), x) -> y,
        /(x, x) -> e(),
      /(x, e()) -> x,
  /(x, \(y, x)) -> y,
  /(.(y, x), x) -> y,
      .(x, e()) -> x,
  .(x, \(x, y)) -> y,
      .(e(), x) -> x,
  .(/(y, x), x) -> y
 }
 Natural interpretation:
  Strict:
   {
          \(x, x) -> e(),
    \(x, .(x, y)) -> y,
        \(e(), x) -> x,
    \(/(x, y), x) -> y,
          /(x, x) -> e(),
        /(x, e()) -> x,
    /(x, \(y, x)) -> y,
    /(.(y, x), x) -> y,
        .(x, e()) -> x,
    .(x, \(x, y)) -> y,
        .(e(), x) -> x,
    .(/(y, x), x) -> y
   }
  Weak:
   {}
  Interpretation class: stronglylinear
  [.](X1, X0) = + 1*X0 + 1*X1 + 1
  [/](X1, X0) = + 1*X0 + 1*X1 + 1
  [\](X1, X0) = + 1*X0 + 1*X1 + 1
  [e] = + 0
  
  Qed