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