Term Rewriting System R:

   [X, Y, M, N]
   filter(cons(X, Y), 0, M) -> cons(0, filter(Y, M, M))
   filter(cons(X, Y), s(N), M) -> cons(X, filter(Y, N, M))
   sieve(cons(0, Y)) -> cons(0, sieve(Y))
   sieve(cons(s(N), Y)) -> cons(s(N), sieve(filter(Y, N, N)))
   nats(N) -> cons(N, nats(s(N)))
   zprimes -> sieve(nats(s(s(0))))

Termination of R to be shown.


This program has no overlaps, so it is sufficient to show innermost termination. 


R contains the following Dependency Pairs: 


   ZPRIMES -> SIEVE(nats(s(s(0))))
   ZPRIMES -> NATS(s(s(0)))
   SIEVE(cons(s(N), Y)) -> SIEVE(filter(Y, N, N))
   SIEVE(cons(s(N), Y)) -> FILTER(Y, N, N)
   SIEVE(cons(0, Y)) -> SIEVE(Y)
   NATS(N) -> NATS(s(N))
   FILTER(cons(X, Y), 0, M) -> FILTER(Y, M, M)
   FILTER(cons(X, Y), s(N), M) -> FILTER(Y, N, M)

Furthermore, R contains three SCCs.


SCC1:

FILTER(cons(X, Y), s(N), M) -> FILTER(Y, N, M)
FILTER(cons(X, Y), 0, M) -> FILTER(Y, M, M)

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

No rules need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
POL(s(x_1)) = 0
POL(FILTER(x_1, x_2, x_3)) = 1 + x_1 + x_3
POL(0) = 0
POL(cons(x_1, x_2)) = 1 + x_1 + x_2

 resulting in no subcycles.


SCC2:

NATS(N) -> NATS(s(N))

Found an infinite P-chain over R:
P = NATS(N) -> NATS(s(N))
R = []
s = NATS(N) evaluates to t = NATS(s(N))
Thus, s starts an infinite reduction as s matches t.


Non-Termination of R could be shown.

Duration: 0.658 seconds.