YES(?,O(n^1))
TRS:
 {
    p(m, n, s r) -> p(m, r, n),
  p(m, s n, 0()) -> p(0(), n, m),
  p(m, 0(), 0()) -> m
 }
 DUP: We consider a non-duplicating system.
  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] = + 6
   [s](X0) = + 1*X0 + 3
   [p](X2, X1, X0) = + 1*X0 + 1*X1 + 1*X2 + 1
   
   Qed