YES(?,O(n^1))

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

Proof:
 Bounds Processor:
  bound: 4
  enrichment: match
  automaton:
   final states: {2,1}
   transitions:
    b3(202) -> 203*
    b3(192) -> 193*
    b3(194) -> 195*
    b3(134) -> 135*
    b3(246) -> 247*
    b3(166) -> 167*
    b3(136) -> 137*
    b3(106) -> 107*
    b3(248) -> 249*
    b3(198) -> 199*
    b3(168) -> 169*
    b3(138) -> 139*
    b3(108) -> 109*
    b3(240) -> 241*
    b3(200) -> 201*
    b3(170) -> 171*
    b3(110) -> 111*
    a4(224) -> 225*
    a4(219) -> 220*
    a4(214) -> 215*
    a4(209) -> 210*
    a4(226) -> 227*
    a4(221) -> 222*
    a4(216) -> 217*
    a4(211) -> 212*
    a4(223) -> 224*
    a4(213) -> 214*
    a4(225) -> 226*
    a4(215) -> 216*
    b4(222) -> 223*
    b4(212) -> 213*
    b4(218) -> 219*
    b4(208) -> 209*
    b4(220) -> 221*
    b4(210) -> 211*
    b0(2) -> 1*
    b0(1) -> 1*
    a0(2) -> 2*
    a0(1) -> 2*
    a1(10) -> 11*
    a1(5) -> 6*
    a1(12) -> 13*
    a1(7) -> 8*
    a1(9) -> 10*
    a1(11) -> 12*
    b1(62) -> 63*
    b1(64) -> 65*
    b1(34) -> 35*
    b1(4) -> 5*
    b1(6) -> 7*
    b1(58) -> 59*
    b1(8) -> 9*
    a2(102) -> 103*
    a2(97) -> 98*
    a2(72) -> 73*
    a2(67) -> 68*
    a2(42) -> 43*
    a2(37) -> 38*
    a2(104) -> 105*
    a2(99) -> 100*
    a2(74) -> 75*
    a2(69) -> 70*
    a2(44) -> 45*
    a2(39) -> 40*
    a2(101) -> 102*
    a2(71) -> 72*
    a2(41) -> 42*
    a2(103) -> 104*
    a2(73) -> 74*
    a2(43) -> 44*
    b2(70) -> 71*
    b2(40) -> 41*
    b2(144) -> 145*
    b2(176) -> 177*
    b2(96) -> 97*
    b2(76) -> 77*
    b2(66) -> 67*
    b2(36) -> 37*
    b2(98) -> 99*
    b2(78) -> 79*
    b2(68) -> 69*
    b2(38) -> 39*
    b2(120) -> 121*
    b2(100) -> 101*
    a3(172) -> 173*
    a3(167) -> 168*
    a3(142) -> 143*
    a3(137) -> 138*
    a3(112) -> 113*
    a3(107) -> 108*
    a3(204) -> 205*
    a3(199) -> 200*
    a3(174) -> 175*
    a3(169) -> 170*
    a3(139) -> 140*
    a3(114) -> 115*
    a3(109) -> 110*
    a3(206) -> 207*
    a3(201) -> 202*
    a3(171) -> 172*
    a3(141) -> 142*
    a3(111) -> 112*
    a3(203) -> 204*
    a3(173) -> 174*
    a3(113) -> 114*
    a3(205) -> 206*
    a3(140) -> 141*
    a3(135) -> 136*
    1 -> 34*
    2 -> 4*
    9 -> 78*
    10 -> 64,36
    11 -> 76,62
    12 -> 58*
    13 -> 5,7,1
    35 -> 5*
    43 -> 198,66
    45 -> 69,7
    59 -> 5*
    63 -> 5*
    65 -> 5*
    71 -> 194*
    72 -> 106*
    73 -> 134,96
    74 -> 120*
    75 -> 39,7,37,9,65
    77 -> 67*
    79 -> 37*
    101 -> 240*
    102 -> 192*
    103 -> 248,176
    104 -> 144*
    105 -> 65,5,37,7,9,39
    115 -> 39*
    121 -> 37*
    139 -> 208*
    142 -> 166*
    143 -> 41*
    145 -> 37*
    173 -> 246*
    175 -> 201,69
    177 -> 67*
    193 -> 107*
    195 -> 107*
    205 -> 218*
    207 -> 107*
    217 -> 169*
    227 -> 111*
    241 -> 107*
    247 -> 199*
    249 -> 135*
  problem:
   
  Qed