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(M(V(x0)))))
M(x0) → x0
M(V(c(x0))) → V(Xc(x0))
M(V(a(x0))) → V(Xa(x0))
M(V(d(x0))) → V(Xd(x0))
M(V(b(x0))) → V(Xb(x0))
Xc(c(x0)) → c(Xc(x0))
Xc(a(x0)) → a(Xc(x0))
Xc(d(x0)) → d(Xc(x0))
Xc(b(x0)) → b(Xc(x0))
Xa(c(x0)) → c(Xa(x0))
Xa(a(x0)) → a(Xa(x0))
Xa(d(x0)) → d(Xa(x0))
Xa(b(x0)) → b(Xa(x0))
Xd(c(x0)) → c(Xd(x0))
Xd(a(x0)) → a(Xd(x0))
Xd(d(x0)) → d(Xd(x0))
Xd(b(x0)) → b(Xd(x0))
Xb(c(x0)) → c(Xb(x0))
Xb(a(x0)) → a(Xb(x0))
Xb(d(x0)) → d(Xb(x0))
Xb(b(x0)) → b(Xb(x0))
Xc(E(x0)) → c(E(x0))
Xa(E(x0)) → a(E(x0))
Xd(E(x0)) → d(E(x0))
Xb(E(x0)) → b(E(x0))
W(V(x0)) → R(L(x0))
L(c(x0)) → Yc(L(x0))
L(a(x0)) → Ya(L(x0))
L(d(x0)) → Yd(L(x0))
L(b(x0)) → Yb(L(x0))
L(c(c(c(a(x0))))) → D(d(d(x0)))
L(d(b(x0))) → D(c(c(x0)))
L(c(x0)) → D(a(a(a(a(x0)))))
L(d(x0)) → D(b(b(b(b(x0)))))
L(b(d(x0))) → D(c(c(x0)))
L(a(c(c(c(x0))))) → D(d(d(x0)))
Yc(D(x0)) → D(c(x0))
Ya(D(x0)) → D(a(x0))
Yd(D(x0)) → D(d(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
[Yb(x1)] = 3 · x1 + -∞
[c(x1)] = 8 · x1 + -∞
[Yc(x1)] = 8 · x1 + -∞
[d(x1)] = 13 · x1 + -∞
[V(x1)] = 0 · x1 + -∞
[W(x1)] = 8 · x1 + -∞
[Ya(x1)] = 2 · x1 + -∞
[D(x1)] = 0 · x1 + -∞
[Yd(x1)] = 13 · x1 + -∞
[Xc(x1)] = 8 · x1 + -∞
[b(x1)] = 3 · x1 + -∞
[B(x1)] = 8 · x1 + -∞
[Xa(x1)] = 2 · x1 + -∞
[R(x1)] = 8 · x1 + -∞
[E(x1)] = 0 · x1 + -∞
[Xb(x1)] = 3 · x1 + -∞
[Xd(x1)] = 13 · x1 + -∞
[L(x1)] = 0 · x1 + -∞
[a(x1)] = 2 · x1 + -∞
[M(x1)] = 0 · x1 + -∞
the rules
B(x0) → W(M(M(M(V(x0)))))
M(x0) → x0
M(V(c(x0))) → V(Xc(x0))
M(V(a(x0))) → V(Xa(x0))
M(V(d(x0))) → V(Xd(x0))
M(V(b(x0))) → V(Xb(x0))
Xc(c(x0)) → c(Xc(x0))
Xc(a(x0)) → a(Xc(x0))
Xc(d(x0)) → d(Xc(x0))
Xc(b(x0)) → b(Xc(x0))
Xa(c(x0)) → c(Xa(x0))
Xa(a(x0)) → a(Xa(x0))
Xa(d(x0)) → d(Xa(x0))
Xa(b(x0)) → b(Xa(x0))
Xd(c(x0)) → c(Xd(x0))
Xd(a(x0)) → a(Xd(x0))
Xd(d(x0)) → d(Xd(x0))
Xd(b(x0)) → b(Xd(x0))
Xb(c(x0)) → c(Xb(x0))
Xb(a(x0)) → a(Xb(x0))
Xb(d(x0)) → d(Xb(x0))
Xb(b(x0)) → b(Xb(x0))
Xc(E(x0)) → c(E(x0))
Xa(E(x0)) → a(E(x0))
Xd(E(x0)) → d(E(x0))
Xb(E(x0)) → b(E(x0))
W(V(x0)) → R(L(x0))
L(c(x0)) → Yc(L(x0))
L(a(x0)) → Ya(L(x0))
L(d(x0)) → Yd(L(x0))
L(b(x0)) → Yb(L(x0))
L(c(c(c(a(x0))))) → D(d(d(x0)))
L(d(b(x0))) → D(c(c(x0)))
L(c(x0)) → D(a(a(a(a(x0)))))
L(b(d(x0))) → D(c(c(x0)))
L(a(c(c(c(x0))))) → D(d(d(x0)))
Yc(D(x0)) → D(c(x0))
Ya(D(x0)) → D(a(x0))
Yd(D(x0)) → D(d(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
[Yb(x1)] = 4 · x1 + -∞
[c(x1)] = 6 · x1 + -∞
[Yc(x1)] = 6 · x1 + -∞
[d(x1)] = 8 · x1 + -∞
[V(x1)] = 0 · x1 + -∞
[W(x1)] = 0 · x1 + -∞
[Ya(x1)] = 1 · x1 + -∞
[D(x1)] = 0 · x1 + -∞
[Yd(x1)] = 8 · x1 + -∞
[Xc(x1)] = 6 · x1 + -∞
[b(x1)] = 4 · x1 + -∞
[B(x1)] = 0 · x1 + -∞
[Xa(x1)] = 1 · x1 + -∞
[R(x1)] = 0 · x1 + -∞
[E(x1)] = 0 · x1 + -∞
[Xb(x1)] = 4 · x1 + -∞
[Xd(x1)] = 8 · x1 + -∞
[L(x1)] = 0 · x1 + -∞
[a(x1)] = 1 · x1 + -∞
[M(x1)] = 0 · x1 + -∞
the rules
B(x0) → W(M(M(M(V(x0)))))
M(x0) → x0
M(V(c(x0))) → V(Xc(x0))
M(V(a(x0))) → V(Xa(x0))
M(V(d(x0))) → V(Xd(x0))
M(V(b(x0))) → V(Xb(x0))
Xc(c(x0)) → c(Xc(x0))
Xc(a(x0)) → a(Xc(x0))
Xc(d(x0)) → d(Xc(x0))
Xc(b(x0)) → b(Xc(x0))
Xa(c(x0)) → c(Xa(x0))
Xa(a(x0)) → a(Xa(x0))
Xa(d(x0)) → d(Xa(x0))
Xa(b(x0)) → b(Xa(x0))
Xd(c(x0)) → c(Xd(x0))
Xd(a(x0)) → a(Xd(x0))
Xd(d(x0)) → d(Xd(x0))
Xd(b(x0)) → b(Xd(x0))
Xb(c(x0)) → c(Xb(x0))
Xb(a(x0)) → a(Xb(x0))
Xb(d(x0)) → d(Xb(x0))
Xb(b(x0)) → b(Xb(x0))
Xc(E(x0)) → c(E(x0))
Xa(E(x0)) → a(E(x0))
Xd(E(x0)) → d(E(x0))
Xb(E(x0)) → b(E(x0))
W(V(x0)) → R(L(x0))
L(c(x0)) → Yc(L(x0))
L(a(x0)) → Ya(L(x0))
L(d(x0)) → Yd(L(x0))
L(b(x0)) → Yb(L(x0))
L(d(b(x0))) → D(c(c(x0)))
L(b(d(x0))) → D(c(c(x0)))
Yc(D(x0)) → D(c(x0))
Ya(D(x0)) → D(a(x0))
Yd(D(x0)) → D(d(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
[Yb(x1)] = 0 · x1 + -∞
[c(x1)] = 0 · x1 + -∞
[Yc(x1)] = 0 · x1 + -∞
[d(x1)] = 9 · x1 + -∞
[V(x1)] = 1 · x1 + -∞
[W(x1)] = 7 · x1 + -∞
[Ya(x1)] = 0 · x1 + -∞
[D(x1)] = 8 · x1 + -∞
[Yd(x1)] = 9 · x1 + -∞
[Xc(x1)] = 0 · x1 + -∞
[b(x1)] = 0 · x1 + -∞
[B(x1)] = 8 · x1 + -∞
[Xa(x1)] = 0 · x1 + -∞
[R(x1)] = 8 · x1 + -∞
[E(x1)] = 0 · x1 + -∞
[Xb(x1)] = 0 · x1 + -∞
[Xd(x1)] = 9 · x1 + -∞
[L(x1)] = 0 · x1 + -∞
[a(x1)] = 0 · x1 + -∞
[M(x1)] = 0 · x1 + -∞
the rules
B(x0) → W(M(M(M(V(x0)))))
M(x0) → x0
M(V(c(x0))) → V(Xc(x0))
M(V(a(x0))) → V(Xa(x0))
M(V(d(x0))) → V(Xd(x0))
M(V(b(x0))) → V(Xb(x0))
Xc(c(x0)) → c(Xc(x0))
Xc(a(x0)) → a(Xc(x0))
Xc(d(x0)) → d(Xc(x0))
Xc(b(x0)) → b(Xc(x0))
Xa(c(x0)) → c(Xa(x0))
Xa(a(x0)) → a(Xa(x0))
Xa(d(x0)) → d(Xa(x0))
Xa(b(x0)) → b(Xa(x0))
Xd(c(x0)) → c(Xd(x0))
Xd(a(x0)) → a(Xd(x0))
Xd(d(x0)) → d(Xd(x0))
Xd(b(x0)) → b(Xd(x0))
Xb(c(x0)) → c(Xb(x0))
Xb(a(x0)) → a(Xb(x0))
Xb(d(x0)) → d(Xb(x0))
Xb(b(x0)) → b(Xb(x0))
Xc(E(x0)) → c(E(x0))
Xa(E(x0)) → a(E(x0))
Xd(E(x0)) → d(E(x0))
Xb(E(x0)) → b(E(x0))
W(V(x0)) → R(L(x0))
L(c(x0)) → Yc(L(x0))
L(a(x0)) → Ya(L(x0))
L(d(x0)) → Yd(L(x0))
L(b(x0)) → Yb(L(x0))
Yc(D(x0)) → D(c(x0))
Ya(D(x0)) → D(a(x0))
Yd(D(x0)) → D(d(x0))
Yb(D(x0)) → D(b(x0))
remain.

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers
[Yb(x1)] = 0 · x1 + -∞
[c(x1)] = 0 · x1 + -∞
[Yc(x1)] = 0 · x1 + -∞
[d(x1)] = 8 · x1 + -∞
[V(x1)] = 2 · x1 + -∞
[W(x1)] = 0 · x1 + -∞
[Ya(x1)] = 8 · x1 + -∞
[D(x1)] = 0 · x1 + -∞
[Yd(x1)] = 8 · x1 + -∞
[Xc(x1)] = 3 · x1 + -∞
[b(x1)] = 0 · x1 + -∞
[B(x1)] = 11 · x1 + -∞
[Xa(x1)] = 8 · x1 + -∞
[R(x1)] = 2 · x1 + -∞
[E(x1)] = 0 · x1 + -∞
[Xb(x1)] = 2 · x1 + -∞
[Xd(x1)] = 8 · x1 + -∞
[L(x1)] = 0 · x1 + -∞
[a(x1)] = 8 · x1 + -∞
[M(x1)] = 3 · x1 + -∞
the rules
B(x0) → W(M(M(M(V(x0)))))
M(V(c(x0))) → V(Xc(x0))
Xc(c(x0)) → c(Xc(x0))
Xc(a(x0)) → a(Xc(x0))
Xc(d(x0)) → d(Xc(x0))
Xc(b(x0)) → b(Xc(x0))
Xa(c(x0)) → c(Xa(x0))
Xa(a(x0)) → a(Xa(x0))
Xa(d(x0)) → d(Xa(x0))
Xa(b(x0)) → b(Xa(x0))
Xd(c(x0)) → c(Xd(x0))
Xd(a(x0)) → a(Xd(x0))
Xd(d(x0)) → d(Xd(x0))
Xd(b(x0)) → b(Xd(x0))
Xb(c(x0)) → c(Xb(x0))
Xb(a(x0)) → a(Xb(x0))
Xb(d(x0)) → d(Xb(x0))
Xb(b(x0)) → b(Xb(x0))
Xa(E(x0)) → a(E(x0))
Xd(E(x0)) → d(E(x0))
W(V(x0)) → R(L(x0))
L(c(x0)) → Yc(L(x0))
L(a(x0)) → Ya(L(x0))
L(d(x0)) → Yd(L(x0))
L(b(x0)) → Yb(L(x0))
Yc(D(x0)) → D(c(x0))
Ya(D(x0)) → D(a(x0))
Yd(D(x0)) → D(d(x0))
Yb(D(x0)) → D(b(x0))
remain.

1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers
[Yb(x1)] = 0 · x1 + -∞
[c(x1)] = 2 · x1 + -∞
[Yc(x1)] = 2 · x1 + -∞
[d(x1)] = 1 · x1 + -∞
[V(x1)] = 0 · x1 + -∞
[W(x1)] = 0 · x1 + -∞
[Ya(x1)] = 4 · x1 + -∞
[D(x1)] = 0 · x1 + -∞
[Yd(x1)] = 1 · x1 + -∞
[Xc(x1)] = 0 · x1 + -∞
[b(x1)] = 0 · x1 + -∞
[B(x1)] = 0 · x1 + -∞
[Xa(x1)] = 10 · x1 + -∞
[R(x1)] = 0 · x1 + -∞
[E(x1)] = 13 · x1 + -∞
[Xb(x1)] = 1 · x1 + -∞
[Xd(x1)] = 1 · x1 + -∞
[L(x1)] = 0 · x1 + -∞
[a(x1)] = 4 · x1 + -∞
[M(x1)] = 0 · x1 + -∞
the rules
B(x0) → W(M(M(M(V(x0)))))
Xc(c(x0)) → c(Xc(x0))
Xc(a(x0)) → a(Xc(x0))
Xc(d(x0)) → d(Xc(x0))
Xc(b(x0)) → b(Xc(x0))
Xa(c(x0)) → c(Xa(x0))
Xa(a(x0)) → a(Xa(x0))
Xa(d(x0)) → d(Xa(x0))
Xa(b(x0)) → b(Xa(x0))
Xd(c(x0)) → c(Xd(x0))
Xd(a(x0)) → a(Xd(x0))
Xd(d(x0)) → d(Xd(x0))
Xd(b(x0)) → b(Xd(x0))
Xb(c(x0)) → c(Xb(x0))
Xb(a(x0)) → a(Xb(x0))
Xb(d(x0)) → d(Xb(x0))
Xb(b(x0)) → b(Xb(x0))
Xd(E(x0)) → d(E(x0))
W(V(x0)) → R(L(x0))
L(c(x0)) → Yc(L(x0))
L(a(x0)) → Ya(L(x0))
L(d(x0)) → Yd(L(x0))
L(b(x0)) → Yb(L(x0))
Yc(D(x0)) → D(c(x0))
Ya(D(x0)) → D(a(x0))
Yd(D(x0)) → D(d(x0))
Yb(D(x0)) → D(b(x0))
remain.

1.1.1.1.1.1 Bounds

The given TRS is match-bounded by 0. This is shown by the following automaton.