YES
O(n)
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:
   Automaton:
    {
     +_2(11, 20) -> 28 | 21 | 20 | 11,
      +_1(2, 11) -> 11 | 2,
      +_1(2, 10) -> 11 | 2,
       +_0(4, 4) -> 4,
       +_0(4, 3) -> 4,
       +_0(4, 2) -> 4,
       +_0(4, 1) -> 4,
       +_0(4, 0) -> 4,
       +_0(3, 4) -> 4,
       +_0(3, 3) -> 4,
       +_0(3, 2) -> 4,
       +_0(3, 1) -> 4,
       +_0(3, 0) -> 4,
       +_0(2, 4) -> 4,
       +_0(2, 3) -> 4,
       +_0(2, 2) -> 4,
       +_0(2, 1) -> 4,
       +_0(2, 0) -> 4,
       +_0(1, 4) -> 4,
       +_0(1, 3) -> 4,
       +_0(1, 2) -> 4,
       +_0(1, 1) -> 4,
       +_0(1, 0) -> 4,
       +_0(0, 4) -> 4,
       +_0(0, 3) -> 4,
       +_0(0, 2) -> 4,
       +_0(0, 1) -> 4,
       +_0(0, 0) -> 4,
     *_3(28, 29) -> 29 | 28 | 27 | 21,
     *_2(21, 27) -> 11,
     *_2(20, 21) -> 28 | 21 | 20 | 11,
     *_2(11, 22) -> 28 | 21 | 20 | 11,
     *_1(11, 11) -> 11 | 2,
     *_1(11, 10) -> 11 | 2,
     *_1(10, 11) -> 11 | 2,
     *_1(10, 10) -> 11,
      *_1(2, 16) -> 11 | 10 | 2,
       *_0(4, 4) -> 3,
       *_0(4, 3) -> 3,
       *_0(4, 2) -> 3,
       *_0(4, 1) -> 3,
       *_0(4, 0) -> 3,
       *_0(3, 4) -> 3,
       *_0(3, 3) -> 3,
       *_0(3, 2) -> 3,
       *_0(3, 1) -> 3,
       *_0(3, 0) -> 3,
       *_0(2, 4) -> 3,
       *_0(2, 3) -> 3,
       *_0(2, 2) -> 3,
       *_0(2, 1) -> 3,
       *_0(2, 0) -> 3,
       *_0(1, 4) -> 3,
       *_0(1, 3) -> 3,
       *_0(1, 2) -> 3,
       *_0(1, 1) -> 3,
       *_0(1, 0) -> 3,
       *_0(0, 4) -> 3,
       *_0(0, 3) -> 3,
       *_0(0, 2) -> 3,
       *_0(0, 1) -> 3,
       *_0(0, 0) -> 3,
         f_3(20) -> 29,
         f_3(11) -> 28,
         f_2(20) -> 27,
         f_2(17) -> 22,
         f_2(11) -> 21,
         f_2(10) -> 21,
          f_2(2) -> 20,
         f_1(11) -> 11,
         f_1(10) -> 11,
          f_1(7) -> 16,
          f_1(4) -> 11,
          f_1(3) -> 11,
          f_1(2) -> 11,
          f_1(1) -> 11,
          f_1(0) -> 11 | 10,
          f_0(4) -> 2,
          f_0(3) -> 2,
          f_0(2) -> 2,
          f_0(1) -> 2,
          f_0(0) -> 2,
           0_3() -> 23,
           0_2() -> 17,
           0_1() -> 7,
           0_0() -> 1,
         s_3(23) -> 22,
         s_2(17) -> 16,
         s_2(16) -> 28 | 21 | 20 | 11,
          s_1(7) -> 11 | 2,
          s_1(2) -> 11 | 10 | 2,
          s_0(4) -> 0,
          s_0(3) -> 0,
          s_0(2) -> 0,
          s_0(1) -> 0,
          s_0(0) -> 0
    }
   Strict:
    {}
   Qed