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