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: 1
  enrichment: match
  automaton:
   final states: {7,6,5,4}
   transitions:
    b1(20) -> 21*
    b1(26) -> 27*
    b1(28) -> 29*
    c1(10) -> 11*
    c1(12) -> 13*
    c1(18) -> 19*
    a0(2) -> 4*
    a0(1) -> 4*
    a0(3) -> 4*
    c0(2) -> 1*
    c0(1) -> 1*
    c0(3) -> 1*
    d0(2) -> 2*
    d0(1) -> 2*
    d0(3) -> 2*
    u0(2) -> 5*
    u0(1) -> 5*
    u0(3) -> 5*
    b0(2) -> 3*
    b0(1) -> 3*
    b0(3) -> 3*
    v0(2) -> 6*
    v0(1) -> 6*
    v0(3) -> 6*
    w0(2) -> 7*
    w0(1) -> 7*
    w0(3) -> 7*
    1 -> 26,12
    2 -> 20,10
    3 -> 28,18
    11 -> 4*
    13 -> 4*
    19 -> 4*
    21 -> 7,6,5
    27 -> 7,6,5
    29 -> 7,6,5
  problem:
   
  Qed