YES
O(n)
TRS:
 {   f(0()) -> cons(0()),
  f(s(0())) -> f(p(s(0()))),
    p(s(X)) -> X}
 DUP: We consider a non-duplicating system.
  Trs:
   {   f(0()) -> cons(0()),
    f(s(0())) -> f(p(s(0()))),
      p(s(X)) -> X}
  BOUND:
   Automaton:
    {
         s_1(8) -> 9,
         s_0(5) -> 5,
         p_1(9) -> 10,
         p_0(5) -> 5,
        f_1(10) -> 11,
         f_0(5) -> 5,
          0_2() -> 12,
          0_1() -> 6,
          0_0() -> 5,
     cons_2(12) -> 13,
      cons_1(6) -> 7,
      cons_0(5) -> 5,
             13 -> 11,
             11 -> 5,
              8 -> 10,
              7 -> 5,
              6 -> 8
    }
   Strict:
    {}
   Qed