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(0())) -> 0(), 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(0())) -> 0(), activate(X) -> X, activate(n__f(X)) -> f(X) } BOUND: Automaton: { activate_0(7) -> 7, p_1(8) -> 7, p_0(7) -> 7, f_1(7) -> 7, f_0(7) -> 7, s_2(7) -> 10, s_1(7) -> 8, s_0(7) -> 7, n__f_2(10) -> 11, n__f_2(7) -> 7, n__f_1(8) -> 9, n__f_1(7) -> 7, n__f_0(7) -> 7, 0_2() -> 7, 0_1() -> 7, 0_0() -> 7, cons_2(7, 11) -> 7, cons_1(7, 9) -> 7, cons_0(7, 7) -> 7 } Strict: {} Qed