YES
Termination Proof
Termination Proof
by ttt2 (version ttt2 1.15)
Input
The rewrite relation of the following TRS is considered.
|
B(x0) |
→ |
W(M(M(V(x0)))) |
|
M(x0) |
→ |
x0 |
|
M(V(a(x0))) |
→ |
V(Xa(x0)) |
|
M(V(b(x0))) |
→ |
V(Xb(x0)) |
|
Xa(a(x0)) |
→ |
a(Xa(x0)) |
|
Xa(b(x0)) |
→ |
b(Xa(x0)) |
|
Xb(a(x0)) |
→ |
a(Xb(x0)) |
|
Xb(b(x0)) |
→ |
b(Xb(x0)) |
|
Xa(E(x0)) |
→ |
a(E(x0)) |
|
Xb(E(x0)) |
→ |
b(E(x0)) |
|
W(V(x0)) |
→ |
R(L(x0)) |
|
L(a(x0)) |
→ |
Ya(L(x0)) |
|
L(b(x0)) |
→ |
Yb(L(x0)) |
|
L(a(x0)) |
→ |
D(b(b(x0))) |
|
L(b(b(b(x0)))) |
→ |
D(a(x0)) |
|
Ya(D(x0)) |
→ |
D(a(x0)) |
|
Yb(D(x0)) |
→ |
D(b(x0)) |
|
R(D(x0)) |
→ |
B(x0) |
Proof
1 Rule Removal
Using the
linear polynomial interpretation over the arctic semiring over the integers
| [a(x1)] |
= |
2 ·
x1 +
-∞
|
| [E(x1)] |
= |
0 ·
x1 +
-∞
|
| [V(x1)] |
= |
0 ·
x1 +
-∞
|
| [W(x1)] |
= |
0 ·
x1 +
-∞
|
| [Xa(x1)] |
= |
2 ·
x1 +
-∞
|
| [R(x1)] |
= |
0 ·
x1 +
-∞
|
| [B(x1)] |
= |
0 ·
x1 +
-∞
|
| [Xb(x1)] |
= |
1 ·
x1 +
-∞
|
| [Yb(x1)] |
= |
1 ·
x1 +
-∞
|
| [Ya(x1)] |
= |
2 ·
x1 +
-∞
|
| [L(x1)] |
= |
0 ·
x1 +
-∞
|
| [D(x1)] |
= |
0 ·
x1 +
-∞
|
| [b(x1)] |
= |
1 ·
x1 +
-∞
|
| [M(x1)] |
= |
0 ·
x1 +
-∞
|
the
rules
|
B(x0) |
→ |
W(M(M(V(x0)))) |
|
M(x0) |
→ |
x0 |
|
M(V(a(x0))) |
→ |
V(Xa(x0)) |
|
M(V(b(x0))) |
→ |
V(Xb(x0)) |
|
Xa(a(x0)) |
→ |
a(Xa(x0)) |
|
Xa(b(x0)) |
→ |
b(Xa(x0)) |
|
Xb(a(x0)) |
→ |
a(Xb(x0)) |
|
Xb(b(x0)) |
→ |
b(Xb(x0)) |
|
Xa(E(x0)) |
→ |
a(E(x0)) |
|
Xb(E(x0)) |
→ |
b(E(x0)) |
|
W(V(x0)) |
→ |
R(L(x0)) |
|
L(a(x0)) |
→ |
Ya(L(x0)) |
|
L(b(x0)) |
→ |
Yb(L(x0)) |
|
L(a(x0)) |
→ |
D(b(b(x0))) |
|
Ya(D(x0)) |
→ |
D(a(x0)) |
|
Yb(D(x0)) |
→ |
D(b(x0)) |
|
R(D(x0)) |
→ |
B(x0) |
remain.
1.1 Rule Removal
Using the
linear polynomial interpretation over the arctic semiring over the integers
| [a(x1)] |
= |
8 ·
x1 +
-∞
|
| [E(x1)] |
= |
4 ·
x1 +
-∞
|
| [V(x1)] |
= |
0 ·
x1 +
-∞
|
| [W(x1)] |
= |
2 ·
x1 +
-∞
|
| [Xa(x1)] |
= |
8 ·
x1 +
-∞
|
| [R(x1)] |
= |
0 ·
x1 +
-∞
|
| [B(x1)] |
= |
8 ·
x1 +
-∞
|
| [Xb(x1)] |
= |
1 ·
x1 +
-∞
|
| [Yb(x1)] |
= |
0 ·
x1 +
-∞
|
| [Ya(x1)] |
= |
8 ·
x1 +
-∞
|
| [L(x1)] |
= |
0 ·
x1 +
-∞
|
| [D(x1)] |
= |
8 ·
x1 +
-∞
|
| [b(x1)] |
= |
0 ·
x1 +
-∞
|
| [M(x1)] |
= |
1 ·
x1 +
-∞
|
the
rules
|
M(V(b(x0))) |
→ |
V(Xb(x0)) |
|
Xa(a(x0)) |
→ |
a(Xa(x0)) |
|
Xa(b(x0)) |
→ |
b(Xa(x0)) |
|
Xb(a(x0)) |
→ |
a(Xb(x0)) |
|
Xb(b(x0)) |
→ |
b(Xb(x0)) |
|
Xa(E(x0)) |
→ |
a(E(x0)) |
|
L(a(x0)) |
→ |
Ya(L(x0)) |
|
L(b(x0)) |
→ |
Yb(L(x0)) |
|
L(a(x0)) |
→ |
D(b(b(x0))) |
|
Ya(D(x0)) |
→ |
D(a(x0)) |
|
Yb(D(x0)) |
→ |
D(b(x0)) |
|
R(D(x0)) |
→ |
B(x0) |
remain.
1.1.1 Rule Removal
Using the
linear polynomial interpretation over the arctic semiring over the integers
| [a(x1)] |
= |
15 ·
x1 +
-∞
|
| [E(x1)] |
= |
8 ·
x1 +
-∞
|
| [V(x1)] |
= |
12 ·
x1 +
-∞
|
| [Xa(x1)] |
= |
15 ·
x1 +
-∞
|
| [R(x1)] |
= |
11 ·
x1 +
-∞
|
| [B(x1)] |
= |
0 ·
x1 +
-∞
|
| [Xb(x1)] |
= |
8 ·
x1 +
-∞
|
| [Yb(x1)] |
= |
6 ·
x1 +
-∞
|
| [Ya(x1)] |
= |
15 ·
x1 +
-∞
|
| [L(x1)] |
= |
12 ·
x1 +
-∞
|
| [D(x1)] |
= |
4 ·
x1 +
-∞
|
| [b(x1)] |
= |
6 ·
x1 +
-∞
|
| [M(x1)] |
= |
2 ·
x1 +
-∞
|
the
rules
|
M(V(b(x0))) |
→ |
V(Xb(x0)) |
|
Xa(a(x0)) |
→ |
a(Xa(x0)) |
|
Xa(b(x0)) |
→ |
b(Xa(x0)) |
|
Xb(a(x0)) |
→ |
a(Xb(x0)) |
|
Xb(b(x0)) |
→ |
b(Xb(x0)) |
|
Xa(E(x0)) |
→ |
a(E(x0)) |
|
L(a(x0)) |
→ |
Ya(L(x0)) |
|
L(b(x0)) |
→ |
Yb(L(x0)) |
|
Ya(D(x0)) |
→ |
D(a(x0)) |
|
Yb(D(x0)) |
→ |
D(b(x0)) |
remain.
1.1.1.1 Rule Removal
Using the
Knuth Bendix order with w0 = 1 and the following precedence and weight function
| prec(D) |
= |
0 |
|
weight(D) |
= |
1 |
|
|
|
| prec(Yb) |
= |
2 |
|
weight(Yb) |
= |
1 |
|
|
|
| prec(Ya) |
= |
2 |
|
weight(Ya) |
= |
1 |
|
|
|
| prec(L) |
= |
3 |
|
weight(L) |
= |
1 |
|
|
|
| prec(E) |
= |
0 |
|
weight(E) |
= |
1 |
|
|
|
| prec(Xb) |
= |
1 |
|
weight(Xb) |
= |
1 |
|
|
|
| prec(b) |
= |
0 |
|
weight(b) |
= |
1 |
|
|
|
| prec(Xa) |
= |
1 |
|
weight(Xa) |
= |
1 |
|
|
|
| prec(a) |
= |
0 |
|
weight(a) |
= |
1 |
|
|
|
| prec(M) |
= |
7 |
|
weight(M) |
= |
0 |
|
|
|
| prec(V) |
= |
0 |
|
weight(V) |
= |
1 |
|
|
|
all rules could be removed.
1.1.1.1.1 R is empty
There are no rules in the TRS. Hence, it is terminating.