YES Trs: {a b a -> b a} Comment: We consider a non-duplicating trs. BOUND: Automaton: {a_2(q11) -> q12, a_1(q3) -> q4, a_0(q2) -> q2, b_2(q12) -> q13, b_1(q4) -> q5, b_0(q2) -> q2, q13 -> q12 | q4, q5 -> q12 | q4 | q2, q3 -> q11, q2 -> q3} Strict: {} Qed