Certification Problem
Input (TPDB TRS_Standard/Strategy_removed_mixed_05/n001)
The rewrite relation of the following TRS is considered.
|
h(f(f(x))) |
→ |
h(f(g(f(x)))) |
(1) |
|
f(g(f(x))) |
→ |
f(f(x)) |
(2) |
Property / Task
Prove or disprove termination.Answer / Result
No.Proof (by AProVE @ termCOMP 2023)
1 Looping derivation
There is a looping derivation.
h f f →+ ε h f f ε
The derivation can be derived as follows.
-
h f f →+ h f g f:
This is an original rule (OC1).
-
f g f →+ f f:
This is an original rule (OC1).
-
h f f →+ h f f:
The overlap closure is obtained from the following two overlap closures (OC2).
-
h f f →+ h f g f
-
f g f →+ f f