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