Certification Problem

Input (TPDB TRS_Outermost/Strategy_outermost_added_08/#4.17)

The rewrite relation of the following TRS is considered.

f(g(x),s(0),y) f(g(s(0)),y,g(x)) (1)
g(s(x)) s(g(x)) (2)
g(0) 0 (3)
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 = f(g(s(0)),g(s(0)),g(s(0)))
f(g(s(0)),s(g(0)),g(s(0)))
f(g(s(0)),s(0),g(s(0)))
f(g(s(0)),g(s(0)),g(s(0)))
= t3
where t3 = t0