Consider the TRS R consisting of the rewrite rules

1: a__filter(cons(X,Y),0,M) -> cons(0,filter(Y,M,M))
2: a__filter(cons(X,Y),s(N),M) -> cons(mark(X),filter(Y,N,M))
3: a__sieve(cons(0,Y)) -> cons(0,sieve(Y))
4: a__sieve(cons(s(N),Y)) -> cons(s(mark(N)),sieve(filter(Y,N,N)))
5: a__nats(N) -> cons(mark(N),nats(s(N)))
6: a__zprimes -> a__sieve(a__nats(s(s(0))))
7: mark(filter(X1,X2,X3)) -> a__filter(mark(X1),mark(X2),mark(X3))
8: mark(sieve(X)) -> a__sieve(mark(X))
9: mark(nats(X)) -> a__nats(mark(X))
10: mark(zprimes) -> a__zprimes
11: mark(cons(X1,X2)) -> cons(mark(X1),X2)
12: mark(0) -> 0
13: mark(s(X)) -> s(mark(X))
14: a__filter(X1,X2,X3) -> filter(X1,X2,X3)
15: a__sieve(X) -> sieve(X)
16: a__nats(X) -> nats(X)
17: a__zprimes -> zprimes

There are 16 dependency pairs:

18: A__FILTER(cons(X,Y),s(N),M) -> MARK(X)
19: A__SIEVE(cons(s(N),Y)) -> MARK(N)
20: A__NATS(N) -> MARK(N)
21: A__ZPRIMES -> A__SIEVE(a__nats(s(s(0))))
22: A__ZPRIMES -> A__NATS(s(s(0)))
23: MARK(filter(X1,X2,X3)) -> A__FILTER(mark(X1),mark(X2),mark(X3))
24: MARK(filter(X1,X2,X3)) -> MARK(X1)
25: MARK(filter(X1,X2,X3)) -> MARK(X2)
26: MARK(filter(X1,X2,X3)) -> MARK(X3)
27: MARK(sieve(X)) -> A__SIEVE(mark(X))
28: MARK(sieve(X)) -> MARK(X)
29: MARK(nats(X)) -> A__NATS(mark(X))
30: MARK(nats(X)) -> MARK(X)
31: MARK(zprimes) -> A__ZPRIMES
32: MARK(cons(X1,X2)) -> MARK(X1)
33: MARK(s(X)) -> MARK(X)

The approximated dependency graph contains one SCC:
{18-33}.

- Consider the SCC {18-33}.
By taking the polynomial interpretation
[0] = [a__zprimes] = [A__ZPRIMES] = [zprimes] = 1,
[a__nats](x) = [A__NATS](x) = [a__sieve](x) = [A__SIEVE](x) = [cons](x,y) = [mark](x) = [MARK](x) = [nats](x) = [s](x) = [sieve](x) = x
and [a__filter](x,y,z) = [A__FILTER](x,y,z) = [filter](x,y,z) = x + y + z + 1,
the rules in {3-17,19-23,27-33}
are weakly decreasing and
the rules in {1,2,18,24-26}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {19-22,27-33}.
By taking the polynomial interpretation
[0] = 0,
[a__zprimes] = [A__ZPRIMES] = [zprimes] = 1,
[a__sieve](x) = [A__SIEVE](x) = [mark](x) = [s](x) = [sieve](x) = x,
[a__nats](x) = [A__NATS](x) = [cons](x,y) = [MARK](x) = [nats](x) = x + 1
and [a__filter](x,y,z) = [filter](x,y,z) = x + y + z + 1,
the rules in {3-17,19-22,28,33}
are weakly decreasing and
the rules in {1,2,27,29-32}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {28,33}.
There are no usable rules.
By taking the polynomial interpretation
[MARK](x) = [s](x) = [sieve](x) = x + 1,
the rules in {28,33}
are strictly decreasing.



Hence the TRS is terminating.