The rewrite relation of the following TRS is considered.
filter(cons(X,Y),0,M) | → | cons(0,filter(Y,M,M)) | (1) |
filter(cons(X,Y),s(N),M) | → | cons(X,filter(Y,N,M)) | (2) |
sieve(cons(0,Y)) | → | cons(0,sieve(Y)) | (3) |
sieve(cons(s(N),Y)) | → | cons(s(N),sieve(filter(Y,N,N))) | (4) |
nats(N) | → | cons(N,nats(s(N))) | (5) |
zprimes | → | sieve(nats(s(s(0)))) | (6) |
filter(cons(x0,x1),0,x2) |
filter(cons(x0,x1),s(x2),x3) |
sieve(cons(0,x0)) |
sieve(cons(s(x0),x1)) |
nats(x0) |
zprimes |
filter#(cons(X,Y),0,M) | → | filter#(Y,M,M) | (7) |
filter#(cons(X,Y),s(N),M) | → | filter#(Y,N,M) | (8) |
sieve#(cons(0,Y)) | → | sieve#(Y) | (9) |
sieve#(cons(s(N),Y)) | → | sieve#(filter(Y,N,N)) | (10) |
sieve#(cons(s(N),Y)) | → | filter#(Y,N,N) | (11) |
nats#(N) | → | nats#(s(N)) | (12) |
zprimes# | → | sieve#(nats(s(s(0)))) | (13) |
zprimes# | → | nats#(s(s(0))) | (14) |
filter#(cons(X,Y),0,M) | → | filter#(Y,M,M) | (7) |
filter#(cons(X,Y),s(N),M) | → | filter#(Y,N,M) | (8) |
sieve#(cons(0,Y)) | → | sieve#(Y) | (9) |
sieve#(cons(s(N),Y)) | → | sieve#(filter(Y,N,N)) | (10) |
sieve#(cons(s(N),Y)) | → | filter#(Y,N,N) | (11) |
zprimes# | → | sieve#(nats(s(s(0)))) | (13) |
zprimes# | → | nats#(s(s(0))) | (14) |
filter(cons(X,Y),0,M) | → | cons(0,filter(Y,M,M)) | (1) |
filter(cons(X,Y),s(N),M) | → | cons(X,filter(Y,N,M)) | (2) |
sieve(cons(0,Y)) | → | cons(0,sieve(Y)) | (3) |
sieve(cons(s(N),Y)) | → | cons(s(N),sieve(filter(Y,N,N))) | (4) |
nats(N) | → | cons(N,nats(s(N))) | (5) |
zprimes | → | sieve(nats(s(s(0)))) | (6) |
We restrict the innermost strategy to the following left hand sides.
There are no lhss.
nats#(s(z0)) | → | nats#(s(s(z0))) | (15) |
nats#(s(s(z0))) | → | nats#(s(s(s(z0)))) | (16) |
t0 | = | nats#(s(s(z0))) |
→P | nats#(s(s(s(z0)))) | |
= | t1 |