YES(?,O(n^1))

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

Proof:
 Bounds Processor:
  bound: 4
  enrichment: match
  automaton:
   final states: {3}
   transitions:
    a3(252) -> 253*
    a3(247) -> 248*
    a3(237) -> 238*
    a3(207) -> 208*
    a3(197) -> 198*
    a3(172) -> 173*
    a3(152) -> 153*
    a3(294) -> 295*
    a3(249) -> 250*
    a3(239) -> 240*
    a3(234) -> 235*
    a3(209) -> 210*
    a3(194) -> 195*
    a3(174) -> 175*
    a3(154) -> 155*
    a3(296) -> 297*
    a3(251) -> 252*
    a3(236) -> 237*
    a3(196) -> 197*
    a3(176) -> 177*
    a3(151) -> 152*
    a3(293) -> 294*
    a3(253) -> 254*
    a3(238) -> 239*
    a3(228) -> 229*
    a3(213) -> 214*
    a3(198) -> 199*
    a3(173) -> 174*
    a3(153) -> 154*
    a3(295) -> 296*
    a3(250) -> 251*
    a3(240) -> 241*
    a3(195) -> 196*
    a3(175) -> 176*
    a3(155) -> 156*
    a3(297) -> 298*
    b4(379) -> 380*
    b4(359) -> 360*
    b4(344) -> 345*
    b4(334) -> 335*
    b4(324) -> 325*
    b4(289) -> 290*
    b4(381) -> 382*
    b4(356) -> 357*
    b4(346) -> 347*
    b4(336) -> 337*
    b4(326) -> 327*
    b4(291) -> 292*
    b4(378) -> 379*
    b4(358) -> 359*
    b4(348) -> 349*
    b4(333) -> 334*
    b4(323) -> 324*
    b4(288) -> 289*
    b4(380) -> 381*
    b4(355) -> 356*
    b4(345) -> 346*
    b4(335) -> 336*
    b4(325) -> 326*
    b4(290) -> 291*
    b4(377) -> 378*
    b4(357) -> 358*
    b4(347) -> 348*
    b4(337) -> 338*
    b4(322) -> 323*
    b4(287) -> 288*
    a4(374) -> 375*
    a4(354) -> 355*
    a4(339) -> 340*
    a4(329) -> 330*
    a4(319) -> 320*
    a4(284) -> 285*
    a4(376) -> 377*
    a4(351) -> 352*
    a4(341) -> 342*
    a4(331) -> 332*
    a4(321) -> 322*
    a4(286) -> 287*
    a4(373) -> 374*
    a4(353) -> 354*
    a4(343) -> 344*
    a4(328) -> 329*
    a4(318) -> 319*
    a4(283) -> 284*
    a4(375) -> 376*
    a4(350) -> 351*
    a4(340) -> 341*
    a4(330) -> 331*
    a4(320) -> 321*
    a4(285) -> 286*
    a4(372) -> 373*
    a4(352) -> 353*
    a4(342) -> 343*
    a4(332) -> 333*
    a4(317) -> 318*
    a4(282) -> 283*
    a0(3) -> 3*
    b0(3) -> 3*
    b1(20) -> 21*
    b1(22) -> 23*
    b1(24) -> 25*
    b1(21) -> 22*
    b1(23) -> 24*
    a1(65) -> 66*
    a1(50) -> 51*
    a1(15) -> 16*
    a1(67) -> 68*
    a1(17) -> 18*
    a1(19) -> 20*
    a1(16) -> 17*
    a1(18) -> 19*
    b2(75) -> 76*
    b2(35) -> 36*
    b2(132) -> 133*
    b2(117) -> 118*
    b2(77) -> 78*
    b2(32) -> 33*
    b2(134) -> 135*
    b2(114) -> 115*
    b2(74) -> 75*
    b2(34) -> 35*
    b2(131) -> 132*
    b2(116) -> 117*
    b2(76) -> 77*
    b2(31) -> 32*
    b2(133) -> 134*
    b2(113) -> 114*
    b2(78) -> 79*
    b2(33) -> 34*
    b2(130) -> 131*
    b2(115) -> 116*
    a2(70) -> 71*
    a2(30) -> 31*
    a2(127) -> 128*
    a2(112) -> 113*
    a2(72) -> 73*
    a2(27) -> 28*
    a2(149) -> 150*
    a2(129) -> 130*
    a2(119) -> 120*
    a2(109) -> 110*
    a2(69) -> 70*
    a2(29) -> 30*
    a2(166) -> 167*
    a2(136) -> 137*
    a2(126) -> 127*
    a2(121) -> 122*
    a2(111) -> 112*
    a2(71) -> 72*
    a2(26) -> 27*
    a2(128) -> 129*
    a2(123) -> 124*
    a2(108) -> 109*
    a2(73) -> 74*
    a2(28) -> 29*
    a2(125) -> 126*
    a2(110) -> 111*
    b3(257) -> 258*
    b3(242) -> 243*
    b3(202) -> 203*
    b3(177) -> 178*
    b3(157) -> 158*
    b3(299) -> 300*
    b3(254) -> 255*
    b3(244) -> 245*
    b3(199) -> 200*
    b3(179) -> 180*
    b3(159) -> 160*
    b3(301) -> 302*
    b3(256) -> 257*
    b3(241) -> 242*
    b3(201) -> 202*
    b3(181) -> 182*
    b3(156) -> 157*
    b3(298) -> 299*
    b3(258) -> 259*
    b3(243) -> 244*
    b3(203) -> 204*
    b3(178) -> 179*
    b3(158) -> 159*
    b3(300) -> 301*
    b3(255) -> 256*
    b3(245) -> 246*
    b3(200) -> 201*
    b3(180) -> 181*
    b3(160) -> 161*
    b3(302) -> 303*
    3 -> 15*
    20 -> 125*
    21 -> 108*
    22 -> 119*
    23 -> 26*
    24 -> 50*
    25 -> 16,17,18,3
    31 -> 172*
    32 -> 151,121
    33 -> 207,123
    34 -> 209,69,65
    35 -> 136,67
    36 -> 126,19,20,16,17,3,18
    51 -> 27*
    66 -> 16*
    68 -> 16*
    74 -> 228*
    75 -> 234*
    76 -> 194*
    77 -> 213,166
    78 -> 149*
    79 -> 126,127,18,19,20
    114 -> 293*
    116 -> 247*
    118 -> 29*
    120 -> 109*
    122 -> 27*
    124 -> 27*
    135 -> 111*
    137 -> 126*
    150 -> 126*
    157 -> 328*
    159 -> 249*
    161 -> 197,72
    167 -> 70*
    178 -> 317*
    180 -> 236*
    182 -> 197,29
    204 -> 129,130,128
    208 -> 195*
    210 -> 195*
    214 -> 195*
    229 -> 152*
    235 -> 152*
    242 -> 350*
    244 -> 282*
    246 -> 173*
    248 -> 237*
    255 -> 372*
    257 -> 339*
    259 -> 229*
    292 -> 176*
    303 -> 239*
    327 -> 239*
    338 -> 252*
    349 -> 155*
    360 -> 285*
    382 -> 342*
  problem:
   
  Qed