YES Trs: {f(f(X)) -> c(), h(X) -> c(), c() -> d()} Comment: We consider a non-duplicating trs. BOUND: Automaton: {f_0(q3) -> q3, d_2() -> q8, d_1() -> q6, d_0() -> q3, h_0(q3) -> q3, c_1() -> q4, c_0() -> q3, q8 -> q4, q6 -> q3, q4 -> q3} Strict: {} Qed