YES
TRS:
 {                    activate(X) -> X,
  activate(n__filter(X1, X2, X3)) -> filter(X1, X2, X3),
            activate(n__sieve(X)) -> sieve(X),
             activate(n__nats(X)) -> nats(X),
               filter(X1, X2, X3) -> n__filter(X1, X2, X3),
       filter(cons(X, Y), 0(), M) -> cons(0(), n__filter(activate(Y), M, M)),
      filter(cons(X, Y), s(N), M) -> cons(X, n__filter(activate(Y), N, M)),
                         sieve(X) -> n__sieve(X),
              sieve(cons(0(), Y)) -> cons(0(), n__sieve(activate(Y))),
             sieve(cons(s(N), Y)) -> cons(s(N), n__sieve(filter(activate(Y), N, N))),
                          nats(X) -> n__nats(X),
                          nats(N) -> cons(N, n__nats(s(N))),
                        zprimes() -> sieve(nats(s(s(0()))))}
 DP:
  Strict:
   {activate#(n__filter(X1, X2, X3)) -> filter#(X1, X2, X3),
              activate#(n__sieve(X)) -> sieve#(X),
               activate#(n__nats(X)) -> nats#(X),
         filter#(cons(X, Y), 0(), M) -> activate#(Y),
        filter#(cons(X, Y), s(N), M) -> activate#(Y),
                sieve#(cons(0(), Y)) -> activate#(Y),
               sieve#(cons(s(N), Y)) -> activate#(Y),
               sieve#(cons(s(N), Y)) -> filter#(activate(Y), N, N),
                          zprimes#() -> sieve#(nats(s(s(0())))),
                          zprimes#() -> nats#(s(s(0())))}
  Weak:
  {                    activate(X) -> X,
   activate(n__filter(X1, X2, X3)) -> filter(X1, X2, X3),
             activate(n__sieve(X)) -> sieve(X),
              activate(n__nats(X)) -> nats(X),
                filter(X1, X2, X3) -> n__filter(X1, X2, X3),
        filter(cons(X, Y), 0(), M) -> cons(0(), n__filter(activate(Y), M, M)),
       filter(cons(X, Y), s(N), M) -> cons(X, n__filter(activate(Y), N, M)),
                          sieve(X) -> n__sieve(X),
               sieve(cons(0(), Y)) -> cons(0(), n__sieve(activate(Y))),
              sieve(cons(s(N), Y)) -> cons(s(N), n__sieve(filter(activate(Y), N, N))),
                           nats(X) -> n__nats(X),
                           nats(N) -> cons(N, n__nats(s(N))),
                         zprimes() -> sieve(nats(s(s(0()))))}
  EDG:
   {(filter#(cons(X, Y), s(N), M) -> activate#(Y), activate#(n__nats(X)) -> nats#(X))
    (filter#(cons(X, Y), s(N), M) -> activate#(Y), activate#(n__sieve(X)) -> sieve#(X))
    (filter#(cons(X, Y), s(N), M) -> activate#(Y), activate#(n__filter(X1, X2, X3)) -> filter#(X1, X2, X3))
    (sieve#(cons(s(N), Y)) -> activate#(Y), activate#(n__nats(X)) -> nats#(X))
    (sieve#(cons(s(N), Y)) -> activate#(Y), activate#(n__sieve(X)) -> sieve#(X))
    (sieve#(cons(s(N), Y)) -> activate#(Y), activate#(n__filter(X1, X2, X3)) -> filter#(X1, X2, X3))
    (zprimes#() -> sieve#(nats(s(s(0())))), sieve#(cons(s(N), Y)) -> filter#(activate(Y), N, N))
    (zprimes#() -> sieve#(nats(s(s(0())))), sieve#(cons(s(N), Y)) -> activate#(Y))
    (zprimes#() -> sieve#(nats(s(s(0())))), sieve#(cons(0(), Y)) -> activate#(Y))
    (activate#(n__filter(X1, X2, X3)) -> filter#(X1, X2, X3), filter#(cons(X, Y), s(N), M) -> activate#(Y))
    (activate#(n__filter(X1, X2, X3)) -> filter#(X1, X2, X3), filter#(cons(X, Y), 0(), M) -> activate#(Y))
    (sieve#(cons(s(N), Y)) -> filter#(activate(Y), N, N), filter#(cons(X, Y), 0(), M) -> activate#(Y))
    (sieve#(cons(s(N), Y)) -> filter#(activate(Y), N, N), filter#(cons(X, Y), s(N), M) -> activate#(Y))
    (activate#(n__sieve(X)) -> sieve#(X), sieve#(cons(0(), Y)) -> activate#(Y))
    (activate#(n__sieve(X)) -> sieve#(X), sieve#(cons(s(N), Y)) -> activate#(Y))
    (activate#(n__sieve(X)) -> sieve#(X), sieve#(cons(s(N), Y)) -> filter#(activate(Y), N, N))
    (sieve#(cons(0(), Y)) -> activate#(Y), activate#(n__filter(X1, X2, X3)) -> filter#(X1, X2, X3))
    (sieve#(cons(0(), Y)) -> activate#(Y), activate#(n__sieve(X)) -> sieve#(X))
    (sieve#(cons(0(), Y)) -> activate#(Y), activate#(n__nats(X)) -> nats#(X))
    (filter#(cons(X, Y), 0(), M) -> activate#(Y), activate#(n__filter(X1, X2, X3)) -> filter#(X1, X2, X3))
    (filter#(cons(X, Y), 0(), M) -> activate#(Y), activate#(n__sieve(X)) -> sieve#(X))
    (filter#(cons(X, Y), 0(), M) -> activate#(Y), activate#(n__nats(X)) -> nats#(X))}
   SCCS:
    Scc:
     {activate#(n__filter(X1, X2, X3)) -> filter#(X1, X2, X3),
                activate#(n__sieve(X)) -> sieve#(X),
           filter#(cons(X, Y), 0(), M) -> activate#(Y),
          filter#(cons(X, Y), s(N), M) -> activate#(Y),
                  sieve#(cons(0(), Y)) -> activate#(Y),
                 sieve#(cons(s(N), Y)) -> activate#(Y),
                 sieve#(cons(s(N), Y)) -> filter#(activate(Y), N, N)}
    SCC:
     Strict:
      {activate#(n__filter(X1, X2, X3)) -> filter#(X1, X2, X3),
                 activate#(n__sieve(X)) -> sieve#(X),
            filter#(cons(X, Y), 0(), M) -> activate#(Y),
           filter#(cons(X, Y), s(N), M) -> activate#(Y),
                   sieve#(cons(0(), Y)) -> activate#(Y),
                  sieve#(cons(s(N), Y)) -> activate#(Y),
                  sieve#(cons(s(N), Y)) -> filter#(activate(Y), N, N)}
     Weak:
     {                    activate(X) -> X,
      activate(n__filter(X1, X2, X3)) -> filter(X1, X2, X3),
                activate(n__sieve(X)) -> sieve(X),
                 activate(n__nats(X)) -> nats(X),
                   filter(X1, X2, X3) -> n__filter(X1, X2, X3),
           filter(cons(X, Y), 0(), M) -> cons(0(), n__filter(activate(Y), M, M)),
          filter(cons(X, Y), s(N), M) -> cons(X, n__filter(activate(Y), N, M)),
                             sieve(X) -> n__sieve(X),
                  sieve(cons(0(), Y)) -> cons(0(), n__sieve(activate(Y))),
                 sieve(cons(s(N), Y)) -> cons(s(N), n__sieve(filter(activate(Y), N, N))),
                              nats(X) -> n__nats(X),
                              nats(N) -> cons(N, n__nats(s(N))),
                            zprimes() -> sieve(nats(s(s(0()))))}
     POLY:
      Argument Filtering:
       pi(zprimes) = [], pi(nats) = [], pi(n__nats) = [], pi(sieve#) = 0, pi(sieve) = [0], pi(n__sieve) = [0], pi(s) = [], pi(filter#) = 0, pi(filter) = 0, pi(activate#) = 0, pi(activate) = 0, pi(n__filter) = 0, pi(0) = [], pi(cons) = 1
      Usable Rules:
       {}
      Interpretation:
       [n__sieve](x0) = x0 + 1
      Strict:
       {activate#(n__filter(X1, X2, X3)) -> filter#(X1, X2, X3),
             filter#(cons(X, Y), 0(), M) -> activate#(Y),
            filter#(cons(X, Y), s(N), M) -> activate#(Y),
                    sieve#(cons(0(), Y)) -> activate#(Y),
                   sieve#(cons(s(N), Y)) -> activate#(Y),
                   sieve#(cons(s(N), Y)) -> filter#(activate(Y), N, N)}
      Weak:
       {                    activate(X) -> X,
        activate(n__filter(X1, X2, X3)) -> filter(X1, X2, X3),
                  activate(n__sieve(X)) -> sieve(X),
                   activate(n__nats(X)) -> nats(X),
                     filter(X1, X2, X3) -> n__filter(X1, X2, X3),
             filter(cons(X, Y), 0(), M) -> cons(0(), n__filter(activate(Y), M, M)),
            filter(cons(X, Y), s(N), M) -> cons(X, n__filter(activate(Y), N, M)),
                               sieve(X) -> n__sieve(X),
                    sieve(cons(0(), Y)) -> cons(0(), n__sieve(activate(Y))),
                   sieve(cons(s(N), Y)) -> cons(s(N), n__sieve(filter(activate(Y), N, N))),
                                nats(X) -> n__nats(X),
                                nats(N) -> cons(N, n__nats(s(N))),
                              zprimes() -> sieve(nats(s(s(0()))))}
      EDG:
       {(filter#(cons(X, Y), s(N), M) -> activate#(Y), activate#(n__filter(X1, X2, X3)) -> filter#(X1, X2, X3))
        (sieve#(cons(s(N), Y)) -> activate#(Y), activate#(n__filter(X1, X2, X3)) -> filter#(X1, X2, X3))
        (activate#(n__filter(X1, X2, X3)) -> filter#(X1, X2, X3), filter#(cons(X, Y), s(N), M) -> activate#(Y))
        (activate#(n__filter(X1, X2, X3)) -> filter#(X1, X2, X3), filter#(cons(X, Y), 0(), M) -> activate#(Y))
        (sieve#(cons(s(N), Y)) -> filter#(activate(Y), N, N), filter#(cons(X, Y), 0(), M) -> activate#(Y))
        (sieve#(cons(s(N), Y)) -> filter#(activate(Y), N, N), filter#(cons(X, Y), s(N), M) -> activate#(Y))
        (sieve#(cons(0(), Y)) -> activate#(Y), activate#(n__filter(X1, X2, X3)) -> filter#(X1, X2, X3))
        (filter#(cons(X, Y), 0(), M) -> activate#(Y), activate#(n__filter(X1, X2, X3)) -> filter#(X1, X2, X3))}
       SCCS:
        Scc:
         {activate#(n__filter(X1, X2, X3)) -> filter#(X1, X2, X3),
               filter#(cons(X, Y), 0(), M) -> activate#(Y),
              filter#(cons(X, Y), s(N), M) -> activate#(Y)}
        SCC:
         Strict:
          {activate#(n__filter(X1, X2, X3)) -> filter#(X1, X2, X3),
                filter#(cons(X, Y), 0(), M) -> activate#(Y),
               filter#(cons(X, Y), s(N), M) -> activate#(Y)}
         Weak:
         {                    activate(X) -> X,
          activate(n__filter(X1, X2, X3)) -> filter(X1, X2, X3),
                    activate(n__sieve(X)) -> sieve(X),
                     activate(n__nats(X)) -> nats(X),
                       filter(X1, X2, X3) -> n__filter(X1, X2, X3),
               filter(cons(X, Y), 0(), M) -> cons(0(), n__filter(activate(Y), M, M)),
              filter(cons(X, Y), s(N), M) -> cons(X, n__filter(activate(Y), N, M)),
                                 sieve(X) -> n__sieve(X),
                      sieve(cons(0(), Y)) -> cons(0(), n__sieve(activate(Y))),
                     sieve(cons(s(N), Y)) -> cons(s(N), n__sieve(filter(activate(Y), N, N))),
                                  nats(X) -> n__nats(X),
                                  nats(N) -> cons(N, n__nats(s(N))),
                                zprimes() -> sieve(nats(s(s(0()))))}
         SPSC:
          Simple Projection:
           pi(filter#) = 0, pi(activate#) = 0
          Strict:
           { filter#(cons(X, Y), 0(), M) -> activate#(Y),
            filter#(cons(X, Y), s(N), M) -> activate#(Y)}
          EDG:
           {}
           SCCS:
            
            Qed