YES
Termination Proof
Termination Proof
by ttt2 (version ttt2 1.15)
Input
The rewrite relation of the following TRS is considered.
|
q0(0(x0)) |
→ |
0'(q1(x0)) |
|
q1(0(x0)) |
→ |
0(q1(x0)) |
|
q1(1'(x0)) |
→ |
1'(q1(x0)) |
|
0(q1(1(x0))) |
→ |
q2(0(1'(x0))) |
|
0'(q1(1(x0))) |
→ |
q2(0'(1'(x0))) |
|
1'(q1(1(x0))) |
→ |
q2(1'(1'(x0))) |
|
0(q2(0(x0))) |
→ |
q2(0(0(x0))) |
|
0'(q2(0(x0))) |
→ |
q2(0'(0(x0))) |
|
1'(q2(0(x0))) |
→ |
q2(1'(0(x0))) |
|
0(q2(1'(x0))) |
→ |
q2(0(1'(x0))) |
|
0'(q2(1'(x0))) |
→ |
q2(0'(1'(x0))) |
|
1'(q2(1'(x0))) |
→ |
q2(1'(1'(x0))) |
|
q2(0'(x0)) |
→ |
0'(q0(x0)) |
|
q0(1'(x0)) |
→ |
1'(q3(x0)) |
|
q3(1'(x0)) |
→ |
1'(q3(x0)) |
|
q3(b(x0)) |
→ |
b(q4(x0)) |
Proof
1 Rule Removal
Using the
linear polynomial interpretation over the arctic semiring over the integers
| [1'(x1)] |
= |
2 ·
x1 +
-∞
|
| [b(x1)] |
= |
2 ·
x1 +
-∞
|
| [q0(x1)] |
= |
6 ·
x1 +
-∞
|
| [0'(x1)] |
= |
9 ·
x1 +
-∞
|
| [1(x1)] |
= |
4 ·
x1 +
-∞
|
| [0(x1)] |
= |
7 ·
x1 +
-∞
|
| [q3(x1)] |
= |
6 ·
x1 +
-∞
|
| [q4(x1)] |
= |
3 ·
x1 +
-∞
|
| [q2(x1)] |
= |
6 ·
x1 +
-∞
|
| [q1(x1)] |
= |
4 ·
x1 +
-∞
|
the
rules
|
q0(0(x0)) |
→ |
0'(q1(x0)) |
|
q1(0(x0)) |
→ |
0(q1(x0)) |
|
q1(1'(x0)) |
→ |
1'(q1(x0)) |
|
0(q1(1(x0))) |
→ |
q2(0(1'(x0))) |
|
0'(q1(1(x0))) |
→ |
q2(0'(1'(x0))) |
|
1'(q1(1(x0))) |
→ |
q2(1'(1'(x0))) |
|
0(q2(0(x0))) |
→ |
q2(0(0(x0))) |
|
0'(q2(0(x0))) |
→ |
q2(0'(0(x0))) |
|
1'(q2(0(x0))) |
→ |
q2(1'(0(x0))) |
|
0(q2(1'(x0))) |
→ |
q2(0(1'(x0))) |
|
0'(q2(1'(x0))) |
→ |
q2(0'(1'(x0))) |
|
1'(q2(1'(x0))) |
→ |
q2(1'(1'(x0))) |
|
q2(0'(x0)) |
→ |
0'(q0(x0)) |
|
q0(1'(x0)) |
→ |
1'(q3(x0)) |
|
q3(1'(x0)) |
→ |
1'(q3(x0)) |
remain.
1.1 Rule Removal
Using the
linear polynomial interpretation over the arctic semiring over the integers
| [1'(x1)] |
= |
1 ·
x1 +
-∞
|
| [q0(x1)] |
= |
0 ·
x1 +
-∞
|
| [0'(x1)] |
= |
0 ·
x1 +
-∞
|
| [1(x1)] |
= |
7 ·
x1 +
-∞
|
| [0(x1)] |
= |
0 ·
x1 +
-∞
|
| [q3(x1)] |
= |
0 ·
x1 +
-∞
|
| [q2(x1)] |
= |
6 ·
x1 +
-∞
|
| [q1(x1)] |
= |
0 ·
x1 +
-∞
|
the
rules
|
q0(0(x0)) |
→ |
0'(q1(x0)) |
|
q1(0(x0)) |
→ |
0(q1(x0)) |
|
q1(1'(x0)) |
→ |
1'(q1(x0)) |
|
0(q1(1(x0))) |
→ |
q2(0(1'(x0))) |
|
0'(q1(1(x0))) |
→ |
q2(0'(1'(x0))) |
|
1'(q1(1(x0))) |
→ |
q2(1'(1'(x0))) |
|
0(q2(0(x0))) |
→ |
q2(0(0(x0))) |
|
0'(q2(0(x0))) |
→ |
q2(0'(0(x0))) |
|
1'(q2(0(x0))) |
→ |
q2(1'(0(x0))) |
|
0(q2(1'(x0))) |
→ |
q2(0(1'(x0))) |
|
0'(q2(1'(x0))) |
→ |
q2(0'(1'(x0))) |
|
1'(q2(1'(x0))) |
→ |
q2(1'(1'(x0))) |
|
q0(1'(x0)) |
→ |
1'(q3(x0)) |
|
q3(1'(x0)) |
→ |
1'(q3(x0)) |
remain.
1.1.1 Rule Removal
Using the
Knuth Bendix order with w0 = 1 and the following precedence and weight function
| prec(q3) |
= |
4 |
|
weight(q3) |
= |
1 |
|
|
|
| prec(q2) |
= |
0 |
|
weight(q2) |
= |
1 |
|
|
|
| prec(1) |
= |
0 |
|
weight(1) |
= |
1 |
|
|
|
| prec(1') |
= |
1 |
|
weight(1') |
= |
1 |
|
|
|
| prec(0') |
= |
2 |
|
weight(0') |
= |
1 |
|
|
|
| prec(q1) |
= |
2 |
|
weight(q1) |
= |
1 |
|
|
|
| prec(q0) |
= |
7 |
|
weight(q0) |
= |
1 |
|
|
|
| prec(0) |
= |
1 |
|
weight(0) |
= |
1 |
|
|
|
all rules could be removed.
1.1.1.1 R is empty
There are no rules in the TRS. Hence, it is terminating.