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)) |
|
M(V(c(x0))) |
→ |
V(Xc(x0)) |
|
M(V(d(x0))) |
→ |
V(Xd(x0)) |
|
Xa(a(x0)) |
→ |
a(Xa(x0)) |
|
Xa(b(x0)) |
→ |
b(Xa(x0)) |
|
Xa(c(x0)) |
→ |
c(Xa(x0)) |
|
Xa(d(x0)) |
→ |
d(Xa(x0)) |
|
Xb(a(x0)) |
→ |
a(Xb(x0)) |
|
Xb(b(x0)) |
→ |
b(Xb(x0)) |
|
Xb(c(x0)) |
→ |
c(Xb(x0)) |
|
Xb(d(x0)) |
→ |
d(Xb(x0)) |
|
Xc(a(x0)) |
→ |
a(Xc(x0)) |
|
Xc(b(x0)) |
→ |
b(Xc(x0)) |
|
Xc(c(x0)) |
→ |
c(Xc(x0)) |
|
Xc(d(x0)) |
→ |
d(Xc(x0)) |
|
Xd(a(x0)) |
→ |
a(Xd(x0)) |
|
Xd(b(x0)) |
→ |
b(Xd(x0)) |
|
Xd(c(x0)) |
→ |
c(Xd(x0)) |
|
Xd(d(x0)) |
→ |
d(Xd(x0)) |
|
Xa(E(x0)) |
→ |
a(E(x0)) |
|
Xb(E(x0)) |
→ |
b(E(x0)) |
|
Xc(E(x0)) |
→ |
c(E(x0)) |
|
Xd(E(x0)) |
→ |
d(E(x0)) |
|
W(V(x0)) |
→ |
R(L(x0)) |
|
L(a(x0)) |
→ |
Ya(L(x0)) |
|
L(b(x0)) |
→ |
Yb(L(x0)) |
|
L(c(x0)) |
→ |
Yc(L(x0)) |
|
L(d(x0)) |
→ |
Yd(L(x0)) |
|
L(a(a(a(x0)))) |
→ |
D(b(b(x0))) |
|
L(b(b(b(x0)))) |
→ |
D(c(d(x0))) |
|
L(c(x0)) |
→ |
D(a(a(x0))) |
|
L(d(x0)) |
→ |
D(c(x0)) |
|
Ya(D(x0)) |
→ |
D(a(x0)) |
|
Yb(D(x0)) |
→ |
D(b(x0)) |
|
Yc(D(x0)) |
→ |
D(c(x0)) |
|
Yd(D(x0)) |
→ |
D(d(x0)) |
|
R(D(x0)) |
→ |
B(x0) |
Proof
1 Rule Removal
Using the
linear polynomial interpretation over the arctic semiring over the integers
| [Yd(x1)] |
= |
4 ·
x1 +
-∞
|
| [a(x1)] |
= |
2 ·
x1 +
-∞
|
| [Ya(x1)] |
= |
2 ·
x1 +
-∞
|
| [c(x1)] |
= |
4 ·
x1 +
-∞
|
| [V(x1)] |
= |
0 ·
x1 +
-∞
|
| [W(x1)] |
= |
2 ·
x1 +
-∞
|
| [Yb(x1)] |
= |
3 ·
x1 +
-∞
|
| [D(x1)] |
= |
2 ·
x1 +
-∞
|
| [Yc(x1)] |
= |
4 ·
x1 +
-∞
|
| [Xa(x1)] |
= |
2 ·
x1 +
-∞
|
| [d(x1)] |
= |
4 ·
x1 +
-∞
|
| [B(x1)] |
= |
2 ·
x1 +
-∞
|
| [Xb(x1)] |
= |
3 ·
x1 +
-∞
|
| [R(x1)] |
= |
0 ·
x1 +
-∞
|
| [E(x1)] |
= |
0 ·
x1 +
-∞
|
| [Xd(x1)] |
= |
4 ·
x1 +
-∞
|
| [Xc(x1)] |
= |
4 ·
x1 +
-∞
|
| [L(x1)] |
= |
2 ·
x1 +
-∞
|
| [b(x1)] |
= |
3 ·
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)) |
|
M(V(c(x0))) |
→ |
V(Xc(x0)) |
|
M(V(d(x0))) |
→ |
V(Xd(x0)) |
|
Xa(a(x0)) |
→ |
a(Xa(x0)) |
|
Xa(b(x0)) |
→ |
b(Xa(x0)) |
|
Xa(c(x0)) |
→ |
c(Xa(x0)) |
|
Xa(d(x0)) |
→ |
d(Xa(x0)) |
|
Xb(a(x0)) |
→ |
a(Xb(x0)) |
|
Xb(b(x0)) |
→ |
b(Xb(x0)) |
|
Xb(c(x0)) |
→ |
c(Xb(x0)) |
|
Xb(d(x0)) |
→ |
d(Xb(x0)) |
|
Xc(a(x0)) |
→ |
a(Xc(x0)) |
|
Xc(b(x0)) |
→ |
b(Xc(x0)) |
|
Xc(c(x0)) |
→ |
c(Xc(x0)) |
|
Xc(d(x0)) |
→ |
d(Xc(x0)) |
|
Xd(a(x0)) |
→ |
a(Xd(x0)) |
|
Xd(b(x0)) |
→ |
b(Xd(x0)) |
|
Xd(c(x0)) |
→ |
c(Xd(x0)) |
|
Xd(d(x0)) |
→ |
d(Xd(x0)) |
|
Xa(E(x0)) |
→ |
a(E(x0)) |
|
Xb(E(x0)) |
→ |
b(E(x0)) |
|
Xc(E(x0)) |
→ |
c(E(x0)) |
|
Xd(E(x0)) |
→ |
d(E(x0)) |
|
W(V(x0)) |
→ |
R(L(x0)) |
|
L(a(x0)) |
→ |
Ya(L(x0)) |
|
L(b(x0)) |
→ |
Yb(L(x0)) |
|
L(c(x0)) |
→ |
Yc(L(x0)) |
|
L(d(x0)) |
→ |
Yd(L(x0)) |
|
L(a(a(a(x0)))) |
→ |
D(b(b(x0))) |
|
L(c(x0)) |
→ |
D(a(a(x0))) |
|
L(d(x0)) |
→ |
D(c(x0)) |
|
Ya(D(x0)) |
→ |
D(a(x0)) |
|
Yb(D(x0)) |
→ |
D(b(x0)) |
|
Yc(D(x0)) |
→ |
D(c(x0)) |
|
Yd(D(x0)) |
→ |
D(d(x0)) |
|
R(D(x0)) |
→ |
B(x0) |
remain.
1.1 Rule Removal
Using the
linear polynomial interpretation over the arctic semiring over the integers
| [Yd(x1)] |
= |
1 ·
x1 +
-∞
|
| [a(x1)] |
= |
0 ·
x1 +
-∞
|
| [Ya(x1)] |
= |
0 ·
x1 +
-∞
|
| [c(x1)] |
= |
0 ·
x1 +
-∞
|
| [V(x1)] |
= |
0 ·
x1 +
-∞
|
| [W(x1)] |
= |
0 ·
x1 +
-∞
|
| [Yb(x1)] |
= |
0 ·
x1 +
-∞
|
| [D(x1)] |
= |
0 ·
x1 +
-∞
|
| [Yc(x1)] |
= |
0 ·
x1 +
-∞
|
| [Xa(x1)] |
= |
0 ·
x1 +
-∞
|
| [d(x1)] |
= |
1 ·
x1 +
-∞
|
| [B(x1)] |
= |
0 ·
x1 +
-∞
|
| [Xb(x1)] |
= |
0 ·
x1 +
-∞
|
| [R(x1)] |
= |
0 ·
x1 +
-∞
|
| [E(x1)] |
= |
0 ·
x1 +
-∞
|
| [Xd(x1)] |
= |
1 ·
x1 +
-∞
|
| [Xc(x1)] |
= |
0 ·
x1 +
-∞
|
| [L(x1)] |
= |
0 ·
x1 +
-∞
|
| [b(x1)] |
= |
0 ·
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)) |
|
M(V(c(x0))) |
→ |
V(Xc(x0)) |
|
M(V(d(x0))) |
→ |
V(Xd(x0)) |
|
Xa(a(x0)) |
→ |
a(Xa(x0)) |
|
Xa(b(x0)) |
→ |
b(Xa(x0)) |
|
Xa(c(x0)) |
→ |
c(Xa(x0)) |
|
Xa(d(x0)) |
→ |
d(Xa(x0)) |
|
Xb(a(x0)) |
→ |
a(Xb(x0)) |
|
Xb(b(x0)) |
→ |
b(Xb(x0)) |
|
Xb(c(x0)) |
→ |
c(Xb(x0)) |
|
Xb(d(x0)) |
→ |
d(Xb(x0)) |
|
Xc(a(x0)) |
→ |
a(Xc(x0)) |
|
Xc(b(x0)) |
→ |
b(Xc(x0)) |
|
Xc(c(x0)) |
→ |
c(Xc(x0)) |
|
Xc(d(x0)) |
→ |
d(Xc(x0)) |
|
Xd(a(x0)) |
→ |
a(Xd(x0)) |
|
Xd(b(x0)) |
→ |
b(Xd(x0)) |
|
Xd(c(x0)) |
→ |
c(Xd(x0)) |
|
Xd(d(x0)) |
→ |
d(Xd(x0)) |
|
Xa(E(x0)) |
→ |
a(E(x0)) |
|
Xb(E(x0)) |
→ |
b(E(x0)) |
|
Xc(E(x0)) |
→ |
c(E(x0)) |
|
Xd(E(x0)) |
→ |
d(E(x0)) |
|
W(V(x0)) |
→ |
R(L(x0)) |
|
L(a(x0)) |
→ |
Ya(L(x0)) |
|
L(b(x0)) |
→ |
Yb(L(x0)) |
|
L(c(x0)) |
→ |
Yc(L(x0)) |
|
L(d(x0)) |
→ |
Yd(L(x0)) |
|
L(a(a(a(x0)))) |
→ |
D(b(b(x0))) |
|
L(c(x0)) |
→ |
D(a(a(x0))) |
|
Ya(D(x0)) |
→ |
D(a(x0)) |
|
Yb(D(x0)) |
→ |
D(b(x0)) |
|
Yc(D(x0)) |
→ |
D(c(x0)) |
|
Yd(D(x0)) |
→ |
D(d(x0)) |
|
R(D(x0)) |
→ |
B(x0) |
remain.
1.1.1 Rule Removal
Using the
linear polynomial interpretation over the arctic semiring over the integers
| [Yd(x1)] |
= |
1 ·
x1 +
-∞
|
| [a(x1)] |
= |
2 ·
x1 +
-∞
|
| [Ya(x1)] |
= |
2 ·
x1 +
-∞
|
| [c(x1)] |
= |
8 ·
x1 +
-∞
|
| [V(x1)] |
= |
3 ·
x1 +
-∞
|
| [W(x1)] |
= |
1 ·
x1 +
-∞
|
| [Yb(x1)] |
= |
2 ·
x1 +
-∞
|
| [D(x1)] |
= |
2 ·
x1 +
-∞
|
| [Yc(x1)] |
= |
8 ·
x1 +
-∞
|
| [Xa(x1)] |
= |
2 ·
x1 +
-∞
|
| [d(x1)] |
= |
1 ·
x1 +
-∞
|
| [B(x1)] |
= |
5 ·
x1 +
-∞
|
| [Xb(x1)] |
= |
2 ·
x1 +
-∞
|
| [R(x1)] |
= |
4 ·
x1 +
-∞
|
| [E(x1)] |
= |
0 ·
x1 +
-∞
|
| [Xd(x1)] |
= |
1 ·
x1 +
-∞
|
| [Xc(x1)] |
= |
8 ·
x1 +
-∞
|
| [L(x1)] |
= |
0 ·
x1 +
-∞
|
| [b(x1)] |
= |
2 ·
x1 +
-∞
|
| [M(x1)] |
= |
0 ·
x1 +
-∞
|
the
rules
|
M(x0) |
→ |
x0 |
|
M(V(a(x0))) |
→ |
V(Xa(x0)) |
|
M(V(b(x0))) |
→ |
V(Xb(x0)) |
|
M(V(c(x0))) |
→ |
V(Xc(x0)) |
|
M(V(d(x0))) |
→ |
V(Xd(x0)) |
|
Xa(a(x0)) |
→ |
a(Xa(x0)) |
|
Xa(b(x0)) |
→ |
b(Xa(x0)) |
|
Xa(c(x0)) |
→ |
c(Xa(x0)) |
|
Xa(d(x0)) |
→ |
d(Xa(x0)) |
|
Xb(a(x0)) |
→ |
a(Xb(x0)) |
|
Xb(b(x0)) |
→ |
b(Xb(x0)) |
|
Xb(c(x0)) |
→ |
c(Xb(x0)) |
|
Xb(d(x0)) |
→ |
d(Xb(x0)) |
|
Xc(a(x0)) |
→ |
a(Xc(x0)) |
|
Xc(b(x0)) |
→ |
b(Xc(x0)) |
|
Xc(c(x0)) |
→ |
c(Xc(x0)) |
|
Xc(d(x0)) |
→ |
d(Xc(x0)) |
|
Xd(a(x0)) |
→ |
a(Xd(x0)) |
|
Xd(b(x0)) |
→ |
b(Xd(x0)) |
|
Xd(c(x0)) |
→ |
c(Xd(x0)) |
|
Xd(d(x0)) |
→ |
d(Xd(x0)) |
|
Xa(E(x0)) |
→ |
a(E(x0)) |
|
Xb(E(x0)) |
→ |
b(E(x0)) |
|
Xc(E(x0)) |
→ |
c(E(x0)) |
|
Xd(E(x0)) |
→ |
d(E(x0)) |
|
W(V(x0)) |
→ |
R(L(x0)) |
|
L(a(x0)) |
→ |
Ya(L(x0)) |
|
L(b(x0)) |
→ |
Yb(L(x0)) |
|
L(c(x0)) |
→ |
Yc(L(x0)) |
|
L(d(x0)) |
→ |
Yd(L(x0)) |
|
L(a(a(a(x0)))) |
→ |
D(b(b(x0))) |
|
Ya(D(x0)) |
→ |
D(a(x0)) |
|
Yb(D(x0)) |
→ |
D(b(x0)) |
|
Yc(D(x0)) |
→ |
D(c(x0)) |
|
Yd(D(x0)) |
→ |
D(d(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(Yd) |
= |
2 |
|
weight(Yd) |
= |
1 |
|
|
|
| prec(Yc) |
= |
2 |
|
weight(Yc) |
= |
1 |
|
|
|
| prec(Yb) |
= |
2 |
|
weight(Yb) |
= |
1 |
|
|
|
| prec(Ya) |
= |
2 |
|
weight(Ya) |
= |
1 |
|
|
|
| prec(R) |
= |
0 |
|
weight(R) |
= |
1 |
|
|
|
| prec(L) |
= |
3 |
|
weight(L) |
= |
1 |
|
|
|
| prec(E) |
= |
0 |
|
weight(E) |
= |
1 |
|
|
|
| prec(Xd) |
= |
1 |
|
weight(Xd) |
= |
1 |
|
|
|
| prec(d) |
= |
0 |
|
weight(d) |
= |
1 |
|
|
|
| prec(Xc) |
= |
5 |
|
weight(Xc) |
= |
1 |
|
|
|
| prec(c) |
= |
0 |
|
weight(c) |
= |
1 |
|
|
|
| prec(Xb) |
= |
6 |
|
weight(Xb) |
= |
1 |
|
|
|
| prec(b) |
= |
0 |
|
weight(b) |
= |
1 |
|
|
|
| prec(Xa) |
= |
6 |
|
weight(Xa) |
= |
1 |
|
|
|
| prec(a) |
= |
0 |
|
weight(a) |
= |
1 |
|
|
|
| prec(W) |
= |
1 |
|
weight(W) |
= |
1 |
|
|
|
| prec(M) |
= |
0 |
|
weight(M) |
= |
1 |
|
|
|
| prec(V) |
= |
7 |
|
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.