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