Certification Problem
Input (TPDB TRS_Standard/HirokawaMiddeldorp_04/n006)
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 g
The derivation can be derived as follows.
-
f →+ f g:
This is an original rule (OC1).