TRS:
 { and(tt(), X) -> activate(X),
   plus(N, 0()) -> N,
  plus(N, s(M)) -> s(plus(N, M)),
    activate(X) -> X}
 MPO:
  Prec:
   plus > s, 
   and > activate
   empty
  Strict:
   {}
   Weak:
    {}
  Qed