Certification Problem

Input (TPDB TRS_Outermost/Strategy_outermost_added_08/#4.16)

The rewrite relation of the following TRS is considered.

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