YES O(n) TRS: { f(X) -> n__f(X), f(0()) -> cons(0(), n__f(s(0()))), f(s(0())) -> f(p(s(0()))), p(s(X)) -> X, activate(X) -> X, activate(n__f(X)) -> f(X) } DUP: We consider a non-duplicating system. Trs: { f(X) -> n__f(X), f(0()) -> cons(0(), n__f(s(0()))), f(s(0())) -> f(p(s(0()))), p(s(X)) -> X, activate(X) -> X, activate(n__f(X)) -> f(X) } BOUND: Automaton: { activate_0(7) -> 7, p_1(9) -> 7, p_0(7) -> 7, f_1(7) -> 7, f_0(7) -> 7, s_2(11) -> 12, s_1(8) -> 9, s_0(7) -> 7, n__f_2(12) -> 13, n__f_2(7) -> 7, n__f_1(9) -> 10, n__f_1(7) -> 7, n__f_0(7) -> 7, 0_2() -> 11, 0_1() -> 8, 0_0() -> 7, cons_2(11, 13) -> 7, cons_1(8, 10) -> 7, cons_0(7, 7) -> 7, 8 -> 7 } Strict: {} Qed