YES
O(n^2)
TRS:
 {
  U12(tt(), M, N) -> s(plus(activate(N), activate(M))),
      activate(X) -> X,
  U11(tt(), M, N) -> U12(tt(), activate(M), activate(N)),
    plus(N, s(M)) -> U11(tt(), M, N),
     plus(N, 0()) -> N
 }
 Natural interpretation:
  Strict:
   {
    U12(tt(), M, N) -> s(plus(activate(N), activate(M))),
        activate(X) -> X,
    U11(tt(), M, N) -> U12(tt(), activate(M), activate(N)),
      plus(N, s(M)) -> U11(tt(), M, N),
       plus(N, 0()) -> N
   }
  Weak:
   {}
  Interpretation class: deltarestricted
  [0](delta) = + 0 + 2*delta
  [plus](delta, X1, X0) = + 1*X0 + 1*X1 + 0 + 3*X0*delta + 0*X1*delta + 0*delta
  [s](delta, X0) = + 1*X0 + 3 + 0*X0*delta + 0*delta
  [U11](delta, X2, X1, X0) = + 1*X0 + 1*X1 + 1*X2 + 3 + 0*X0*delta + 3*X1*delta + 0*X2*delta + 3*delta
  [activate](delta, X0) = + 1*X0 + 0 + 0*X0*delta + 1*delta
  [tt](delta) = + 0 + 3*delta
  [U12](delta, X2, X1, X0) = + 1*X0 + 1*X1 + 1*X2 + 3 + 0*X0*delta + 3*X1*delta + 0*X2*delta + 0*delta
  
  plus_tau_1(delta) = delta/(1 + 0 * delta)plus_tau_2(delta) = delta/(1 + 3 * delta)
  s_tau_1(delta) = delta/(1 + 0 * delta)
  U11_tau_1(delta) = delta/(1 + 0 * delta)U11_tau_2(delta) = delta/(1 + 3 * delta)U11_tau_3(delta) = delta/(1 + 0 * delta)
  activate_tau_1(delta) = delta/(1 + 0 * delta)
  
  U12_tau_1(delta) = delta/(1 + 0 * delta)U12_tau_2(delta) = delta/(1 + 3 * delta)U12_tau_3(delta) = delta/(1 + 0 * delta)
  
  Qed