YES(?,O(n^1))

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

Proof:
 Complexity Transformation Processor:
  strict:
   a(a(b(a(a(b(a(x1))))))) -> a(b(a(a(b(a(a(a(b(x1)))))))))
  weak:
   
  Bounds Processor:
   bound: 5
   enrichment: match
   automaton:
    final states: {3}
    transitions:
     b3(262) -> 263*
     b3(222) -> 223*
     b3(374) -> 375*
     b3(167) -> 168*
     b3(364) -> 365*
     b3(137) -> 138*
     b3(314) -> 315*
     b3(436) -> 437*
     b3(214) -> 215*
     b3(164) -> 165*
     b3(356) -> 357*
     b3(346) -> 347*
     b3(134) -> 135*
     b3(316) -> 317*
     b3(186) -> 187*
     b3(378) -> 379*
     b3(338) -> 339*
     b3(308) -> 309*
     b3(238) -> 239*
     b3(228) -> 229*
     b3(218) -> 219*
     b3(198) -> 199*
     b3(193) -> 194*
     b3(370) -> 371*
     b3(340) -> 341*
     b3(190) -> 191*
     b3(362) -> 363*
     b3(160) -> 161*
     b3(332) -> 333*
     b3(130) -> 131*
     a4(272) -> 273*
     a4(247) -> 248*
     a4(429) -> 430*
     a4(424) -> 425*
     a4(486) -> 487*
     a4(244) -> 245*
     a4(426) -> 427*
     a4(276) -> 277*
     a4(271) -> 272*
     a4(428) -> 429*
     a4(490) -> 491*
     a4(485) -> 486*
     a4(278) -> 279*
     a4(273) -> 274*
     a4(248) -> 249*
     a4(243) -> 244*
     a4(425) -> 426*
     a4(487) -> 488*
     a4(275) -> 276*
     a4(250) -> 251*
     a4(245) -> 246*
     a4(489) -> 490*
     b4(277) -> 278*
     b4(242) -> 243*
     b4(434) -> 435*
     b4(404) -> 405*
     b4(394) -> 395*
     b4(491) -> 492*
     b4(274) -> 275*
     b4(249) -> 250*
     b4(396) -> 397*
     b4(386) -> 387*
     b4(488) -> 489*
     b4(246) -> 247*
     b4(423) -> 424*
     b4(388) -> 389*
     b4(430) -> 431*
     b4(410) -> 411*
     b4(380) -> 381*
     b4(270) -> 271*
     b4(442) -> 443*
     b4(427) -> 428*
     b4(402) -> 403*
     b4(484) -> 485*
     a0(3) -> 3*
     a5(469) -> 470*
     a5(449) -> 450*
     a5(516) -> 517*
     a5(466) -> 467*
     a5(446) -> 447*
     a5(513) -> 514*
     a5(508) -> 509*
     a5(503) -> 504*
     a5(505) -> 506*
     a5(470) -> 471*
     a5(465) -> 466*
     a5(450) -> 451*
     a5(445) -> 446*
     a5(517) -> 518*
     a5(512) -> 513*
     a5(507) -> 508*
     a5(472) -> 473*
     a5(467) -> 468*
     a5(452) -> 453*
     a5(447) -> 448*
     a5(514) -> 515*
     a5(504) -> 505*
     b0(3) -> 3*
     b5(464) -> 465*
     b5(444) -> 445*
     b5(511) -> 512*
     b5(506) -> 507*
     b5(471) -> 472*
     b5(451) -> 452*
     b5(518) -> 519*
     b5(468) -> 469*
     b5(448) -> 449*
     b5(515) -> 516*
     b5(502) -> 503*
     b5(509) -> 510*
     a1(20) -> 21*
     a1(15) -> 16*
     a1(22) -> 23*
     a1(17) -> 18*
     a1(19) -> 20*
     a1(16) -> 17*
     b1(30) -> 31*
     b1(152) -> 153*
     b1(294) -> 295*
     b1(32) -> 33*
     b1(296) -> 297*
     b1(24) -> 25*
     b1(14) -> 15*
     b1(21) -> 22*
     b1(118) -> 119*
     b1(290) -> 291*
     b1(18) -> 19*
     a2(60) -> 61*
     a2(40) -> 41*
     a2(92) -> 93*
     a2(87) -> 88*
     a2(89) -> 90*
     a2(64) -> 65*
     a2(59) -> 60*
     a2(44) -> 45*
     a2(39) -> 40*
     a2(86) -> 87*
     a2(66) -> 67*
     a2(61) -> 62*
     a2(46) -> 47*
     a2(41) -> 42*
     a2(63) -> 64*
     a2(43) -> 44*
     a2(90) -> 91*
     a2(85) -> 86*
     b2(65) -> 66*
     b2(45) -> 46*
     b2(182) -> 183*
     b2(354) -> 355*
     b2(324) -> 325*
     b2(122) -> 123*
     b2(82) -> 83*
     b2(264) -> 265*
     b2(62) -> 63*
     b2(42) -> 43*
     b2(234) -> 235*
     b2(124) -> 125*
     b2(114) -> 115*
     b2(306) -> 307*
     b2(84) -> 85*
     b2(226) -> 227*
     b2(348) -> 349*
     b2(106) -> 107*
     b2(91) -> 92*
     b2(158) -> 159*
     b2(330) -> 331*
     b2(108) -> 109*
     b2(88) -> 89*
     b2(68) -> 69*
     b2(58) -> 59*
     b2(38) -> 39*
     b2(200) -> 201*
     b2(150) -> 151*
     b2(322) -> 323*
     b2(302) -> 303*
     a3(192) -> 193*
     a3(187) -> 188*
     a3(162) -> 163*
     a3(132) -> 133*
     a3(194) -> 195*
     a3(189) -> 190*
     a3(191) -> 192*
     a3(166) -> 167*
     a3(161) -> 162*
     a3(136) -> 137*
     a3(131) -> 132*
     a3(188) -> 189*
     a3(168) -> 169*
     a3(163) -> 164*
     a3(138) -> 139*
     a3(133) -> 134*
     a3(165) -> 166*
     a3(135) -> 136*
     3 -> 14*
     15 -> 182*
     16 -> 82*
     17 -> 38,24
     19 -> 58*
     20 -> 84,30
     22 -> 68,32
     23 -> 41,17,3
     25 -> 15*
     31 -> 15*
     33 -> 15*
     39 -> 362,348
     40 -> 436,306
     41 -> 316,290
     43 -> 346,302
     44 -> 340,330,296
     46 -> 314,124,118
     47 -> 17,41,3,42,18
     59 -> 378,354
     60 -> 356,322
     61 -> 160,122
     63 -> 186*
     64 -> 130,106
     66 -> 374,114
     67 -> 273,163,41,17
     69 -> 59*
     83 -> 59*
     85 -> 222*
     86 -> 364,200
     87 -> 214,158,152
     89 -> 198*
     90 -> 218,150
     92 -> 338,108
     93 -> 41,45,3,17,21
     107 -> 85*
     109 -> 85*
     115 -> 59*
     119 -> 15*
     123 -> 39*
     125 -> 39*
     133 -> 394*
     136 -> 410*
     138 -> 404,332,324,294
     139 -> 277,273,163,167,45
     151 -> 85*
     153 -> 15*
     159 -> 39*
     163 -> 388*
     166 -> 402*
     168 -> 386,308,264
     169 -> 274,273,163,164,18,42
     183 -> 59*
     187 -> 484*
     188 -> 442*
     189 -> 270,228
     191 -> 423,262
     192 -> 242,238,234
     194 -> 434,370,226
     195 -> 273,163,17,41
     199 -> 187*
     201 -> 59*
     215 -> 161*
     219 -> 131*
     223 -> 187*
     227 -> 59*
     229 -> 161*
     235 -> 85*
     239 -> 131*
     250 -> 396*
     251 -> 277,167
     263 -> 187*
     265 -> 39*
     278 -> 380*
     279 -> 274,164
     291 -> 15*
     295 -> 15*
     297 -> 15*
     303 -> 39*
     307 -> 39*
     309 -> 161*
     315 -> 161*
     317 -> 161*
     323 -> 39*
     325 -> 85*
     331 -> 85*
     333 -> 131*
     339 -> 131*
     341 -> 131*
     347 -> 187*
     349 -> 39*
     355 -> 39*
     357 -> 187*
     363 -> 187*
     365 -> 187*
     371 -> 187*
     375 -> 131*
     379 -> 131*
     381 -> 271*
     387 -> 271*
     389 -> 271*
     395 -> 271*
     397 -> 243*
     403 -> 243*
     405 -> 243*
     411 -> 243*
     426 -> 464*
     429 -> 444*
     431 -> 272*
     435 -> 424*
     437 -> 131*
     443 -> 424*
     453 -> 277*
     473 -> 274*
     487 -> 511*
     490 -> 502*
     492 -> 466*
     510 -> 470*
     519 -> 467*
   problem:
    strict:
     
    weak:
     a(a(b(a(a(b(a(x1))))))) -> a(b(a(a(b(a(a(a(b(x1)))))))))
   Qed