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)-DP-bounded by 0
      Automaton:
       {   s_0(16) -> 14*
           s_0(15) -> 13*
           s_0(14) -> 14*
           s_0(13) -> 14*
           s_0(12) -> 14*
           s_0(11) -> 14*
           s_0(10) -> 14*
           p_0(16) -> 12*
           p_0(15) -> 12*
           p_0(14) -> 12*
           p_0(13) -> 16*
           p_0(12) -> 12*
           p_0(11) -> 12*
           p_0(10) -> 12*
          f#_0(16) -> 7*
           f_0(16) -> 11*
           f_0(15) -> 11*
           f_0(14) -> 11*
           f_0(13) -> 11*
           f_0(12) -> 11*
           f_0(11) -> 11*
           f_0(10) -> 11*
             0_0() -> 15*
        cons_0(16) -> 10*
        cons_0(15) -> 10*
        cons_0(14) -> 10*
        cons_0(13) -> 10*
        cons_0(12) -> 10*
        cons_0(11) -> 10*
        cons_0(10) -> 10*
                16 -> 12*
                15 -> 16*
                14 -> 12*
                13 -> 12*
                11 -> 12*
                10 -> 12 | 11}
      Strict:
       {}
      Qed