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(x0))
L(c(x0)) → D(d(d(x0)))
L(d(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)

Proof

1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers
[Yd(x1)] = 6 · x1 + -∞
[a(x1)] = 3 · x1 + -∞
[Ya(x1)] = 3 · x1 + -∞
[c(x1)] = 12 · x1 + -∞
[V(x1)] = 0 · x1 + -∞
[W(x1)] = 0 · x1 + -∞
[Yb(x1)] = 4 · x1 + -∞
[D(x1)] = 0 · x1 + -∞
[Yc(x1)] = 12 · x1 + -∞
[Xa(x1)] = 3 · x1 + -∞
[d(x1)] = 6 · x1 + -∞
[B(x1)] = 0 · x1 + -∞
[Xb(x1)] = 4 · x1 + -∞
[R(x1)] = 0 · x1 + -∞
[E(x1)] = 0 · x1 + -∞
[Xd(x1)] = 6 · x1 + -∞
[Xc(x1)] = 12 · x1 + -∞
[L(x1)] = 0 · x1 + -∞
[b(x1)] = 4 · 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(b(b(b(x0)))) → D(c(x0))
L(c(x0)) → D(d(d(x0)))
L(d(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 Rule Removal

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