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