YES Trs: {f(g(x), y) -> f(x, y), f(x, x) -> a()} Comment: We consider a non-duplicating trs. BOUND: Automaton: { a_2() -> q2, a_1() -> q2, a_0() -> q2, g_0(q3) -> q3, g_0(q2) -> q3, f_1(q3, q3) -> q2, f_1(q3, q2) -> q2, f_1(q2, q3) -> q2, f_1(q2, q2) -> q2, f_0(q3, q3) -> q2, f_0(q3, q2) -> q2, f_0(q2, q3) -> q2, f_0(q2, q2) -> q2} Strict: {} Qed