YES(?,O(n^1))

Problem:
 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)

Proof:
 Bounds Processor:
  bound: 2
  enrichment: match
  automaton:
   final states: {8}
   transitions:
    b1(41) -> 42*
    b1(23) -> 24*
    b1(13) -> 14*
    u1(20) -> 21*
    d1(35) -> 36*
    d1(22) -> 23*
    w1(29) -> 30*
    v1(19) -> 20*
    c1(11) -> 12*
    b2(43) -> 44*
    a0(8) -> 8*
    c0(8) -> 8*
    d0(8) -> 8*
    u0(8) -> 8*
    b0(8) -> 8*
    v0(8) -> 8*
    w0(8) -> 8*
    8 -> 29,22,19,13,11
    11 -> 43,41,35
    12 -> 8*
    14 -> 21,8
    21 -> 30,20,8
    24 -> 20*
    30 -> 20*
    36 -> 13*
    42 -> 8*
    44 -> 30,20
  problem:
   
  Qed