YES
O(n)
TRS:
 {f(g(f(a()), h(a(), f(a())))) -> f(h(g(f(a()), a()), g(f(a()), f(a()))))}
 DUP: We consider a non-duplicating system.
  Trs:
   {f(g(f(a()), h(a(), f(a())))) -> f(h(g(f(a()), a()), g(f(a()), f(a()))))}
  BOUND:
   Automaton:
    {
          a_1() -> 5,
          a_0() -> 4,
      g_1(8, 9) -> 10,
      g_1(6, 5) -> 7,
      g_0(4, 4) -> 4,
     h_1(7, 10) -> 11,
      h_0(4, 4) -> 4,
        f_1(11) -> 4,
         f_1(5) -> 9 | 8 | 6,
         f_0(4) -> 4
    }
   Strict:
    {}
   Qed