YES
TRS:
 {             f(X) -> n__f(X),
             f(0()) -> cons(0(), n__f(s(0()))),
          f(s(0())) -> f(p(s(0()))),
          p(s(0())) -> 0(),
        activate(X) -> X,
  activate(n__f(X)) -> f(X)}
 RUF:
  Strict:
   {     f(X) -> n__f(X),
       f(0()) -> cons(0(), n__f(s(0()))),
    f(s(0())) -> f(p(s(0()))),
    p(s(0())) -> 0()}
  Weak:
   {}
  DP:
   Strict:
    {f#(s(0())) -> f#(p(s(0()))),
     f#(s(0())) -> p#(s(0()))}
   Weak:
   {     f(X) -> n__f(X),
       f(0()) -> cons(0(), n__f(s(0()))),
    f(s(0())) -> f(p(s(0()))),
    p(s(0())) -> 0()}
   EDG:
    {}
    SCCS:
     
     Qed