TRS: { and(tt(), X) -> activate(X), plus(N, 0()) -> N, plus(N, s(M)) -> s(plus(N, M)), activate(X) -> X} POP*: Precedence: plus > s, and > activate empty Normal: pi(plus) = [1,2], pi(and) = [1,2] Safe: pi(s) = [1], pi(activate) = [1] Predicative System: { and(tt(),X;) -> activate(;X), plus(N,0();) -> N, plus(N,s(;M);) -> s(;plus(N,M;)), activate(;X) -> X} Qed