YES
TRS:
 {f(s(x)) -> s(s(f(p(s(x))))),
   f(0()) -> 0(),
  p(s(x)) -> x}
 DP:
  Strict:
   {f#(s(x)) -> f#(p(s(x))),
    f#(s(x)) -> p#(s(x))}
  Weak:
  {f(s(x)) -> s(s(f(p(s(x))))),
    f(0()) -> 0(),
   p(s(x)) -> x}
  EDG:
   {(f#(s(x)) -> f#(p(s(x))), f#(s(x)) -> f#(p(s(x))))
    (f#(s(x)) -> f#(p(s(x))), f#(s(x)) -> p#(s(x)))}
   SCCS:
    Scc:
     {f#(s(x)) -> f#(p(s(x)))}
    SCC:
     Strict:
      {f#(s(x)) -> f#(p(s(x)))}
     Weak:
     {f(s(x)) -> s(s(f(p(s(x))))),
       f(0()) -> 0(),
      p(s(x)) -> x}
     UR:
      {p(s(x)) -> x}
      BOUND:
       Bound: match(-raise)-bounded by 1
       Automaton:
        { p_1(3) -> 4*
          p_0(1) -> 1*
         f#_1(4) -> 5*
         f#_0(1) -> 1*
          s_1(2) -> 3*
          s_0(1) -> 1*
               5 -> 1*
               2 -> 4*
               1 -> 2*}
       Strict:
        {}
       Qed