YES(?,O(n^1))

Problem:
 a(d(x1)) -> d(b(x1))
 a(x1) -> b(b(b(x1)))
 d(x1) -> x1
 a(x1) -> x1
 b(d(b(x1))) -> a(d(x1))
 b(c(x1)) -> c(d(d(x1)))
 a(c(x1)) -> b(b(c(d(x1))))

Proof:
 Bounds Processor:
  bound: 2
  enrichment: match
  automaton:
   final states: {4,3,2}
   transitions:
    b1(5) -> 6*
    b1(7) -> 8*
    b1(6) -> 7*
    c1(19) -> 20*
    c1(21) -> 22*
    d1(17) -> 18*
    d1(18) -> 19*
    c2(27) -> 28*
    c2(39) -> 40*
    d2(25) -> 26*
    d2(37) -> 38*
    d2(26) -> 27*
    d2(43) -> 44*
    d2(38) -> 39*
    a0(1) -> 2*
    d0(1) -> 3*
    b0(1) -> 4*
    c0(1) -> 1*
    1 -> 17,2,3,5
    8 -> 2*
    17 -> 18,21
    18 -> 19,21
    19 -> 43*
    20 -> 6,4
    21 -> 25*
    22 -> 6*
    25 -> 26*
    26 -> 27*
    27 -> 37*
    28 -> 7*
    37 -> 38*
    38 -> 39*
    40 -> 8*
    43 -> 44*
    44 -> 25*
  problem:
   
  Qed