YES
Trs:
 {f(g(f(a()), h(a(), f(a())))) -> f(h(g(f(a()), a()), g(f(a()), f(a()))))}
 Comment:
  We consider a non-duplicating trs.
  BOUND:
   Automaton:
    {       a_1() -> q5,
            a_0() -> q4,
      g_1(q8, q9) -> q10,
      g_1(q6, q5) -> q7,
      g_0(q4, q4) -> q4,
     h_1(q7, q10) -> q11,
      h_0(q4, q4) -> q4,
         f_1(q11) -> q4,
          f_1(q5) -> q9 | q8 | q6,
          f_0(q4) -> q4}
   Strict:
   {}
   Qed