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))
 }
 DUP: We consider a non-duplicating system.
  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))
   }
  BOUND:
   Automaton:
    {
     w_1(21) -> 22,
      w_0(7) -> 7,
     v_1(16) -> 17,
      v_0(7) -> 7,
     u_1(17) -> 18,
      u_0(7) -> 7,
     b_2(36) -> 37,
     b_1(32) -> 33,
     b_1(26) -> 27,
     b_1(12) -> 13,
      b_0(7) -> 7,
     d_1(44) -> 45,
     d_1(25) -> 26,
      d_0(7) -> 7,
      a_0(7) -> 7,
      c_1(8) -> 9,
      c_0(7) -> 7,
          45 -> 26,
          37 -> 22 | 17,
          33 -> 7,
          27 -> 17,
          22 -> 17,
          18 -> 22 | 17 | 7,
          13 -> 18 | 7,
           9 -> 7,
           8 -> 44 | 36 | 32,
           7 -> 25 | 21 | 16 | 12 | 8
    }
   Strict:
    {}
   Qed