YES Trs: {f(f(a())) -> c()} Comment: We consider a non-duplicating trs. BOUND: Automaton: { a_0() -> q3, f_0(q3) -> q2, f_0(q2) -> q2, c_1() -> q4, c_0() -> q2, q4 -> q2} Strict: {} Qed