Certification Problem
Input (TPDB TRS_Standard/HirokawaMiddeldorp_04/n005)
The rewrite relation of the following TRS is considered.
Property / Task
Prove or disprove termination.Answer / Result
No.Proof (by AProVE @ termCOMP 2023)
1 Looping derivation
There is a looping derivation.
f →+ ε f f
The derivation can be derived as follows.
-
f →+ f f:
This is an original rule (OC1).