The rewrite relation of the following TRS is considered.
primes |
→ |
sieve(from(s(s(0)))) |
(1) |
from(X) |
→ |
cons(X,n__from(s(X))) |
(2) |
head(cons(X,Y)) |
→ |
X |
(3) |
tail(cons(X,Y)) |
→ |
activate(Y) |
(4) |
if(true,X,Y) |
→ |
activate(X) |
(5) |
if(false,X,Y) |
→ |
activate(Y) |
(6) |
filter(s(s(X)),cons(Y,Z)) |
→ |
if(divides(s(s(X)),Y),n__filter(s(s(X)),activate(Z)),n__cons(Y,n__filter(X,sieve(Y)))) |
(7) |
sieve(cons(X,Y)) |
→ |
cons(X,n__filter(X,sieve(activate(Y)))) |
(8) |
from(X) |
→ |
n__from(X) |
(9) |
filter(X1,X2) |
→ |
n__filter(X1,X2) |
(10) |
cons(X1,X2) |
→ |
n__cons(X1,X2) |
(11) |
activate(n__from(X)) |
→ |
from(X) |
(12) |
activate(n__filter(X1,X2)) |
→ |
filter(X1,X2) |
(13) |
activate(n__cons(X1,X2)) |
→ |
cons(X1,X2) |
(14) |
activate(X) |
→ |
X |
(15) |
primes# |
→ |
sieve#(from(s(s(0)))) |
(16) |
primes# |
→ |
from#(s(s(0))) |
(17) |
from#(X) |
→ |
cons#(X,n__from(s(X))) |
(18) |
tail#(cons(X,Y)) |
→ |
activate#(Y) |
(19) |
if#(true,X,Y) |
→ |
activate#(X) |
(20) |
if#(false,X,Y) |
→ |
activate#(Y) |
(21) |
filter#(s(s(X)),cons(Y,Z)) |
→ |
if#(divides(s(s(X)),Y),n__filter(s(s(X)),activate(Z)),n__cons(Y,n__filter(X,sieve(Y)))) |
(22) |
filter#(s(s(X)),cons(Y,Z)) |
→ |
activate#(Z) |
(23) |
filter#(s(s(X)),cons(Y,Z)) |
→ |
sieve#(Y) |
(24) |
sieve#(cons(X,Y)) |
→ |
cons#(X,n__filter(X,sieve(activate(Y)))) |
(25) |
sieve#(cons(X,Y)) |
→ |
sieve#(activate(Y)) |
(26) |
sieve#(cons(X,Y)) |
→ |
activate#(Y) |
(27) |
activate#(n__from(X)) |
→ |
from#(X) |
(28) |
activate#(n__filter(X1,X2)) |
→ |
filter#(X1,X2) |
(29) |
activate#(n__cons(X1,X2)) |
→ |
cons#(X1,X2) |
(30) |
It remains to prove infiniteness of the resulting DP problem.
primes# |
→ |
sieve#(from(s(s(0)))) |
(16) |
primes# |
→ |
from#(s(s(0))) |
(17) |
from#(X) |
→ |
cons#(X,n__from(s(X))) |
(18) |
tail#(cons(X,Y)) |
→ |
activate#(Y) |
(19) |
if#(true,X,Y) |
→ |
activate#(X) |
(20) |
if#(false,X,Y) |
→ |
activate#(Y) |
(21) |
filter#(s(s(X)),cons(Y,Z)) |
→ |
if#(divides(s(s(X)),Y),n__filter(s(s(X)),activate(Z)),n__cons(Y,n__filter(X,sieve(Y)))) |
(22) |
sieve#(cons(X,Y)) |
→ |
cons#(X,n__filter(X,sieve(activate(Y)))) |
(25) |
activate#(n__from(X)) |
→ |
from#(X) |
(28) |
activate#(n__cons(X1,X2)) |
→ |
cons#(X1,X2) |
(30) |
and the following rules have been deleted.