YES
Trs:
 {   f(0()) -> cons(0()),
  f(s(0())) -> f(p(s(0()))),
    p(s(X)) -> X}
 Comment:
  We consider a non-duplicating trs.
  BOUND:
   Automaton:
    {cons_2(q11) -> q12,
      cons_1(q5) -> q6,
      cons_0(q4) -> q4,
           0_2() -> q11,
           0_1() -> q5,
           0_0() -> q4,
         f_1(q9) -> q10,
         f_0(q4) -> q4,
         s_1(q7) -> q8,
         s_0(q4) -> q4,
         p_1(q8) -> q9,
         p_0(q4) -> q4,
             q12 -> q10,
             q10 -> q4,
              q7 -> q9,
              q6 -> q4,
              q5 -> q7}
   Strict:
   {}
   Qed