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