YES
TRS:
 {        mark(tt()) -> tt(),
           mark(0()) -> 0(),
          mark(s(X)) -> s(mark(X)),
   mark(and(X1, X2)) -> a__and(mark(X1), X2),
  mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)),
      a__and(X1, X2) -> and(X1, X2),
     a__and(tt(), X) -> mark(X),
     a__plus(N, 0()) -> mark(N),
    a__plus(N, s(M)) -> s(a__plus(mark(N), mark(M))),
     a__plus(X1, X2) -> plus(X1, X2)}
 DP:
  Strict:
   {        mark#(s(X)) -> mark#(X),
     mark#(and(X1, X2)) -> mark#(X1),
     mark#(and(X1, X2)) -> a__and#(mark(X1), X2),
    mark#(plus(X1, X2)) -> mark#(X1),
    mark#(plus(X1, X2)) -> mark#(X2),
    mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)),
       a__and#(tt(), X) -> mark#(X),
       a__plus#(N, 0()) -> mark#(N),
      a__plus#(N, s(M)) -> mark#(N),
      a__plus#(N, s(M)) -> mark#(M),
      a__plus#(N, s(M)) -> a__plus#(mark(N), mark(M))}
  Weak:
  {        mark(tt()) -> tt(),
            mark(0()) -> 0(),
           mark(s(X)) -> s(mark(X)),
    mark(and(X1, X2)) -> a__and(mark(X1), X2),
   mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)),
       a__and(X1, X2) -> and(X1, X2),
      a__and(tt(), X) -> mark(X),
      a__plus(N, 0()) -> mark(N),
     a__plus(N, s(M)) -> s(a__plus(mark(N), mark(M))),
      a__plus(X1, X2) -> plus(X1, X2)}
  EDG:
   {(a__plus#(N, s(M)) -> a__plus#(mark(N), mark(M)), a__plus#(N, s(M)) -> a__plus#(mark(N), mark(M)))
    (a__plus#(N, s(M)) -> a__plus#(mark(N), mark(M)), a__plus#(N, s(M)) -> mark#(M))
    (a__plus#(N, s(M)) -> a__plus#(mark(N), mark(M)), a__plus#(N, s(M)) -> mark#(N))
    (a__plus#(N, s(M)) -> a__plus#(mark(N), mark(M)), a__plus#(N, 0()) -> mark#(N))
    (a__and#(tt(), X) -> mark#(X), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)))
    (a__and#(tt(), X) -> mark#(X), mark#(plus(X1, X2)) -> mark#(X2))
    (a__and#(tt(), X) -> mark#(X), mark#(plus(X1, X2)) -> mark#(X1))
    (a__and#(tt(), X) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
    (a__and#(tt(), X) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1))
    (a__and#(tt(), X) -> mark#(X), mark#(s(X)) -> mark#(X))
    (a__plus#(N, s(M)) -> mark#(N), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)))
    (a__plus#(N, s(M)) -> mark#(N), mark#(plus(X1, X2)) -> mark#(X2))
    (a__plus#(N, s(M)) -> mark#(N), mark#(plus(X1, X2)) -> mark#(X1))
    (a__plus#(N, s(M)) -> mark#(N), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
    (a__plus#(N, s(M)) -> mark#(N), mark#(and(X1, X2)) -> mark#(X1))
    (a__plus#(N, s(M)) -> mark#(N), mark#(s(X)) -> mark#(X))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X2))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X1))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
    (mark#(plus(X1, X2)) -> mark#(X2), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)))
    (mark#(plus(X1, X2)) -> mark#(X2), mark#(plus(X1, X2)) -> mark#(X2))
    (mark#(plus(X1, X2)) -> mark#(X2), mark#(plus(X1, X2)) -> mark#(X1))
    (mark#(plus(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
    (mark#(plus(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> mark#(X1))
    (mark#(plus(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X))
    (mark#(and(X1, X2)) -> a__and#(mark(X1), X2), a__and#(tt(), X) -> mark#(X))
    (mark#(plus(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
    (mark#(plus(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1))
    (mark#(plus(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
    (mark#(plus(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X1))
    (mark#(plus(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X2))
    (mark#(plus(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)))
    (a__plus#(N, s(M)) -> mark#(M), mark#(s(X)) -> mark#(X))
    (a__plus#(N, s(M)) -> mark#(M), mark#(and(X1, X2)) -> mark#(X1))
    (a__plus#(N, s(M)) -> mark#(M), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
    (a__plus#(N, s(M)) -> mark#(M), mark#(plus(X1, X2)) -> mark#(X1))
    (a__plus#(N, s(M)) -> mark#(M), mark#(plus(X1, X2)) -> mark#(X2))
    (a__plus#(N, s(M)) -> mark#(M), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)))
    (a__plus#(N, 0()) -> mark#(N), mark#(s(X)) -> mark#(X))
    (a__plus#(N, 0()) -> mark#(N), mark#(and(X1, X2)) -> mark#(X1))
    (a__plus#(N, 0()) -> mark#(N), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
    (a__plus#(N, 0()) -> mark#(N), mark#(plus(X1, X2)) -> mark#(X1))
    (a__plus#(N, 0()) -> mark#(N), mark#(plus(X1, X2)) -> mark#(X2))
    (a__plus#(N, 0()) -> mark#(N), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)))
    (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
    (mark#(s(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1))
    (mark#(s(X)) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
    (mark#(s(X)) -> mark#(X), mark#(plus(X1, X2)) -> mark#(X1))
    (mark#(s(X)) -> mark#(X), mark#(plus(X1, X2)) -> mark#(X2))
    (mark#(s(X)) -> mark#(X), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)))
    (mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)), a__plus#(N, 0()) -> mark#(N))
    (mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)), a__plus#(N, s(M)) -> mark#(N))
    (mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)), a__plus#(N, s(M)) -> mark#(M))
    (mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)), a__plus#(N, s(M)) -> a__plus#(mark(N), mark(M)))}
   SCCS:
    Scc:
     {        mark#(s(X)) -> mark#(X),
       mark#(and(X1, X2)) -> mark#(X1),
       mark#(and(X1, X2)) -> a__and#(mark(X1), X2),
      mark#(plus(X1, X2)) -> mark#(X1),
      mark#(plus(X1, X2)) -> mark#(X2),
      mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)),
         a__and#(tt(), X) -> mark#(X),
         a__plus#(N, 0()) -> mark#(N),
        a__plus#(N, s(M)) -> mark#(N),
        a__plus#(N, s(M)) -> mark#(M),
        a__plus#(N, s(M)) -> a__plus#(mark(N), mark(M))}
    SCC:
     Strict:
      {        mark#(s(X)) -> mark#(X),
        mark#(and(X1, X2)) -> mark#(X1),
        mark#(and(X1, X2)) -> a__and#(mark(X1), X2),
       mark#(plus(X1, X2)) -> mark#(X1),
       mark#(plus(X1, X2)) -> mark#(X2),
       mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)),
          a__and#(tt(), X) -> mark#(X),
          a__plus#(N, 0()) -> mark#(N),
         a__plus#(N, s(M)) -> mark#(N),
         a__plus#(N, s(M)) -> mark#(M),
         a__plus#(N, s(M)) -> a__plus#(mark(N), mark(M))}
     Weak:
     {        mark(tt()) -> tt(),
               mark(0()) -> 0(),
              mark(s(X)) -> s(mark(X)),
       mark(and(X1, X2)) -> a__and(mark(X1), X2),
      mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)),
          a__and(X1, X2) -> and(X1, X2),
         a__and(tt(), X) -> mark(X),
         a__plus(N, 0()) -> mark(N),
        a__plus(N, s(M)) -> s(a__plus(mark(N), mark(M))),
         a__plus(X1, X2) -> plus(X1, X2)}
     POLY:
      Argument Filtering:
       pi(plus) = [0,1], pi(and) = [0,1], pi(s) = 0, pi(0) = [], pi(a__plus#) = [0,1], pi(a__plus) = [0,1], pi(tt) = [], pi(a__and#) = 1, pi(a__and) = [0,1], pi(mark#) = 0, pi(mark) = 0
      Usable Rules:
       {}
      Interpretation:
       [a__plus#](x0, x1) = x0 + x1,
       [plus](x0, x1) = x0 + x1,
       [and](x0, x1) = x0 + x1,
       [0] = 1
      Strict:
       {        mark#(s(X)) -> mark#(X),
         mark#(and(X1, X2)) -> mark#(X1),
         mark#(and(X1, X2)) -> a__and#(mark(X1), X2),
        mark#(plus(X1, X2)) -> mark#(X1),
        mark#(plus(X1, X2)) -> mark#(X2),
        mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)),
           a__and#(tt(), X) -> mark#(X),
          a__plus#(N, s(M)) -> mark#(N),
          a__plus#(N, s(M)) -> mark#(M),
          a__plus#(N, s(M)) -> a__plus#(mark(N), mark(M))}
      Weak:
       {        mark(tt()) -> tt(),
                 mark(0()) -> 0(),
                mark(s(X)) -> s(mark(X)),
         mark(and(X1, X2)) -> a__and(mark(X1), X2),
        mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)),
            a__and(X1, X2) -> and(X1, X2),
           a__and(tt(), X) -> mark(X),
           a__plus(N, 0()) -> mark(N),
          a__plus(N, s(M)) -> s(a__plus(mark(N), mark(M))),
           a__plus(X1, X2) -> plus(X1, X2)}
      EDG:
       {(a__and#(tt(), X) -> mark#(X), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)))
        (a__and#(tt(), X) -> mark#(X), mark#(plus(X1, X2)) -> mark#(X2))
        (a__and#(tt(), X) -> mark#(X), mark#(plus(X1, X2)) -> mark#(X1))
        (a__and#(tt(), X) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
        (a__and#(tt(), X) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1))
        (a__and#(tt(), X) -> mark#(X), mark#(s(X)) -> mark#(X))
        (a__plus#(N, s(M)) -> mark#(M), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)))
        (a__plus#(N, s(M)) -> mark#(M), mark#(plus(X1, X2)) -> mark#(X2))
        (a__plus#(N, s(M)) -> mark#(M), mark#(plus(X1, X2)) -> mark#(X1))
        (a__plus#(N, s(M)) -> mark#(M), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
        (a__plus#(N, s(M)) -> mark#(M), mark#(and(X1, X2)) -> mark#(X1))
        (a__plus#(N, s(M)) -> mark#(M), mark#(s(X)) -> mark#(X))
        (mark#(plus(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)))
        (mark#(plus(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X2))
        (mark#(plus(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X1))
        (mark#(plus(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
        (mark#(plus(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1))
        (mark#(plus(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
        (mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)), a__plus#(N, s(M)) -> a__plus#(mark(N), mark(M)))
        (mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)), a__plus#(N, s(M)) -> mark#(M))
        (mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)), a__plus#(N, s(M)) -> mark#(N))
        (mark#(and(X1, X2)) -> a__and#(mark(X1), X2), a__and#(tt(), X) -> mark#(X))
        (a__plus#(N, s(M)) -> a__plus#(mark(N), mark(M)), a__plus#(N, s(M)) -> mark#(N))
        (a__plus#(N, s(M)) -> a__plus#(mark(N), mark(M)), a__plus#(N, s(M)) -> mark#(M))
        (a__plus#(N, s(M)) -> a__plus#(mark(N), mark(M)), a__plus#(N, s(M)) -> a__plus#(mark(N), mark(M)))
        (mark#(plus(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X))
        (mark#(plus(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> mark#(X1))
        (mark#(plus(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
        (mark#(plus(X1, X2)) -> mark#(X2), mark#(plus(X1, X2)) -> mark#(X1))
        (mark#(plus(X1, X2)) -> mark#(X2), mark#(plus(X1, X2)) -> mark#(X2))
        (mark#(plus(X1, X2)) -> mark#(X2), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)))
        (mark#(and(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
        (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1))
        (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
        (mark#(and(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X1))
        (mark#(and(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X2))
        (mark#(and(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)))
        (a__plus#(N, s(M)) -> mark#(N), mark#(s(X)) -> mark#(X))
        (a__plus#(N, s(M)) -> mark#(N), mark#(and(X1, X2)) -> mark#(X1))
        (a__plus#(N, s(M)) -> mark#(N), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
        (a__plus#(N, s(M)) -> mark#(N), mark#(plus(X1, X2)) -> mark#(X1))
        (a__plus#(N, s(M)) -> mark#(N), mark#(plus(X1, X2)) -> mark#(X2))
        (a__plus#(N, s(M)) -> mark#(N), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)))
        (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
        (mark#(s(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1))
        (mark#(s(X)) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
        (mark#(s(X)) -> mark#(X), mark#(plus(X1, X2)) -> mark#(X1))
        (mark#(s(X)) -> mark#(X), mark#(plus(X1, X2)) -> mark#(X2))
        (mark#(s(X)) -> mark#(X), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)))}
       SCCS:
        Scc:
         {        mark#(s(X)) -> mark#(X),
           mark#(and(X1, X2)) -> mark#(X1),
           mark#(and(X1, X2)) -> a__and#(mark(X1), X2),
          mark#(plus(X1, X2)) -> mark#(X1),
          mark#(plus(X1, X2)) -> mark#(X2),
          mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)),
             a__and#(tt(), X) -> mark#(X),
            a__plus#(N, s(M)) -> mark#(N),
            a__plus#(N, s(M)) -> mark#(M),
            a__plus#(N, s(M)) -> a__plus#(mark(N), mark(M))}
        SCC:
         Strict:
          {        mark#(s(X)) -> mark#(X),
            mark#(and(X1, X2)) -> mark#(X1),
            mark#(and(X1, X2)) -> a__and#(mark(X1), X2),
           mark#(plus(X1, X2)) -> mark#(X1),
           mark#(plus(X1, X2)) -> mark#(X2),
           mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)),
              a__and#(tt(), X) -> mark#(X),
             a__plus#(N, s(M)) -> mark#(N),
             a__plus#(N, s(M)) -> mark#(M),
             a__plus#(N, s(M)) -> a__plus#(mark(N), mark(M))}
         Weak:
         {        mark(tt()) -> tt(),
                   mark(0()) -> 0(),
                  mark(s(X)) -> s(mark(X)),
           mark(and(X1, X2)) -> a__and(mark(X1), X2),
          mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)),
              a__and(X1, X2) -> and(X1, X2),
             a__and(tt(), X) -> mark(X),
             a__plus(N, 0()) -> mark(N),
            a__plus(N, s(M)) -> s(a__plus(mark(N), mark(M))),
             a__plus(X1, X2) -> plus(X1, X2)}
         POLY:
          Argument Filtering:
           pi(plus) = [0,1], pi(and) = [0,1], pi(s) = [0], pi(0) = [], pi(a__plus#) = [0,1], pi(a__plus) = [0,1], pi(tt) = [], pi(a__and#) = [0,1], pi(a__and) = [0,1], pi(mark#) = 0, pi(mark) = 0
          Usable Rules:
           {}
          Interpretation:
           [a__plus#](x0, x1) = x0 + x1,
           [a__and#](x0, x1) = x0 + x1,
           [plus](x0, x1) = x0 + x1 + 1,
           [and](x0, x1) = x0 + x1,
           [s](x0) = x0 + 1,
           [tt] = 0
          Strict:
           {mark#(and(X1, X2)) -> mark#(X1),
            mark#(and(X1, X2)) -> a__and#(mark(X1), X2),
              a__and#(tt(), X) -> mark#(X)}
          Weak:
           {        mark(tt()) -> tt(),
                     mark(0()) -> 0(),
                    mark(s(X)) -> s(mark(X)),
             mark(and(X1, X2)) -> a__and(mark(X1), X2),
            mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)),
                a__and(X1, X2) -> and(X1, X2),
               a__and(tt(), X) -> mark(X),
               a__plus(N, 0()) -> mark(N),
              a__plus(N, s(M)) -> s(a__plus(mark(N), mark(M))),
               a__plus(X1, X2) -> plus(X1, X2)}
          EDG:
           {(a__and#(tt(), X) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
            (a__and#(tt(), X) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1))
            (mark#(and(X1, X2)) -> a__and#(mark(X1), X2), a__and#(tt(), X) -> mark#(X))
            (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1))
            (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))}
           SCCS:
            Scc:
             {mark#(and(X1, X2)) -> mark#(X1),
              mark#(and(X1, X2)) -> a__and#(mark(X1), X2),
                a__and#(tt(), X) -> mark#(X)}
            SCC:
             Strict:
              {mark#(and(X1, X2)) -> mark#(X1),
               mark#(and(X1, X2)) -> a__and#(mark(X1), X2),
                 a__and#(tt(), X) -> mark#(X)}
             Weak:
             {        mark(tt()) -> tt(),
                       mark(0()) -> 0(),
                      mark(s(X)) -> s(mark(X)),
               mark(and(X1, X2)) -> a__and(mark(X1), X2),
              mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)),
                  a__and(X1, X2) -> and(X1, X2),
                 a__and(tt(), X) -> mark(X),
                 a__plus(N, 0()) -> mark(N),
                a__plus(N, s(M)) -> s(a__plus(mark(N), mark(M))),
                 a__plus(X1, X2) -> plus(X1, X2)}
             SPSC:
              Simple Projection:
               pi(a__and#) = 1, pi(mark#) = 0
              Strict:
               {mark#(and(X1, X2)) -> mark#(X1),
                  a__and#(tt(), X) -> mark#(X)}
              EDG:
               {(mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1))
                (a__and#(tt(), X) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1))}
               SCCS:
                Scc:
                 {mark#(and(X1, X2)) -> mark#(X1)}
                SCC:
                 Strict:
                  {mark#(and(X1, X2)) -> mark#(X1)}
                 Weak:
                 {        mark(tt()) -> tt(),
                           mark(0()) -> 0(),
                          mark(s(X)) -> s(mark(X)),
                   mark(and(X1, X2)) -> a__and(mark(X1), X2),
                  mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)),
                      a__and(X1, X2) -> and(X1, X2),
                     a__and(tt(), X) -> mark(X),
                     a__plus(N, 0()) -> mark(N),
                    a__plus(N, s(M)) -> s(a__plus(mark(N), mark(M))),
                     a__plus(X1, X2) -> plus(X1, X2)}
                 SPSC:
                  Simple Projection:
                   pi(mark#) = 0
                  Strict:
                   {}
                  Qed