YES
O(n)
TRS:
 {
     a(c(d(x))) -> c(x),
  u(b(d(d(x)))) -> b(x),
        v(c(x)) -> b(x),
     v(a(c(x))) -> u(b(d(x))),
     v(a(a(x))) -> u(v(x)),
        w(c(x)) -> b(x),
     w(a(c(x))) -> u(b(d(x))),
     w(a(a(x))) -> u(w(x))
 }
 Natural interpretation:
  Strict:
   {
       a(c(d(x))) -> c(x),
    u(b(d(d(x)))) -> b(x),
          v(c(x)) -> b(x),
       v(a(c(x))) -> u(b(d(x))),
       v(a(a(x))) -> u(v(x)),
          w(c(x)) -> b(x),
       w(a(c(x))) -> u(b(d(x))),
       w(a(a(x))) -> u(w(x))
   }
  Weak:
   {}
  Interpretation class: stronglylinear
  [w](X0) = + 1*X0 + 0
  [v](X0) = + 1*X0 + 0
  [u](X0) = + 1*X0 + 0
  [b](X0) = + 1*X0 + 0
  [d](X0) = + 1*X0 + 1
  [a](X0) = + 1*X0 + 1
  [c](X0) = + 1*X0 + 1
  
  Qed