(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
active(primes) → mark(sieve(from(s(s(0)))))
active(from(X)) → mark(cons(X, from(s(X))))
active(head(cons(X, Y))) → mark(X)
active(tail(cons(X, Y))) → mark(Y)
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(filter(s(s(X)), cons(Y, Z))) → mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y)))))
active(sieve(cons(X, Y))) → mark(cons(X, filter(X, sieve(Y))))
mark(primes) → active(primes)
mark(sieve(X)) → active(sieve(mark(X)))
mark(from(X)) → active(from(mark(X)))
mark(s(X)) → active(s(mark(X)))
mark(0) → active(0)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))
mark(true) → active(true)
mark(false) → active(false)
mark(filter(X1, X2)) → active(filter(mark(X1), mark(X2)))
mark(divides(X1, X2)) → active(divides(mark(X1), mark(X2)))
sieve(mark(X)) → sieve(X)
sieve(active(X)) → sieve(X)
from(mark(X)) → from(X)
from(active(X)) → from(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
filter(mark(X1), X2) → filter(X1, X2)
filter(X1, mark(X2)) → filter(X1, X2)
filter(active(X1), X2) → filter(X1, X2)
filter(X1, active(X2)) → filter(X1, X2)
divides(mark(X1), X2) → divides(X1, X2)
divides(X1, mark(X2)) → divides(X1, X2)
divides(active(X1), X2) → divides(X1, X2)
divides(X1, active(X2)) → divides(X1, X2)
Q is empty.