YES
Termination Proof
Termination Proof
by ttt2 (version ttt2 1.15)
Input
The rewrite relation of the following TRS is considered.
|
c(c(x0)) |
→ |
a(a(a(b(b(b(x0)))))) |
|
b(b(b(a(x0)))) |
→ |
b(b(b(b(b(b(b(b(x0)))))))) |
|
b(b(c(c(x0)))) |
→ |
c(c(c(a(a(a(a(x0))))))) |
Proof
1 Rule Removal
Using the
linear polynomial interpretation over (2 x 2)-matrices with strict dimension 1
over the arctic semiring over the integers
| [b(x1)] |
= |
·
x1 +
|
| [c(x1)] |
= |
·
x1 +
|
| [a(x1)] |
= |
·
x1 +
|
the
rules
|
b(b(b(a(x0)))) |
→ |
b(b(b(b(b(b(b(b(x0)))))))) |
|
b(b(c(c(x0)))) |
→ |
c(c(c(a(a(a(a(x0))))))) |
remain.
1.1 String Reversal
Since only unary symbols occur, one can reverse all terms and obtains the TRS
|
a(b(b(b(x0)))) |
→ |
b(b(b(b(b(b(b(b(x0)))))))) |
|
c(c(b(b(x0)))) |
→ |
a(a(a(a(c(c(c(x0))))))) |
1.1.1 Bounds
The given TRS is
match-bounded by 0.
This is shown by the following automaton.
-
final states:
{10, 1}
-
transitions:
| 10 |
→ |
12 |
| 10 |
→ |
11 |
|
c0(11) |
→ |
12 |
|
c0(2) |
→ |
11 |
|
c0(12) |
→ |
13 |
|
b0(5) |
→ |
6 |
|
b0(7) |
→ |
8 |
|
b0(9) |
→ |
1 |
|
b0(8) |
→ |
9 |
|
b0(2) |
→ |
3 |
|
b0(6) |
→ |
7 |
|
b0(4) |
→ |
5 |
|
b0(3) |
→ |
4 |
|
f30
|
→ |
2 |
|
a0(15) |
→ |
16 |
|
a0(13) |
→ |
14 |
|
a0(14) |
→ |
15 |
|
a0(16) |
→ |
10 |