YES
TRS:
 {             f(X) -> n__f(X),
             f(0()) -> cons(0(), n__f(s(0()))),
          f(s(0())) -> f(p(s(0()))),
            p(s(X)) -> X,
        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(X)) -> X}
  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(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(X) -> n__f(X),
          f(0()) -> cons(0(), n__f(s(0()))),
       f(s(0())) -> f(p(s(0()))),
         p(s(X)) -> X}
      BOUND:
       Bound: match(-raise)-bounded by 2
       Automaton:
        {      p_1(3) -> 4*
               p_0(1) -> 1*
              f#_1(4) -> 1*
              f#_0(1) -> 1*
               f_1(4) -> 1*
               f_0(1) -> 1*
               s_2(6) -> 7*
               s_1(2) -> 3*
               s_0(1) -> 1*
            n__f_2(7) -> 8*
            n__f_2(4) -> 1*
            n__f_1(3) -> 5*
            n__f_1(1) -> 1*
            n__f_0(1) -> 1*
                0_2() -> 6*
                0_1() -> 2*
                0_0() -> 1*
         cons_2(6, 8) -> 1*
         cons_1(2, 5) -> 1*
         cons_0(1, 1) -> 1*
                    2 -> 4*}
       Strict:
        {}
       Qed