YES
TRS:
 {   f(0()) -> cons(0()),
  f(s(0())) -> f(p(s(0()))),
    p(s(X)) -> X}
 DP:
  Strict:
   {f#(s(0())) -> f#(p(s(0()))),
    f#(s(0())) -> p#(s(0()))}
  Weak:
  {   f(0()) -> cons(0()),
   f(s(0())) -> f(p(s(0()))),
     p(s(X)) -> X}
  EDG:
   {(f#(s(0())) -> f#(p(s(0()))), f#(s(0())) -> p#(s(0())))
    (f#(s(0())) -> f#(p(s(0()))), f#(s(0())) -> f#(p(s(0()))))}
   SCCS:
    Scc:
     {f#(s(0())) -> f#(p(s(0())))}
    SCC:
     Strict:
      {f#(s(0())) -> f#(p(s(0())))}
     Weak:
     {   f(0()) -> cons(0()),
      f(s(0())) -> f(p(s(0()))),
        p(s(X)) -> X}
     BOUND:
      Bound: match(-raise)-bounded by 2
      Automaton:
       {    s_1(4) -> 5*
            s_0(1) -> 1*
            p_1(5) -> 6*
            p_0(1) -> 1*
           f#_1(8) -> 9*
           f#_0(1) -> 1*
            f_1(6) -> 7*
            f_0(1) -> 1*
             0_2() -> 10*
             0_1() -> 2*
             0_0() -> 1*
        cons_2(10) -> 11*
         cons_1(2) -> 3*
         cons_0(1) -> 1*
                11 -> 7*
                 9 -> 1*
                 7 -> 1*
                 6 -> 8*
                 4 -> 6*
                 3 -> 1*
                 2 -> 4*}
      Strict:
       {}
      Qed