YES(?,O(n^1))

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

Proof:
 Bounds Processor:
  bound: 3
  enrichment: match
  automaton:
   final states: {3}
   transitions:
    a3(167) -> 168*
    a3(159) -> 160*
    a3(144) -> 145*
    a3(134) -> 135*
    a3(166) -> 167*
    a3(161) -> 162*
    a3(136) -> 137*
    a3(126) -> 127*
    a3(163) -> 164*
    a3(143) -> 144*
    a3(138) -> 139*
    a3(133) -> 134*
    a3(128) -> 129*
    a3(140) -> 141*
    a3(130) -> 131*
    a1(22) -> 23*
    a1(14) -> 15*
    a1(21) -> 22*
    a1(16) -> 17*
    a1(18) -> 19*
    b3(162) -> 163*
    b3(142) -> 143*
    b3(137) -> 138*
    b3(132) -> 133*
    b3(127) -> 128*
    b3(164) -> 165*
    b3(139) -> 140*
    b3(129) -> 130*
    b3(141) -> 142*
    b3(131) -> 132*
    b3(165) -> 166*
    b3(160) -> 161*
    b1(50) -> 51*
    b1(20) -> 21*
    b1(15) -> 16*
    b1(52) -> 53*
    b1(17) -> 18*
    b1(19) -> 20*
    b1(46) -> 47*
    a2(65) -> 66*
    a2(102) -> 103*
    a2(97) -> 98*
    a2(32) -> 33*
    a2(99) -> 100*
    a2(84) -> 85*
    a2(64) -> 65*
    a2(59) -> 60*
    a2(24) -> 25*
    a2(76) -> 77*
    a2(61) -> 62*
    a2(31) -> 32*
    a2(26) -> 27*
    a2(103) -> 104*
    a2(83) -> 84*
    a2(78) -> 79*
    a2(28) -> 29*
    a2(80) -> 81*
    b0(3) -> 3*
    b2(60) -> 61*
    b2(30) -> 31*
    b2(25) -> 26*
    b2(82) -> 83*
    b2(77) -> 78*
    b2(62) -> 63*
    b2(27) -> 28*
    b2(79) -> 80*
    b2(29) -> 30*
    b2(146) -> 147*
    b2(101) -> 102*
    b2(96) -> 97*
    b2(81) -> 82*
    b2(98) -> 99*
    b2(63) -> 64*
    b2(58) -> 59*
    b2(105) -> 106*
    b2(100) -> 101*
    a0(3) -> 3*
    3 -> 14*
    21 -> 76*
    22 -> 46,24
    23 -> 16,18,3
    31 -> 126*
    32 -> 105,50
    33 -> 20,58,52,16,3,14,18
    47 -> 16*
    51 -> 16*
    53 -> 16*
    65 -> 96*
    66 -> 18,20
    85 -> 28*
    102 -> 159*
    103 -> 136*
    104 -> 47,18,78
    106 -> 97*
    135 -> 61*
    144 -> 146*
    145 -> 20,82
    147 -> 97*
    168 -> 140*
  problem:
   
  Qed