YES(?,O(n^1))

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

Proof:
 Bounds Processor:
  bound: 5
  enrichment: match
  automaton:
   final states: {2,1}
   transitions:
    b3(242) -> 243*
    b3(137) -> 138*
    b3(112) -> 113*
    b3(97) -> 98*
    b3(144) -> 145*
    b3(139) -> 140*
    b3(114) -> 115*
    b3(99) -> 100*
    b3(201) -> 202*
    b3(146) -> 147*
    b3(153) -> 154*
    b3(148) -> 149*
    b3(135) -> 136*
    b3(110) -> 111*
    b3(95) -> 96*
    a4(267) -> 268*
    a4(227) -> 228*
    a4(207) -> 208*
    a4(197) -> 198*
    a4(187) -> 188*
    a4(229) -> 230*
    a4(214) -> 215*
    a4(209) -> 210*
    a4(189) -> 190*
    a4(179) -> 180*
    a4(221) -> 222*
    a4(211) -> 212*
    a4(196) -> 197*
    a4(191) -> 192*
    a4(186) -> 187*
    a4(181) -> 182*
    a4(228) -> 229*
    a4(223) -> 224*
    a4(213) -> 214*
    a4(193) -> 194*
    a4(183) -> 184*
    a4(225) -> 226*
    a4(215) -> 216*
    a4(195) -> 196*
    a4(185) -> 186*
    b4(222) -> 223*
    b4(212) -> 213*
    b4(192) -> 193*
    b4(182) -> 183*
    b4(224) -> 225*
    b4(194) -> 195*
    b4(184) -> 185*
    b4(226) -> 227*
    b4(208) -> 209*
    b4(210) -> 211*
    b4(190) -> 191*
    b4(180) -> 181*
    b0(2) -> 1*
    b0(1) -> 1*
    a5(262) -> 263*
    a5(257) -> 258*
    a5(259) -> 260*
    a5(261) -> 262*
    a5(263) -> 264*
    a5(255) -> 256*
    a0(2) -> 2*
    a0(1) -> 2*
    b5(256) -> 257*
    b5(258) -> 259*
    b5(260) -> 261*
    a1(10) -> 11*
    a1(12) -> 13*
    a1(34) -> 35*
    a1(4) -> 5*
    a1(11) -> 12*
    a1(6) -> 7*
    a1(8) -> 9*
    b1(65) -> 66*
    b1(5) -> 6*
    b1(67) -> 68*
    b1(52) -> 53*
    b1(7) -> 8*
    b1(9) -> 10*
    b1(48) -> 49*
    a2(40) -> 41*
    a2(82) -> 83*
    a2(42) -> 43*
    a2(44) -> 45*
    a2(81) -> 82*
    a2(76) -> 77*
    a2(36) -> 37*
    a2(78) -> 79*
    a2(73) -> 74*
    a2(43) -> 44*
    a2(38) -> 39*
    a2(80) -> 81*
    b2(75) -> 76*
    b2(77) -> 78*
    b2(37) -> 38*
    b2(104) -> 105*
    b2(79) -> 80*
    b2(39) -> 40*
    b2(41) -> 42*
    b2(63) -> 64*
    a3(147) -> 148*
    a3(142) -> 143*
    a3(117) -> 118*
    a3(102) -> 103*
    a3(149) -> 150*
    a3(134) -> 135*
    a3(94) -> 95*
    a3(151) -> 152*
    a3(141) -> 142*
    a3(136) -> 137*
    a3(116) -> 117*
    a3(111) -> 112*
    a3(101) -> 102*
    a3(96) -> 97*
    a3(138) -> 139*
    a3(113) -> 114*
    a3(98) -> 99*
    a3(150) -> 151*
    a3(145) -> 146*
    a3(140) -> 141*
    a3(130) -> 131*
    a3(115) -> 116*
    a3(100) -> 101*
    1 -> 34*
    2 -> 4*
    10 -> 73*
    11 -> 52,36
    13 -> 6,48,8,1
    35 -> 5*
    42 -> 134*
    43 -> 104,94,65
    44 -> 63*
    45 -> 38,75,53,10,67,6,1,34,8
    49 -> 6*
    53 -> 6*
    64 -> 38*
    66 -> 6*
    68 -> 6*
    74 -> 37*
    81 -> 130*
    83 -> 40*
    100 -> 189*
    101 -> 179*
    102 -> 110*
    103 -> 8,136,105,53,66,38,10,144,42,40
    105 -> 38*
    115 -> 267*
    116 -> 207*
    117 -> 153*
    118 -> 53,242,42,10,73,134,136,40,8,66,105
    131 -> 110*
    143 -> 78*
    150 -> 221*
    151 -> 201*
    152 -> 40,98
    154 -> 96*
    188 -> 140,138
    198 -> 147*
    202 -> 96*
    216 -> 138,140
    228 -> 255*
    230 -> 191*
    243 -> 145*
    264 -> 195*
    268 -> 190*
  problem:
   
  Qed