The rewrite relation of the following TRS is considered.
primes | → | sieve(from(s(s(0)))) | (1) |
from(X) | → | cons(X,n__from(s(X))) | (2) |
head(cons(X,Y)) | → | X | (3) |
tail(cons(X,Y)) | → | activate(Y) | (4) |
if(true,X,Y) | → | activate(X) | (5) |
if(false,X,Y) | → | activate(Y) | (6) |
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)))) | (7) |
sieve(cons(X,Y)) | → | cons(X,n__filter(X,sieve(activate(Y)))) | (8) |
from(X) | → | n__from(X) | (9) |
filter(X1,X2) | → | n__filter(X1,X2) | (10) |
cons(X1,X2) | → | n__cons(X1,X2) | (11) |
activate(n__from(X)) | → | from(X) | (12) |
activate(n__filter(X1,X2)) | → | filter(X1,X2) | (13) |
activate(n__cons(X1,X2)) | → | cons(X1,X2) | (14) |
activate(X) | → | X | (15) |
t0 | = | sieve(cons(X,n__from(x6204))) |
→ | cons(X,n__filter(X,sieve(activate(n__from(x6204))))) | |
→ | cons(X,n__filter(X,sieve(from(x6204)))) | |
→ | cons(X,n__filter(X,sieve(cons(x6204,n__from(s(x6204)))))) | |
= | t3 |