YES
TRS:
 {  activate(X) -> X,
   and(tt(), X) -> activate(X),
   plus(N, 0()) -> N,
  plus(N, s(M)) -> s(plus(N, M))}
 RUF:
  Strict:
   {  activate(X) -> X,
    plus(N, s(M)) -> s(plus(N, M))}
  Weak:
   {}
  RUF:
   Strict:
    {plus(N, s(M)) -> s(plus(N, M))}
   Weak:
    {}
   DP:
    Strict:
     {plus#(N, s(M)) -> plus#(N, M)}
    Weak:
    {plus(N, s(M)) -> s(plus(N, M))}
    EDG:
     {(plus#(N, s(M)) -> plus#(N, M), plus#(N, s(M)) -> plus#(N, M))}
     SCCS:
      Scc:
       {plus#(N, s(M)) -> plus#(N, M)}
      SCC:
       Strict:
        {plus#(N, s(M)) -> plus#(N, M)}
       Weak:
       {plus(N, s(M)) -> s(plus(N, M))}
       SPSC:
        Simple Projection:
         pi(plus#) = 1
        Strict:
         {}
        Qed