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