Certification Problem

Input (TPDB TRS_Outermost/Strategy_outermost_added_08/ExAppendixB_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,Z)) → 2ndspos(s(N),cons2(X,Z)) (3)
2ndspos(s(N),cons2(X,cons(Y,Z))) → rcons(posrecip(Y),2ndsneg(N,Z)) (4)
2ndsneg(0,Z) → rnil (5)
2ndsneg(s(N),cons(X,Z)) → 2ndsneg(s(N),cons2(X,Z)) (6)
2ndsneg(s(N),cons2(X,cons(Y,Z))) → rcons(negrecip(Y),2ndspos(N,Z)) (7)
pi(X) → 2ndspos(X,from(0)) (8)
plus(0,Y) → Y (9)
plus(s(X),Y) → s(plus(X,Y)) (10)
times(0,Y) → 0 (11)
times(s(X),Y) → plus(Y,times(X,Y)) (12)
square(X) → times(X,X) (13)
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 = from(X)
→ cons(X,from(s(X)))
= t1
where t1 = C[t0σ] and σ = {X/s(X)} and C = cons(X,☐)