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