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