Term Rewriting System R:

   [X, Y, Z, X1, X2]
   primes -> sieve(from(s(s(0))))
   from(X) -> cons(X, n__from(s(X)))
   from(X) -> n__from(X)
   head(cons(X, Y)) -> X
   tail(cons(X, Y)) -> activate(Y)
   if(true, X, Y) -> activate(X)
   if(false, X, Y) -> activate(Y)
   filter(s(s(X)), cons(Y, Z)) -> if(divides(s(s(X)), Y), n__filter(s(s(X)), activate(Z)), n__cons(Y, n__filter(X, sieve(Y))))
   filter(X1, X2) -> n__filter(X1, X2)
   sieve(cons(X, Y)) -> cons(X, n__filter(X, sieve(activate(Y))))
   cons(X1, X2) -> n__cons(X1, X2)
   activate(n__from(X)) -> from(X)
   activate(n__filter(X1, X2)) -> filter(X1, X2)
   activate(n__cons(X1, X2)) -> cons(X1, X2)
   activate(X) -> X

Termination of R to be shown.


R contains the following Dependency Pairs: 


   SIEVE(cons(X, Y)) -> CONS(X, n__filter(X, sieve(activate(Y))))
   SIEVE(cons(X, Y)) -> SIEVE(activate(Y))
   SIEVE(cons(X, Y)) -> ACTIVATE(Y)
   ACTIVATE(n__from(X)) -> FROM(X)
   ACTIVATE(n__filter(X1, X2)) -> FILTER(X1, X2)
   ACTIVATE(n__cons(X1, X2)) -> CONS(X1, X2)
   FILTER(s(s(X)), cons(Y, Z)) -> IF(divides(s(s(X)), Y), n__filter(s(s(X)), activate(Z)), n__cons(Y, n__filter(X, sieve(Y))))
   FILTER(s(s(X)), cons(Y, Z)) -> ACTIVATE(Z)
   FILTER(s(s(X)), cons(Y, Z)) -> SIEVE(Y)
   FROM(X) -> CONS(X, n__from(s(X)))
   IF(false, X, Y) -> ACTIVATE(Y)
   IF(true, X, Y) -> ACTIVATE(X)
   TAIL(cons(X, Y)) -> ACTIVATE(Y)
   PRIMES -> SIEVE(from(s(s(0))))
   PRIMES -> FROM(s(s(0)))

Furthermore, R contains one SCC.


SCC1:

FILTER(s(s(X)), cons(Y, Z)) -> SIEVE(Y)
FILTER(s(s(X)), cons(Y, Z)) -> ACTIVATE(Z)
ACTIVATE(n__filter(X1, X2)) -> FILTER(X1, X2)
SIEVE(cons(X, Y)) -> ACTIVATE(Y)
SIEVE(cons(X, Y)) -> SIEVE(activate(Y))

Found an infinite P-chain over R:
P = FILTER(s(s(X)), cons(Y, Z)) -> SIEVE(Y)
FILTER(s(s(X)), cons(Y, Z)) -> ACTIVATE(Z)
ACTIVATE(n__filter(X1, X2)) -> FILTER(X1, X2)
SIEVE(cons(X, Y)) -> ACTIVATE(Y)
SIEVE(cons(X, Y)) -> SIEVE(activate(Y))
R = [sieve(cons(X, Y)) -> cons(X, n__filter(X, sieve(activate(Y)))), cons(X1, X2) -> n__cons(X1, X2), activate(n__from(X)) -> from(X), activate(X) -> X, activate(n__filter(X1, X2)) -> filter(X1, X2), activate(n__cons(X1, X2)) -> cons(X1, X2), filter(X1, X2) -> n__filter(X1, X2), filter(s(s(X)), cons(Y, Z)) -> if(divides(s(s(X)), Y), n__filter(s(s(X)), activate(Z)), n__cons(Y, n__filter(X, sieve(Y)))), from(X) -> cons(X, n__from(s(X))), from(X) -> n__from(X), if(false, X, Y) -> activate(Y), if(true, X, Y) -> activate(X), head(cons(X, Y)) -> X, tail(cons(X, Y)) -> activate(Y), primes -> sieve(from(s(s(0))))]
s = SIEVE(cons(X, n__from(X'''))) evaluates to t = SIEVE(cons(X''', n__from(s(X'''))))
Thus, s starts an infinite reduction as s matches t.


Non-Termination of R could be shown.

Duration: 3.310 seconds.