YES
Trs:
 {p(m, s(n), 0()) -> p(0(), n, m),
   p(m, 0(), 0()) -> m,
    p(m, n, s(r)) -> p(m, r, n)}
 Comment:
  We consider a non-duplicating trs.
  BOUND:
   Automaton:
    {        s_0(q4) -> q4,
             s_0(q3) -> q4,
               0_1() -> q3,
               0_0() -> q3,
     p_1(q3, q3, q3) -> q3,
     p_0(q4, q4, q4) -> q3,
     p_0(q4, q4, q3) -> q3,
     p_0(q4, q3, q4) -> q3,
     p_0(q4, q3, q3) -> q3,
     p_0(q3, q4, q4) -> q3,
     p_0(q3, q4, q3) -> q3,
     p_0(q3, q3, q4) -> q3,
     p_0(q3, q3, q3) -> q3,
                  q4 -> q3}
   Strict:
   {}
   Qed