Certification Problem

Input (TPDB TRS_Relative/INVY_15/ex7)

The relative rewrite relation R/S is considered where R is the following TRS

f(s(x)) → f(x) (1)

and S is the following TRS.

inf → s(inf) (2)

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by AProVE @ termCOMP 2023)

1 Loop

The following loop proves that R/S is not relative terminating.

t0 = f(inf)
→S f(s(inf))
→R f(inf)
= t2
where t2 = t0