Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/ExIntrod_GM99_Z)

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)

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by ttt2 @ termCOMP 2023)

1 Loop

The following loop proves nontermination.

t0 = sieve(cons(X,n__from(x6204)))
→ cons(X,n__filter(X,sieve(activate(n__from(x6204)))))
→ cons(X,n__filter(X,sieve(from(x6204))))
→ cons(X,n__filter(X,sieve(cons(x6204,n__from(s(x6204))))))
= t3
where t3 = C[t0σ] and σ = {x6204/s(x6204), X/x6204} and C = cons(X,n__filter(X,☐))