Termination w.r.t. Q of the given QTRS could be proven:

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

a(c(d(x))) → c(x)
u(b(d(d(x)))) → b(x)
v(a(a(x))) → u(v(x))
v(a(c(x))) → u(b(d(x)))
v(c(x)) → b(x)
w(a(a(x))) → u(w(x))
w(a(c(x))) → u(b(d(x)))
w(c(x)) → b(x)

Q is empty.

(1) DirectTerminationProof (EQUIVALENT transformation)

We use [DIRECT_TERMINATION] with the following order to prove termination.

Knuth-Bendix order [KBO] with precedence:

w₁ > d₁ > v₁ > b₁ > a₁ > c₁ > u₁

and weight map:

a_1=3
c_1=1
d_1=2
u_1=1
b_1=8
v_1=7
w_1=7

The variable weight is 1

(2) TRUE