Certification Problem
Input (TPDB TRS_Standard/Transformed_CSR_04/Ex4_4_Luc96b_L)
The rewrite relation of the following TRS is considered.
Property / Task
Prove or disprove termination.Answer / Result
Yes.Proof (by ttt2 @ termCOMP 2023)
1 String Reversal
Since only unary symbols occur, one can reverse all terms and obtains the TRS
1.1 Rule Removal
Using the
Weighted Path Order with the following precedence and status
prec(f) |
= |
0 |
|
status(f) |
= |
[1] |
|
list-extension(f) |
= |
Lex |
prec(g) |
= |
0 |
|
status(g) |
= |
[1] |
|
list-extension(g) |
= |
Lex |
and the following
Max-polynomial interpretation
[f(x1)] |
=
|
max(0, 6 + 1 · x1) |
[g(x1)] |
=
|
max(0, 0 + 1 · x1) |
all of the following rules can be deleted.
1.1.1 R is empty
There are no rules in the TRS. Hence, it is terminating.