YES Trs: {f(c(b())) -> f(d(a())), f(c(a())) -> f(d(b())), f(c(X)) -> X, f(a()) -> f(c(a())), f(a()) -> f(d(a())), f(d(X)) -> X, e(g(X)) -> e(X)} Comment: We consider a non-duplicating trs. BOUND: Automaton: { b_2() -> q24, b_1() -> q14, b_0() -> q7, c_1(q15) -> q16, c_0(q8) -> q7, c_0(q7) -> q7, a_2() -> q19, a_1() -> q11, a_0() -> q7, d_2(q19) -> q20, d_1(q11) -> q12, d_0(q8) -> q7, d_0(q7) -> q7, f_2(q20) -> q21, f_1(q12) -> q13, f_0(q8) -> q7, f_0(q7) -> q7, g_0(q8) -> q8, g_0(q7) -> q8, e_1(q9) -> q10, e_0(q8) -> q7, e_0(q7) -> q7, q24 -> q19, q21 -> q13, q19 -> q21, q16 -> q12, q15 -> q13, q14 -> q11, q13 -> q7, q11 -> q15 | q13, q10 -> q7, q8 -> q7, q7 -> q9} Strict: {} Qed