YES
Trs:
 {f(y, f(x, y)) -> f(f(a(), y), f(a(), x))}
 Comment:
  We consider a non-duplicating trs.
  BOUND:
   Automaton:
    {      a_1() -> q5,
     f_1(q6, q6) -> q0,
     f_1(q5, q0) -> q6,
     f_0(q0, q0) -> q0}
   Strict:
   {}
   Qed