The rewrite relation of the following TRS is considered.
tail(cons(X)) | → | Y | (1) |
if(true) | → | X | (2) |
if(false) | → | Y | (3) |
primes | → | sieve(from(s(s(0)))) | (4) |
from(X) | → | cons(X) | (5) |
head(cons(X)) | → | X | (6) |
filter(s(s(X)),cons(Y)) | → | if(divides(s(s(X)),Y)) | (7) |
sieve(cons(X)) | → | cons(X) | (8) |
The TRS violates one of the two variable conditions. Thus, it is not terminating.