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: {3}
   transitions:
    b3(212) -> 213*
    b3(132) -> 133*
    b3(264) -> 265*
    b3(214) -> 215*
    b3(184) -> 185*
    b3(154) -> 155*
    b3(104) -> 105*
    b3(186) -> 187*
    b3(156) -> 157*
    b3(106) -> 107*
    b3(208) -> 209*
    b3(188) -> 189*
    b3(158) -> 159*
    b3(128) -> 129*
    b3(108) -> 109*
    b3(240) -> 241*
    b3(220) -> 221*
    b3(210) -> 211*
    b3(190) -> 191*
    b3(130) -> 131*
    a4(262) -> 263*
    a4(257) -> 258*
    a4(232) -> 233*
    a4(227) -> 228*
    a4(259) -> 260*
    a4(234) -> 235*
    a4(229) -> 230*
    a4(261) -> 262*
    a4(231) -> 232*
    a4(233) -> 234*
    a4(260) -> 261*
    a4(255) -> 256*
    b4(254) -> 255*
    b4(256) -> 257*
    b4(226) -> 227*
    b4(258) -> 259*
    b4(228) -> 229*
    b4(230) -> 231*
    b0(3) -> 3*
    a0(3) -> 3*
    a1(20) -> 21*
    a1(15) -> 16*
    a1(22) -> 23*
    a1(17) -> 18*
    a1(19) -> 20*
    a1(21) -> 22*
    b1(74) -> 75*
    b1(14) -> 15*
    b1(46) -> 47*
    b1(16) -> 17*
    b1(68) -> 69*
    b1(48) -> 49*
    b1(18) -> 19*
    a2(60) -> 61*
    a2(55) -> 56*
    a2(30) -> 31*
    a2(25) -> 26*
    a2(82) -> 83*
    a2(77) -> 78*
    a2(62) -> 63*
    a2(57) -> 58*
    a2(32) -> 33*
    a2(27) -> 28*
    a2(84) -> 85*
    a2(79) -> 80*
    a2(59) -> 60*
    a2(29) -> 30*
    a2(81) -> 82*
    a2(61) -> 62*
    a2(31) -> 32*
    a2(83) -> 84*
    b2(242) -> 243*
    b2(114) -> 115*
    b2(54) -> 55*
    b2(24) -> 25*
    b2(126) -> 127*
    b2(76) -> 77*
    b2(66) -> 67*
    b2(56) -> 57*
    b2(26) -> 27*
    b2(98) -> 99*
    b2(78) -> 79*
    b2(58) -> 59*
    b2(28) -> 29*
    b2(150) -> 151*
    b2(80) -> 81*
    a3(217) -> 218*
    a3(192) -> 193*
    a3(187) -> 188*
    a3(162) -> 163*
    a3(157) -> 158*
    a3(112) -> 113*
    a3(107) -> 108*
    a3(194) -> 195*
    a3(189) -> 190*
    a3(159) -> 160*
    a3(134) -> 135*
    a3(129) -> 130*
    a3(109) -> 110*
    a3(216) -> 217*
    a3(211) -> 212*
    a3(191) -> 192*
    a3(161) -> 162*
    a3(136) -> 137*
    a3(131) -> 132*
    a3(111) -> 112*
    a3(218) -> 219*
    a3(213) -> 214*
    a3(193) -> 194*
    a3(133) -> 134*
    a3(215) -> 216*
    a3(160) -> 161*
    a3(155) -> 156*
    a3(135) -> 136*
    a3(110) -> 111*
    a3(105) -> 106*
    3 -> 14*
    19 -> 54*
    20 -> 24*
    21 -> 98,46
    22 -> 48*
    23 -> 15,17,3
    29 -> 150*
    30 -> 66*
    31 -> 76,68
    32 -> 74*
    33 -> 15,3,14,17
    47 -> 25*
    49 -> 25*
    61 -> 104*
    63 -> 79,27
    67 -> 25*
    69 -> 15*
    75 -> 15*
    81 -> 184*
    82 -> 154*
    83 -> 128,114
    84 -> 126*
    85 -> 25,19
    99 -> 77*
    111 -> 254,208
    113 -> 155,67,25
    115 -> 55*
    127 -> 55*
    133 -> 226*
    134 -> 220*
    135 -> 210*
    136 -> 186*
    137 -> 29*
    151 -> 25*
    163 -> 57*
    185 -> 155*
    193 -> 264,242
    195 -> 17,79
    209 -> 129*
    217 -> 240*
    219 -> 27*
    221 -> 211*
    235 -> 189*
    241 -> 105*
    243 -> 77*
    263 -> 159*
    265 -> 105*
  problem:
   
  Qed