Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/ExIntrod_GM99_L)

The rewrite relation of the following TRS is considered.

tail(cons(X)) Y (1)
if(true) X (2)
if(false) Y (3)
primes sieve(from(s(s(0)))) (4)
from(X) cons(X) (5)
head(cons(X)) X (6)
filter(s(s(X)),cons(Y)) if(divides(s(s(X)),Y)) (7)
sieve(cons(X)) cons(X) (8)

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by AProVE @ termCOMP 2023)

1 Variable Condition Violated

The TRS violates one of the two variable conditions. Thus, it is not terminating.