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