YES
O(n)
TRS:
 {f(x, f(y, a())) -> f(f(f(f(a(), a()), y), h(a())), x)}
 DUP: We consider a non-duplicating system.
  Trs:
   {f(x, f(y, a())) -> f(f(f(f(a(), a()), y), h(a())), x)}
  BOUND:
   Automaton:
    {
         h_2(14) -> 17,
          h_1(4) -> 7,
          h_0(3) -> 3,
           a_2() -> 14,
           a_1() -> 4,
           a_0() -> 3,
      f_2(18, 8) -> 6,
     f_2(16, 17) -> 18,
      f_2(15, 4) -> 16,
     f_2(14, 14) -> 15,
       f_1(8, 8) -> 3,
       f_1(8, 5) -> 6,
       f_1(8, 3) -> 3,
       f_1(6, 7) -> 8,
       f_1(5, 8) -> 6,
       f_1(5, 3) -> 6,
       f_1(4, 4) -> 5,
       f_0(3, 3) -> 3
    }
   Strict:
    {}
   Qed