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}
 POP*:
  Precedence:
  and > activate, 
  plus > s, 
  x > plus
  empty
  
Normal:
   pi(x) = [1,2], pi(plus) = [2], pi(and) = [1,2]
  
Safe:
   pi(s) = [1], pi(plus) = [1], pi(activate) = [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