YES
O(n^2)
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: deltarestricted
  [.](delta, X1, X0) = + 1*X0 + 1*X1 + 0 + 0*X0*delta + 0*X1*delta + 1*delta
  [/](delta, X1, X0) = + 1*X0 + 1*X1 + 0 + 0*X0*delta + 0*X1*delta + 1*delta
  [\](delta, X1, X0) = + 1*X0 + 1*X1 + 0 + 0*X0*delta + 0*X1*delta + 1*delta
  [e](delta) = + 0 + 0*delta
  ._tau_1(delta) = delta/(1 + 0 * delta)._tau_2(delta) = delta/(1 + 0 * delta)
  /_tau_1(delta) = delta/(1 + 0 * delta)/_tau_2(delta) = delta/(1 + 0 * delta)
  \_tau_1(delta) = delta/(1 + 0 * delta)\_tau_2(delta) = delta/(1 + 0 * delta)
  
  
  Qed