Consider the TRS R consisting of the rewrite rules

1: filter(cons(X,Y),0,M) -> cons(0,n__filter(activate(Y),M,M))
2: filter(cons(X,Y),s(N),M) -> cons(X,n__filter(activate(Y),N,M))
3: sieve(cons(0,Y)) -> cons(0,n__sieve(activate(Y)))
4: sieve(cons(s(N),Y)) -> cons(s(N),n__sieve(filter(activate(Y),N,N)))
5: nats(N) -> cons(N,n__nats(s(N)))
6: zprimes -> sieve(nats(s(s(0))))
7: filter(X1,X2,X3) -> n__filter(X1,X2,X3)
8: sieve(X) -> n__sieve(X)
9: nats(X) -> n__nats(X)
10: activate(n__filter(X1,X2,X3)) -> filter(X1,X2,X3)
11: activate(n__sieve(X)) -> sieve(X)
12: activate(n__nats(X)) -> nats(X)
13: activate(X) -> X

There are 10 dependency pairs:

14: FILTER(cons(X,Y),0,M) -> ACTIVATE(Y)
15: FILTER(cons(X,Y),s(N),M) -> ACTIVATE(Y)
16: SIEVE(cons(0,Y)) -> ACTIVATE(Y)
17: SIEVE(cons(s(N),Y)) -> FILTER(activate(Y),N,N)
18: SIEVE(cons(s(N),Y)) -> ACTIVATE(Y)
19: ZPRIMES -> SIEVE(nats(s(s(0))))
20: ZPRIMES -> NATS(s(s(0)))
21: ACTIVATE(n__filter(X1,X2,X3)) -> FILTER(X1,X2,X3)
22: ACTIVATE(n__sieve(X)) -> SIEVE(X)
23: ACTIVATE(n__nats(X)) -> NATS(X)

The approximated dependency graph contains one SCC:
{14-18,21,22}.

- Consider the SCC {14-18,21,22}.
The usable rules are {1-5,7-13}.
By taking the polynomial interpretation
[0] = [s](x) = 0,
[activate](x) = [filter](x,y,z) = [n__filter](x,y,z) = x,
[ACTIVATE](x) = [FILTER](x,y,z) = [n__nats](x) = [n__sieve](x) = [nats](x) = [sieve](x) = [SIEVE](x) = x + 1
and [cons](x,y) = x + y,
the rules in {1-5,7-18,21}
are weakly decreasing and
rule 22
is strictly decreasing.
There is one new SCC.

- Consider the SCC {14,15,21}.
There are no usable rules.
By taking the polynomial interpretation
[0] = 1,
[ACTIVATE](x) = [s](x) = x + 1,
[cons](x,y) = x + y + 1
and [FILTER](x,y,z) = [n__filter](x,y,z) = x + y + z + 1,
the rules in {14,15,21}
are strictly decreasing.


Hence the TRS is terminating.