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) |
primes |
from(x0) |
head(cons(x0,x1)) |
tail(cons(x0,x1)) |
if(true,x0,x1) |
if(false,x0,x1) |
filter(s(s(x0)),cons(x1,x2)) |
sieve(cons(x0,x1)) |
primes# | → | sieve#(from(s(s(0)))) | (9) |
primes# | → | from#(s(s(0))) | (10) |
from#(X) | → | from#(s(X)) | (11) |
filter#(s(s(X)),cons(Y,Z)) | → | if#(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y)))) | (12) |
filter#(s(s(X)),cons(Y,Z)) | → | filter#(s(s(X)),Z) | (13) |
filter#(s(s(X)),cons(Y,Z)) | → | filter#(X,sieve(Y)) | (14) |
filter#(s(s(X)),cons(Y,Z)) | → | sieve#(Y) | (15) |
sieve#(cons(X,Y)) | → | filter#(X,sieve(Y)) | (16) |
sieve#(cons(X,Y)) | → | sieve#(Y) | (17) |
primes# | → | sieve#(from(s(s(0)))) | (9) |
primes# | → | from#(s(s(0))) | (10) |
filter#(s(s(X)),cons(Y,Z)) | → | if#(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y)))) | (12) |
filter#(s(s(X)),cons(Y,Z)) | → | filter#(s(s(X)),Z) | (13) |
filter#(s(s(X)),cons(Y,Z)) | → | filter#(X,sieve(Y)) | (14) |
filter#(s(s(X)),cons(Y,Z)) | → | sieve#(Y) | (15) |
sieve#(cons(X,Y)) | → | filter#(X,sieve(Y)) | (16) |
sieve#(cons(X,Y)) | → | sieve#(Y) | (17) |
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) |
We restrict the innermost strategy to the following left hand sides.
There are no lhss.
from#(s(z0)) | → | from#(s(s(z0))) | (18) |
from#(s(s(z0))) | → | from#(s(s(s(z0)))) | (19) |
t0 | = | from#(s(s(z0))) |
→P | from#(s(s(s(z0)))) | |
= | t1 |