YES
Termination Proof
Termination Proof
by ttt2 (version ttt2 1.15)
Input
The rewrite relation of the following TRS is considered.
|
a(b(a(x0))) |
→ |
a(b(b(a(x0)))) |
|
b(b(b(x0))) |
→ |
b(b(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 +
|
| [a(x1)] |
= |
·
x1 +
|
the
rule
|
a(b(a(x0))) |
→ |
a(b(b(a(x0)))) |
remains.
1.1 Bounds
The given TRS is
match-bounded by 0.
This is shown by the following automaton.
-
final states:
{1}
-
transitions:
| 1 |
→ |
3 |
|
a0(2) |
→ |
3 |
|
a0(5) |
→ |
1 |
|
b0(4) |
→ |
5 |
|
b0(3) |
→ |
4 |
|
f20
|
→ |
2 |