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