YES(?,O(n^1))
TRS:
 {  f 0() -> cons 0(),
  f s 0() -> f p s 0(),
  p s 0() -> 0()}
 DUP: We consider a non-duplicating system.
  Trs:
   {  f 0() -> cons 0(),
    f s 0() -> f p s 0(),
    p s 0() -> 0()}
  BOUND:
   Bound: match(-raise)-bounded by 2
   Automaton:
    {
       s_1(5) -> 6*
       s_0(1) -> 1*
       p_1(6) -> 7*
       p_0(1) -> 1*
        0_2() -> 9*
        0_1() -> 2*
        0_0() -> 1*
      cons_2(10) -> 11*
       cons_1(3) -> 4*
       cons_0(1) -> 1*
       f_1(7) -> 8*
     f_0(1) -> 1*
         11 -> 8*
          9 -> 10 | 7
          8 -> 1*
          4 -> 1*
          2 -> 5 | 3 | 1
    }
   Strict:
    {}
   Qed