YES Trs: {g(a(), x) -> f(b(), x), f(a(), x) -> g(a(), x), f(a(), x) -> f(b(), x)} Comment: We consider a non-duplicating trs. BOUND: Automaton: {g_1(q6, q3) -> q3, g_0(q3, q3) -> q3, a_1() -> q6, a_0() -> q3, b_2() -> q7, b_1() -> q4, b_0() -> q3, f_2(q7, q3) -> q3, f_1(q4, q3) -> q3, f_0(q3, q3) -> q3} Strict: {} Qed