Certification Problem

Input (TPDB TRS_Outermost/Strategy_outermost_added_08/Ex26_Luc03b)

The rewrite relation of the following TRS is considered.

terms(N) → cons(recip(sqr(N)),terms(s(N))) (1)
sqr(0) → 0 (2)
sqr(s(X)) → s(add(sqr(X),dbl(X))) (3)
dbl(0) → 0 (4)
dbl(s(X)) → s(s(dbl(X))) (5)
add(0,X) → X (6)
add(s(X),Y) → s(add(X,Y)) (7)
first(0,X) → nil (8)
first(s(X),cons(Y,Z)) → cons(Y,first(X,Z)) (9)
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 = terms(N)
→ cons(recip(sqr(N)),terms(s(N)))
= t1
where t1 = C[t0σ] and σ = {N/s(N)} and C = cons(recip(sqr(N)),☐)