YES
Termination Proof
Termination Proof
by ttt2 (version ttt2 1.15)
Input
The rewrite relation of the following TRS is considered.
a(p(x0)) |
→ |
p(a(A(x0))) |
a(A(x0)) |
→ |
A(a(x0)) |
p(A(A(x0))) |
→ |
a(p(x0)) |
Proof
1 String Reversal
Since only unary symbols occur, one can reverse all terms and obtains the TRS
p(a(x0)) |
→ |
A(a(p(x0))) |
A(a(x0)) |
→ |
a(A(x0)) |
A(A(p(x0))) |
→ |
p(a(x0)) |
1.1 Rule Removal
Using the
linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1
over the naturals
[a(x1)] |
= |
·
x1 +
|
[p(x1)] |
= |
·
x1 +
|
[A(x1)] |
= |
·
x1 +
|
the
rules
p(a(x0)) |
→ |
A(a(p(x0))) |
A(a(x0)) |
→ |
a(A(x0)) |
remain.
1.1.1 String Reversal
Since only unary symbols occur, one can reverse all terms and obtains the TRS
a(p(x0)) |
→ |
p(a(A(x0))) |
a(A(x0)) |
→ |
A(a(x0)) |
1.1.1.1 Bounds
The given TRS is
match-bounded by 1.
This is shown by the following automaton.
-
final states:
{5, 1}
-
transitions:
9 |
→ |
4 |
5 |
→ |
6 |
5 |
→ |
8 |
1 |
→ |
6 |
1 |
→ |
8 |
2 |
→ |
7 |
a1(7) |
→ |
8 |
f30
|
→ |
2 |
p0(4) |
→ |
1 |
A0(2) |
→ |
3 |
A0(6) |
→ |
5 |
A1(8) |
→ |
9 |
a0(2) |
→ |
6 |
a0(3) |
→ |
4 |