YES(?,O(n^1))
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
 }
 DUP: We consider a non-duplicating system.
  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
   }
  BOUND:
   Bound: match(-raise)-bounded by 2
   Automaton:
    {
        activate_0(1) -> 1*
        p_1(3) -> 1*
        p_0(1) -> 1*
        s_2(5) -> 6*
        s_1(2) -> 3*
        s_0(1) -> 1*
        n__f_2(6) -> 7*
        n__f_2(1) -> 1*
        n__f_1(3) -> 4*
        n__f_1(1) -> 1*
        n__f_0(1) -> 1*
         0_2() -> 5*
         0_1() -> 2*
         0_0() -> 1*
     cons_2(5, 7) -> 1*
     cons_1(2, 4) -> 1*
     cons_0(1, 1) -> 1*
        f_1(1) -> 1*
      f_0(1) -> 1*
           2 -> 1*
    }
   Strict:
    {}
   Qed