YES
O(n)
TRS:
 {
    p(m, n, s(r)) -> p(m, r, n),
  p(m, s(n), 0()) -> p(0(), n, m),
   p(m, 0(), 0()) -> m
 }
 Natural interpretation:
  Strict:
   {
      p(m, n, s(r)) -> p(m, r, n),
    p(m, s(n), 0()) -> p(0(), n, m),
     p(m, 0(), 0()) -> m
   }
  Weak:
   {}
  Interpretation class: stronglylinear
  [0] = + 0
  [s](X0) = + 1*X0 + 1
  [p](X2, X1, X0) = + 1*X0 + 1*X1 + 1*X2 + 1
  
  Qed