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