TRS: { f(X) -> g(n__h(n__f(X))), h(X) -> n__h(X), f(X) -> n__f(X), activate(n__h(X)) -> h(activate(X)), activate(n__f(X)) -> f(activate(X)), activate(X) -> X} POP*: Precedence: h > n__h, f > n__f, f > n__h, f > g, activate > h, activate > f empty Normal: pi(activate) = [1] Safe: pi(h) = [1], pi(f) = [1], pi(n__f) = [1], pi(n__h) = [1], pi(g) = [1] Predicative System: { f(;X) -> g(;n__h(;n__f(;X))), h(;X) -> n__h(;X), f(;X) -> n__f(;X), activate(n__h(;X);) -> h(;activate(X;)), activate(n__f(;X);) -> f(;activate(X;)), activate(X;) -> X} Qed