The rewrite relation of the following TRS is considered.
primes | → | sieve(from(s(s(0)))) | (1) |
from(X) | → | cons(X,from(s(X))) | (2) |
head(cons(X,Y)) | → | X | (3) |
tail(cons(X,Y)) | → | Y | (4) |
if(true,X,Y) | → | X | (5) |
if(false,X,Y) | → | Y | (6) |
filter(s(s(X)),cons(Y,Z)) | → | if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y)))) | (7) |
sieve(cons(X,Y)) | → | cons(X,filter(X,sieve(Y))) | (8) |
t0 | = | from(X) |
→ | cons(X,from(s(X))) | |
= | t1 |