YES
Termination Proof
Termination Proof
by ttt2 (version ttt2 1.15)
Input
The rewrite relation of the following TRS is considered.
|
2(7(x0)) |
→ |
1(8(x0)) |
|
2(8(1(x0))) |
→ |
8(x0) |
|
2(8(x0)) |
→ |
4(x0) |
|
5(9(x0)) |
→ |
0(x0) |
|
4(x0) |
→ |
5(2(3(x0))) |
|
5(3(x0)) |
→ |
6(0(x0)) |
|
2(8(x0)) |
→ |
7(x0) |
|
4(7(x0)) |
→ |
1(3(x0)) |
|
5(2(6(x0))) |
→ |
6(2(4(x0))) |
|
9(7(x0)) |
→ |
7(5(x0)) |
|
7(2(x0)) |
→ |
4(x0) |
|
7(0(x0)) |
→ |
9(3(x0)) |
|
6(9(x0)) |
→ |
9(x0) |
|
9(5(9(x0))) |
→ |
5(7(x0)) |
|
4(x0) |
→ |
9(6(6(x0))) |
|
9(x0) |
→ |
6(7(x0)) |
|
6(2(x0)) |
→ |
7(7(x0)) |
|
2(4(x0)) |
→ |
0(7(x0)) |
|
6(6(x0)) |
→ |
3(x0) |
|
0(3(x0)) |
→ |
5(3(x0)) |
Proof
1 String Reversal
Since only unary symbols occur, one can reverse all terms and obtains the TRS
|
7(2(x0)) |
→ |
8(1(x0)) |
|
1(8(2(x0))) |
→ |
8(x0) |
|
8(2(x0)) |
→ |
4(x0) |
|
9(5(x0)) |
→ |
0(x0) |
|
4(x0) |
→ |
3(2(5(x0))) |
|
3(5(x0)) |
→ |
0(6(x0)) |
|
8(2(x0)) |
→ |
7(x0) |
|
7(4(x0)) |
→ |
3(1(x0)) |
|
6(2(5(x0))) |
→ |
4(2(6(x0))) |
|
7(9(x0)) |
→ |
5(7(x0)) |
|
2(7(x0)) |
→ |
4(x0) |
|
0(7(x0)) |
→ |
3(9(x0)) |
|
9(6(x0)) |
→ |
9(x0) |
|
9(5(9(x0))) |
→ |
7(5(x0)) |
|
4(x0) |
→ |
6(6(9(x0))) |
|
9(x0) |
→ |
7(6(x0)) |
|
2(6(x0)) |
→ |
7(7(x0)) |
|
4(2(x0)) |
→ |
7(0(x0)) |
|
6(6(x0)) |
→ |
3(x0) |
|
3(0(x0)) |
→ |
3(5(x0)) |
1.1 Rule Removal
Using the
linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1
over the naturals
| [4(x1)] |
= |
·
x1 +
|
| [3(x1)] |
= |
·
x1 +
|
| [2(x1)] |
= |
·
x1 +
|
| [1(x1)] |
= |
·
x1 +
|
| [9(x1)] |
= |
·
x1 +
|
| [7(x1)] |
= |
·
x1 +
|
| [0(x1)] |
= |
·
x1 +
|
| [6(x1)] |
= |
·
x1 +
|
| [5(x1)] |
= |
·
x1 +
|
| [8(x1)] |
= |
·
x1 +
|
the
rules
|
7(2(x0)) |
→ |
8(1(x0)) |
|
9(5(x0)) |
→ |
0(x0) |
|
4(x0) |
→ |
3(2(5(x0))) |
|
3(5(x0)) |
→ |
0(6(x0)) |
|
7(4(x0)) |
→ |
3(1(x0)) |
|
6(2(5(x0))) |
→ |
4(2(6(x0))) |
|
7(9(x0)) |
→ |
5(7(x0)) |
|
2(7(x0)) |
→ |
4(x0) |
|
0(7(x0)) |
→ |
3(9(x0)) |
|
9(6(x0)) |
→ |
9(x0) |
|
9(5(9(x0))) |
→ |
7(5(x0)) |
|
4(x0) |
→ |
6(6(9(x0))) |
|
9(x0) |
→ |
7(6(x0)) |
|
2(6(x0)) |
→ |
7(7(x0)) |
|
4(2(x0)) |
→ |
7(0(x0)) |
|
6(6(x0)) |
→ |
3(x0) |
|
3(0(x0)) |
→ |
3(5(x0)) |
remain.
1.1.1 Rule Removal
Using the
linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1
over the naturals
| [4(x1)] |
= |
·
x1 +
|
| [3(x1)] |
= |
·
x1 +
|
| [2(x1)] |
= |
·
x1 +
|
| [1(x1)] |
= |
·
x1 +
|
| [9(x1)] |
= |
·
x1 +
|
| [7(x1)] |
= |
·
x1 +
|
| [0(x1)] |
= |
·
x1 +
|
| [6(x1)] |
= |
·
x1 +
|
| [5(x1)] |
= |
·
x1 +
|
| [8(x1)] |
= |
·
x1 +
|
the
rules
|
7(2(x0)) |
→ |
8(1(x0)) |
|
9(5(x0)) |
→ |
0(x0) |
|
4(x0) |
→ |
3(2(5(x0))) |
|
3(5(x0)) |
→ |
0(6(x0)) |
|
7(4(x0)) |
→ |
3(1(x0)) |
|
7(9(x0)) |
→ |
5(7(x0)) |
|
2(7(x0)) |
→ |
4(x0) |
|
0(7(x0)) |
→ |
3(9(x0)) |
|
9(6(x0)) |
→ |
9(x0) |
|
9(5(9(x0))) |
→ |
7(5(x0)) |
|
4(x0) |
→ |
6(6(9(x0))) |
|
9(x0) |
→ |
7(6(x0)) |
|
2(6(x0)) |
→ |
7(7(x0)) |
|
6(6(x0)) |
→ |
3(x0) |
|
3(0(x0)) |
→ |
3(5(x0)) |
remain.
1.1.1.1 Rule Removal
Using the
linear polynomial interpretation over the arctic semiring over the integers
| [4(x1)] |
= |
4 ·
x1 +
-∞
|
| [3(x1)] |
= |
0 ·
x1 +
-∞
|
| [2(x1)] |
= |
4 ·
x1 +
-∞
|
| [1(x1)] |
= |
0 ·
x1 +
-∞
|
| [9(x1)] |
= |
0 ·
x1 +
-∞
|
| [7(x1)] |
= |
0 ·
x1 +
-∞
|
| [0(x1)] |
= |
0 ·
x1 +
-∞
|
| [6(x1)] |
= |
0 ·
x1 +
-∞
|
| [5(x1)] |
= |
0 ·
x1 +
-∞
|
| [8(x1)] |
= |
3 ·
x1 +
-∞
|
the
rules
|
9(5(x0)) |
→ |
0(x0) |
|
4(x0) |
→ |
3(2(5(x0))) |
|
3(5(x0)) |
→ |
0(6(x0)) |
|
7(9(x0)) |
→ |
5(7(x0)) |
|
2(7(x0)) |
→ |
4(x0) |
|
0(7(x0)) |
→ |
3(9(x0)) |
|
9(6(x0)) |
→ |
9(x0) |
|
9(5(9(x0))) |
→ |
7(5(x0)) |
|
9(x0) |
→ |
7(6(x0)) |
|
6(6(x0)) |
→ |
3(x0) |
|
3(0(x0)) |
→ |
3(5(x0)) |
remain.
1.1.1.1.1 Rule Removal
Using the
linear polynomial interpretation over the arctic semiring over the integers
| [4(x1)] |
= |
3 ·
x1 +
-∞
|
| [3(x1)] |
= |
0 ·
x1 +
-∞
|
| [2(x1)] |
= |
2 ·
x1 +
-∞
|
| [9(x1)] |
= |
1 ·
x1 +
-∞
|
| [7(x1)] |
= |
1 ·
x1 +
-∞
|
| [0(x1)] |
= |
0 ·
x1 +
-∞
|
| [6(x1)] |
= |
0 ·
x1 +
-∞
|
| [5(x1)] |
= |
0 ·
x1 +
-∞
|
the
rules
|
3(5(x0)) |
→ |
0(6(x0)) |
|
2(7(x0)) |
→ |
4(x0) |
|
0(7(x0)) |
→ |
3(9(x0)) |
|
9(6(x0)) |
→ |
9(x0) |
|
9(x0) |
→ |
7(6(x0)) |
|
6(6(x0)) |
→ |
3(x0) |
|
3(0(x0)) |
→ |
3(5(x0)) |
remain.
1.1.1.1.1.1 Rule Removal
Using the
linear polynomial interpretation over the arctic semiring over the integers
| [4(x1)] |
= |
8 ·
x1 +
-∞
|
| [3(x1)] |
= |
2 ·
x1 +
-∞
|
| [2(x1)] |
= |
2 ·
x1 +
-∞
|
| [9(x1)] |
= |
8 ·
x1 +
-∞
|
| [7(x1)] |
= |
6 ·
x1 +
-∞
|
| [0(x1)] |
= |
4 ·
x1 +
-∞
|
| [6(x1)] |
= |
2 ·
x1 +
-∞
|
| [5(x1)] |
= |
4 ·
x1 +
-∞
|
the
rules
|
3(5(x0)) |
→ |
0(6(x0)) |
|
2(7(x0)) |
→ |
4(x0) |
|
0(7(x0)) |
→ |
3(9(x0)) |
|
9(x0) |
→ |
7(6(x0)) |
|
3(0(x0)) |
→ |
3(5(x0)) |
remain.
1.1.1.1.1.1.1 Rule Removal
Using the
linear polynomial interpretation over (2 x 2)-matrices with strict dimension 1
over the arctic semiring over the integers
| [4(x1)] |
= |
·
x1 +
|
| [3(x1)] |
= |
·
x1 +
|
| [2(x1)] |
= |
·
x1 +
|
| [9(x1)] |
= |
·
x1 +
|
| [7(x1)] |
= |
·
x1 +
|
| [0(x1)] |
= |
·
x1 +
|
| [6(x1)] |
= |
·
x1 +
|
| [5(x1)] |
= |
·
x1 +
|
the
rules
|
0(7(x0)) |
→ |
3(9(x0)) |
|
9(x0) |
→ |
7(6(x0)) |
|
3(0(x0)) |
→ |
3(5(x0)) |
remain.
1.1.1.1.1.1.1.1 Rule Removal
Using the
linear polynomial interpretation over (2 x 2)-matrices with strict dimension 1
over the arctic semiring over the integers
| [3(x1)] |
= |
·
x1 +
|
| [9(x1)] |
= |
·
x1 +
|
| [7(x1)] |
= |
·
x1 +
|
| [0(x1)] |
= |
·
x1 +
|
| [6(x1)] |
= |
·
x1 +
|
| [5(x1)] |
= |
·
x1 +
|
the
rules
|
9(x0) |
→ |
7(6(x0)) |
|
3(0(x0)) |
→ |
3(5(x0)) |
remain.
1.1.1.1.1.1.1.1.1 Rule Removal
Using the
linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1
over the arctic semiring over the integers
| [3(x1)] |
= |
·
x1 +
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
|
| [9(x1)] |
= |
·
x1 +
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
|
| [7(x1)] |
= |
·
x1 +
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
|
| [0(x1)] |
= |
·
x1 +
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
|
| [6(x1)] |
= |
·
x1 +
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
|
| [5(x1)] |
= |
·
x1 +
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
|
the
rule
remains.
1.1.1.1.1.1.1.1.1.1 Rule Removal
Using the
linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1
over the arctic semiring over the integers
| [9(x1)] |
= |
·
x1 +
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
|
| [7(x1)] |
= |
·
x1 +
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
|
| [6(x1)] |
= |
·
x1 +
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
|
-∞
|
-∞
|
-∞
|
|
all rules could be removed.
1.1.1.1.1.1.1.1.1.1.1 R is empty
There are no rules in the TRS. Hence, it is terminating.