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(x0))) → D(b(c(x0)))
L(b(b(x0))) → D(c(d(x0)))
L(c(c(x0))) → D(d(d(d(x0))))
L(d(d(d(x0)))) → D(a(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)] = 8 · x1 + -∞
[a(x1)] = 12 · x1 + -∞
[Ya(x1)] = 12 · x1 + -∞
[c(x1)] = 12 · x1 + -∞
[V(x1)] = 0 · x1 + -∞
[W(x1)] = 4 · x1 + -∞
[Yb(x1)] = 10 · x1 + -∞
[D(x1)] = 0 · x1 + -∞
[Yc(x1)] = 12 · x1 + -∞
[Xa(x1)] = 12 · x1 + -∞
[d(x1)] = 8 · x1 + -∞
[B(x1)] = 4 · x1 + -∞
[Xb(x1)] = 10 · x1 + -∞
[R(x1)] = 4 · x1 + -∞
[E(x1)] = 0 · x1 + -∞
[Xd(x1)] = 8 · x1 + -∞
[Xc(x1)] = 12 · x1 + -∞
[L(x1)] = 0 · x1 + -∞
[b(x1)] = 10 · 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(x0))) → D(c(d(x0)))
L(c(c(x0))) → D(d(d(d(x0))))
L(d(d(d(x0)))) → D(a(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)] = 0 · x1 + -∞
[a(x1)] = 0 · x1 + -∞
[Ya(x1)] = 0 · x1 + -∞
[c(x1)] = 0 · x1 + -∞
[V(x1)] = 0 · x1 + -∞
[W(x1)] = 0 · x1 + -∞
[Yb(x1)] = 8 · x1 + -∞
[D(x1)] = 0 · x1 + -∞
[Yc(x1)] = 0 · x1 + -∞
[Xa(x1)] = 0 · x1 + -∞
[d(x1)] = 0 · x1 + -∞
[B(x1)] = 0 · x1 + -∞
[Xb(x1)] = 8 · x1 + -∞
[R(x1)] = 0 · x1 + -∞
[E(x1)] = 0 · x1 + -∞
[Xd(x1)] = 0 · x1 + -∞
[Xc(x1)] = 0 · x1 + -∞
[L(x1)] = 0 · x1 + -∞
[b(x1)] = 8 · 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(c(c(x0))) → D(d(d(d(x0))))
L(d(d(d(x0)))) → D(a(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.1 Rule Removal

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

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