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

   
  

  Qed