YES Trs: { p(s(X)) -> X, f(0()) -> cons(0(), n__f(s(0()))), f(s(0())) -> f(p(s(0()))), f(X) -> n__f(X), activate(n__f(X)) -> f(X), activate(X) -> X} Comment: We consider a non-duplicating trs. BOUND: Automaton: {cons_2(q10, q12) -> q6, cons_1(q7, q9) -> q6, cons_0(q6, q6) -> q6, 0_2() -> q10, 0_1() -> q7, 0_0() -> q6, s_2(q10) -> q11, s_1(q7) -> q8, s_0(q6) -> q6, p_1(q8) -> q6, p_0(q6) -> q6, n__f_2(q11) -> q12, n__f_2(q6) -> q6, n__f_1(q8) -> q9, n__f_1(q6) -> q6, n__f_0(q6) -> q6, f_1(q6) -> q6, f_0(q6) -> q6, activate_0(q6) -> q6, q7 -> q6} Strict: {} Qed