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