YES
Trs:
 {         f(0()) -> s(0()),
        f(s(0())) -> s(s(0())),
        f(s(0())) -> *(s(s(0())), f(0())),
  f(+(x, s(0()))) -> +(s(s(0())), f(x)),
       f(+(x, y)) -> *(f(x), f(y))}
 Comment:
  We consider a non-duplicating trs.
  BOUND:
   Automaton:
    {        0_3() -> q22,
             0_2() -> q16,
             0_1() -> q6,
             0_0() -> q3,
          s_3(q22) -> q21,
          s_2(q16) -> q13,
          s_2(q13) -> q20 | q19 | q10 | q9,
           s_1(q6) -> q10 | q0,
           s_1(q0) -> q10 | q0,
           s_0(q3) -> q2,
           s_0(q2) -> q2,
           s_0(q1) -> q2,
           s_0(q0) -> q2,
      +_2(q9, q19) -> q20 | q19 | q10 | q9,
      +_1(q0, q10) -> q10 | q0,
       +_1(q0, q9) -> q10 | q0,
       +_0(q3, q3) -> q1,
       +_0(q3, q2) -> q1,
       +_0(q3, q1) -> q1,
       +_0(q3, q0) -> q1,
       +_0(q2, q3) -> q1,
       +_0(q2, q2) -> q1,
       +_0(q2, q1) -> q1,
       +_0(q2, q0) -> q1,
       +_0(q1, q3) -> q1,
       +_0(q1, q2) -> q1,
       +_0(q1, q1) -> q1,
       +_0(q1, q0) -> q1,
       +_0(q0, q3) -> q1,
       +_0(q0, q2) -> q1,
       +_0(q0, q1) -> q1,
       +_0(q0, q0) -> q1,
          f_3(q19) -> q28,
           f_3(q9) -> q27,
          f_2(q19) -> q26,
          f_2(q16) -> q21,
          f_2(q10) -> q20,
           f_2(q9) -> q20,
           f_2(q0) -> q19,
          f_1(q10) -> q10,
           f_1(q9) -> q10,
           f_1(q6) -> q13,
           f_1(q3) -> q10,
           f_1(q2) -> q10,
           f_1(q1) -> q10,
           f_1(q0) -> q10 | q9,
           f_0(q3) -> q0,
           f_0(q2) -> q0,
           f_0(q1) -> q0,
           f_0(q0) -> q0,
     *_3(q27, q28) -> q28 | q27 | q26 | q20,
     *_2(q20, q26) -> q10,
     *_2(q19, q20) -> q20 | q19 | q10 | q9,
      *_2(q9, q21) -> q20 | q19 | q10 | q9,
     *_1(q10, q10) -> q10 | q0,
      *_1(q10, q9) -> q10 | q0,
      *_1(q9, q10) -> q10 | q0,
       *_1(q9, q9) -> q10,
      *_1(q0, q13) -> q10 | q0}
   Strict:
   {}
   Qed