Certification Problem

Input (TPDB TRS_Standard/Strategy_removed_CSR_05/Ex1_2_AEL03)

The rewrite relation of the following TRS is considered.

from(X) → cons(X,from(s(X))) (1)
2ndspos(0,Z) → rnil (2)
2ndspos(s(N),cons(X,cons(Y,Z))) → rcons(posrecip(Y),2ndsneg(N,Z)) (3)
2ndsneg(0,Z) → rnil (4)
2ndsneg(s(N),cons(X,cons(Y,Z))) → rcons(negrecip(Y),2ndspos(N,Z)) (5)
pi(X) → 2ndspos(X,from(0)) (6)
plus(0,Y) → Y (7)
plus(s(X),Y) → s(plus(X,Y)) (8)
times(0,Y) → 0 (9)
times(s(X),Y) → plus(Y,times(X,Y)) (10)
square(X) → times(X,X) (11)

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by ttt2 @ termCOMP 2023)

1 Loop

The following loop proves nontermination.

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