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