YES Trs: {f f -> g f} Comment: We consider a non-duplicating trs. BOUND: Automaton: {f_1(q2) -> q3, f_0(q1) -> q1, g_1(q3) -> q4, g_0(q1) -> q1, q4 -> q3 | q1, q1 -> q2} Strict: {} Qed