Certification Problem

Input (TPDB TRS_Standard/Strategy_removed_CSR_05/Ex9_BLR02)

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)

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by ttt2 @ termCOMP 2023)

1 Loop

The following loop proves nontermination.

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