Certification Problem
Input (TPDB TRS_Innermost/Transformed_CSR_innermost_04/Ex23_Luc06_L)
The rewrite relation of the following TRS is considered.
The evaluation strategy is innermost.Property / Task
Prove or disprove termination.Answer / Result
Yes.Proof (by AProVE @ termCOMP 2023)
1 Constant to Unary
Every constant is turned into a unary function symbol to obtain the TRS
1.1 String Reversal
Since only unary symbols occur, one can reverse all terms and obtains the TRS
1.1.1 Bounds
The given TRS is
match-(raise)-bounded by 1.
This is shown by the following automaton.
-
final states:
{0, 1, 2}
-
transitions:
|
a'0(0) |
→ |
0 |
|
a'0(1) |
→ |
0 |
|
a'0(2) |
→ |
0 |
|
f0(0) |
→ |
1 |
|
f0(1) |
→ |
1 |
|
f0(2) |
→ |
1 |
|
c'0(0) |
→ |
2 |
|
c'0(1) |
→ |
2 |
|
c'0(2) |
→ |
2 |
|
c'1(0) |
→ |
0 |
|
c'1(1) |
→ |
0 |
|
c'1(2) |
→ |
0 |