Certification Problem

Input (TPDB TRS_Standard/Strategy_removed_mixed_05/ExSec11_1_Luc02a)

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)
half(0) → 0 (10)
half(s(0)) → 0 (11)
half(s(s(X))) → s(half(X)) (12)
half(dbl(X)) → X (13)

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by ttt2 @ 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)),☐)