YES(?,O(n^1))

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

Proof:
 Bounds Processor:
  bound: 5
  enrichment: match
  automaton:
   final states: {2,1}
   transitions:
    a3(272) -> 273*
    a3(469) -> 470*
    a3(252) -> 253*
    a3(232) -> 233*
    a3(222) -> 223*
    a3(399) -> 400*
    a3(192) -> 193*
    a3(364) -> 365*
    a3(334) -> 335*
    a3(324) -> 325*
    a3(299) -> 300*
    a3(289) -> 290*
    a3(274) -> 275*
    a3(471) -> 472*
    a3(254) -> 255*
    a3(234) -> 235*
    a3(224) -> 225*
    a3(396) -> 397*
    a3(194) -> 195*
    a3(361) -> 362*
    a3(336) -> 337*
    a3(326) -> 327*
    a3(301) -> 302*
    a3(291) -> 292*
    a3(271) -> 272*
    a3(468) -> 469*
    a3(256) -> 257*
    a3(231) -> 232*
    a3(221) -> 222*
    a3(398) -> 399*
    a3(196) -> 197*
    a3(363) -> 364*
    a3(333) -> 334*
    a3(328) -> 329*
    a3(298) -> 299*
    a3(288) -> 289*
    a3(273) -> 274*
    a3(470) -> 471*
    a3(253) -> 254*
    a3(233) -> 234*
    a3(223) -> 224*
    a3(400) -> 401*
    a3(193) -> 194*
    a3(360) -> 361*
    a3(335) -> 336*
    a3(325) -> 326*
    a3(300) -> 301*
    a3(290) -> 291*
    a3(472) -> 473*
    a3(270) -> 271*
    a3(255) -> 256*
    a3(230) -> 231*
    a3(225) -> 226*
    a3(397) -> 398*
    a3(195) -> 196*
    a3(362) -> 363*
    a3(337) -> 338*
    a3(327) -> 328*
    a3(297) -> 298*
    a3(292) -> 293*
    b4(439) -> 440*
    b4(374) -> 375*
    b4(546) -> 547*
    b4(511) -> 512*
    b4(446) -> 447*
    b4(411) -> 412*
    b4(376) -> 377*
    b4(518) -> 519*
    b4(483) -> 484*
    b4(448) -> 449*
    b4(438) -> 439*
    b4(545) -> 546*
    b4(520) -> 521*
    b4(510) -> 511*
    b4(410) -> 411*
    b4(375) -> 376*
    b4(547) -> 548*
    b4(482) -> 483*
    b4(447) -> 448*
    b4(437) -> 438*
    b4(412) -> 413*
    b4(519) -> 520*
    b4(509) -> 510*
    b4(484) -> 485*
    a4(479) -> 480*
    a4(444) -> 445*
    a4(434) -> 435*
    a4(409) -> 410*
    a4(369) -> 370*
    a4(541) -> 542*
    a4(516) -> 517*
    a4(506) -> 507*
    a4(481) -> 482*
    a4(441) -> 442*
    a4(436) -> 437*
    a4(406) -> 407*
    a4(371) -> 372*
    a4(543) -> 544*
    a4(513) -> 514*
    a4(508) -> 509*
    a4(478) -> 479*
    a4(443) -> 444*
    a4(433) -> 434*
    a4(408) -> 409*
    a4(373) -> 374*
    a4(540) -> 541*
    a4(515) -> 516*
    a4(505) -> 506*
    a4(480) -> 481*
    a4(445) -> 446*
    a4(435) -> 436*
    a4(405) -> 406*
    a4(370) -> 371*
    a4(542) -> 543*
    a4(517) -> 518*
    a4(507) -> 508*
    a4(477) -> 478*
    a4(442) -> 443*
    a4(432) -> 433*
    a4(407) -> 408*
    a4(372) -> 373*
    a4(544) -> 545*
    a4(514) -> 515*
    a4(504) -> 505*
    a0(2) -> 1*
    a0(1) -> 1*
    b5(581) -> 582*
    b5(556) -> 557*
    b5(583) -> 584*
    b5(555) -> 556*
    b5(582) -> 583*
    b5(554) -> 555*
    b0(2) -> 2*
    b0(1) -> 2*
    a5(576) -> 577*
    a5(551) -> 552*
    a5(578) -> 579*
    a5(553) -> 554*
    a5(580) -> 581*
    a5(550) -> 551*
    a5(577) -> 578*
    a5(552) -> 553*
    a5(579) -> 580*
    a5(549) -> 550*
    b1(40) -> 41*
    b1(10) -> 11*
    b1(39) -> 40*
    b1(9) -> 10*
    b1(11) -> 12*
    b1(38) -> 39*
    a1(35) -> 36*
    a1(5) -> 6*
    a1(37) -> 38*
    a1(7) -> 8*
    a1(44) -> 45*
    a1(34) -> 35*
    a1(4) -> 5*
    a1(101) -> 102*
    a1(36) -> 37*
    a1(31) -> 32*
    a1(6) -> 7*
    a1(88) -> 89*
    a1(33) -> 34*
    a1(8) -> 9*
    b2(60) -> 61*
    b2(172) -> 173*
    b2(152) -> 153*
    b2(72) -> 73*
    b2(62) -> 63*
    b2(189) -> 190*
    b2(109) -> 110*
    b2(171) -> 172*
    b2(151) -> 152*
    b2(71) -> 72*
    b2(61) -> 62*
    b2(188) -> 189*
    b2(108) -> 109*
    b2(73) -> 74*
    b2(190) -> 191*
    b2(170) -> 171*
    b2(150) -> 151*
    b2(110) -> 111*
    a2(75) -> 76*
    a2(70) -> 71*
    a2(55) -> 56*
    a2(187) -> 188*
    a2(167) -> 168*
    a2(147) -> 148*
    a2(107) -> 108*
    a2(67) -> 68*
    a2(57) -> 58*
    a2(184) -> 185*
    a2(169) -> 170*
    a2(149) -> 150*
    a2(134) -> 135*
    a2(104) -> 105*
    a2(69) -> 70*
    a2(59) -> 60*
    a2(186) -> 187*
    a2(166) -> 167*
    a2(146) -> 147*
    a2(121) -> 122*
    a2(106) -> 107*
    a2(66) -> 67*
    a2(56) -> 57*
    a2(183) -> 184*
    a2(168) -> 169*
    a2(148) -> 149*
    a2(103) -> 104*
    a2(68) -> 69*
    a2(58) -> 59*
    a2(250) -> 251*
    a2(185) -> 186*
    a2(165) -> 166*
    a2(145) -> 146*
    a2(105) -> 106*
    b3(277) -> 278*
    b3(474) -> 475*
    b3(257) -> 258*
    b3(237) -> 238*
    b3(227) -> 228*
    b3(197) -> 198*
    b3(339) -> 340*
    b3(329) -> 330*
    b3(304) -> 305*
    b3(294) -> 295*
    b3(259) -> 260*
    b3(401) -> 402*
    b3(199) -> 200*
    b3(366) -> 367*
    b3(331) -> 332*
    b3(276) -> 277*
    b3(473) -> 474*
    b3(236) -> 237*
    b3(226) -> 227*
    b3(403) -> 404*
    b3(338) -> 339*
    b3(303) -> 304*
    b3(293) -> 294*
    b3(475) -> 476*
    b3(258) -> 259*
    b3(228) -> 229*
    b3(198) -> 199*
    b3(365) -> 366*
    b3(340) -> 341*
    b3(330) -> 331*
    b3(295) -> 296*
    b3(275) -> 276*
    b3(235) -> 236*
    b3(402) -> 403*
    b3(367) -> 368*
    b3(302) -> 303*
    1 -> 31*
    2 -> 4*
    9 -> 103*
    10 -> 55,44
    11 -> 33*
    12 -> 6,32,1
    32 -> 5*
    38 -> 121*
    39 -> 101,75
    40 -> 88*
    41 -> 6,1,32
    45 -> 5*
    61 -> 66*
    63 -> 7,8,6
    71 -> 270*
    72 -> 192,134
    73 -> 183*
    74 -> 104,9,103,6,7,8
    76 -> 67*
    89 -> 5*
    102 -> 5*
    109 -> 145*
    111 -> 35*
    122 -> 56*
    135 -> 67*
    151 -> 165*
    153 -> 37*
    171 -> 221*
    173 -> 122*
    189 -> 250,230
    191 -> 6,57
    198 -> 252*
    200 -> 105,106
    227 -> 324*
    229 -> 58*
    238 -> 59*
    251 -> 56*
    257 -> 369*
    259 -> 297*
    260 -> 108,107
    276 -> 288*
    278 -> 185*
    296 -> 187*
    303 -> 333*
    305 -> 147*
    329 -> 432*
    331 -> 360*
    332 -> 60*
    341 -> 149*
    366 -> 396*
    368 -> 68*
    375 -> 405*
    377 -> 299*
    402 -> 468*
    404 -> 70*
    413 -> 301*
    438 -> 441*
    440 -> 362*
    449 -> 364*
    474 -> 477*
    476 -> 271*
    483 -> 504*
    485 -> 273*
    509 -> 549*
    511 -> 513*
    512 -> 275*
    519 -> 540*
    521 -> 290*
    548 -> 292*
    555 -> 576*
    557 -> 515*
    584 -> 517*
  problem:
   
  Qed