YES(?,O(n^1))
TRS:
 {
        f s 0() -> s s 0(),
        f s 0() -> *(s s 0(), f 0()),
          f 0() -> s 0(),
      f +(x, y) -> *(f x, f y),
  f +(x, s 0()) -> +(s s 0(), f x)
 }
 DUP: We consider a non-duplicating system.
  Trs:
   {
          f s 0() -> s s 0(),
          f s 0() -> *(s s 0(), f 0()),
            f 0() -> s 0(),
        f +(x, y) -> *(f x, f y),
    f +(x, s 0()) -> +(s s 0(), f x)
   }
  BOUND:
   Bound: match(-raise)-bounded by 3
   Automaton:
    {
       +_2(3, 8) -> 13 | 12 | 11 | 8 | 4
       +_2(3, 7) -> 13 | 12 | 11 | 8 | 7 | 4 | 3
       +_1(1, 4) -> 13 | 12 | 11 | 8 | 4
       +_1(1, 3) -> 13 | 12 | 11 | 8 | 7 | 4 | 3 | 1
       +_0(1, 1) -> 1*
     *_3(12, 13) -> 13 | 12 | 11 | 8
      *_2(8, 11) -> 4*
       *_2(7, 8) -> 13 | 12 | 11 | 8 | 7 | 4 | 3
       *_2(3, 9) -> 13 | 12 | 11 | 8 | 7 | 4 | 3
       *_1(3, 4) -> 1*
       *_1(3, 3) -> 7 | 4 | 3
       *_1(1, 5) -> 13 | 12 | 11 | 8 | 7 | 4 | 3 | 1
       *_0(1, 1) -> 1*
           0_3() -> 10*
           0_2() -> 6*
           0_1() -> 2*
           0_0() -> 1*
         s_3(10) -> 9*
          s_2(6) -> 5*
          s_2(5) -> 13 | 12 | 11 | 8 | 7 | 4 | 3
          s_1(2) -> 7 | 4 | 3 | 1
          s_1(1) -> 13 | 12 | 11 | 8 | 7 | 4 | 3 | 1
          s_0(1) -> 1*
          f_3(7) -> 13*
          f_3(3) -> 12*
          f_2(7) -> 11*
          f_2(6) -> 9*
          f_2(3) -> 8*
          f_2(1) -> 7*
          f_1(3) -> 4*
          f_1(2) -> 5*
          f_1(1) -> 4 | 3
        f_0(1) -> 1*
    }
   Strict:
    {}
   Qed