Certification Problem

Input (TPDB TRS_Outermost/Strategy_outermost_added_08/ExIntrod_GM99)

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)
The evaluation strategy is outermost

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by AProVE @ termCOMP 2023)

1 Loop

The following loop proves nontermination.

t0 = from(X)
→ cons(X,from(s(X)))
= t1
where t1 = C[t0σ] and σ = {X/s(X)} and C = cons(X,☐)