YES(?,O(n^1))
Problem:
b(a(b(a(a(x1))))) -> a(a(a(b(a(b(a(b(x1))))))))
Proof:
Bounds Processor:
bound: 7
enrichment: match
automaton:
final states: {2,1}
transitions:
b3(167) -> 168*
b3(169) -> 170*
b3(134) -> 135*
b3(89) -> 90*
b3(191) -> 192*
b3(136) -> 137*
b3(116) -> 117*
b3(91) -> 92*
b3(178) -> 179*
b3(163) -> 164*
b3(138) -> 139*
b3(118) -> 119*
b3(295) -> 296*
b3(93) -> 94*
b3(165) -> 166*
b3(140) -> 141*
b3(120) -> 121*
a4(252) -> 253*
a4(247) -> 248*
a4(237) -> 238*
a4(232) -> 233*
a4(187) -> 188*
a4(314) -> 315*
a4(309) -> 310*
a4(304) -> 305*
a4(249) -> 250*
a4(234) -> 235*
a4(219) -> 220*
a4(214) -> 215*
a4(311) -> 312*
a4(306) -> 307*
a4(251) -> 252*
a4(236) -> 237*
a4(216) -> 217*
a4(186) -> 187*
a4(181) -> 182*
a4(313) -> 314*
a4(253) -> 254*
a4(238) -> 239*
a4(218) -> 219*
a4(183) -> 184*
a4(315) -> 316*
a4(305) -> 306*
a4(300) -> 301*
a4(220) -> 221*
a4(185) -> 186*
a4(302) -> 303*
b4(217) -> 218*
b4(399) -> 400*
b4(182) -> 183*
b4(299) -> 300*
b4(184) -> 185*
b4(326) -> 327*
b4(301) -> 302*
b4(246) -> 247*
b4(231) -> 232*
b4(328) -> 329*
b4(308) -> 309*
b4(303) -> 304*
b4(293) -> 294*
b4(248) -> 249*
b4(233) -> 234*
b4(213) -> 214*
b4(310) -> 311*
b4(250) -> 251*
b4(240) -> 241*
b4(235) -> 236*
b4(215) -> 216*
b4(180) -> 181*
b4(312) -> 313*
b4(297) -> 298*
b0(2) -> 1*
b0(1) -> 1*
a5(359) -> 360*
a5(344) -> 345*
a5(324) -> 325*
a5(289) -> 290*
a5(279) -> 280*
a5(274) -> 275*
a5(346) -> 347*
a5(336) -> 337*
a5(331) -> 332*
a5(276) -> 277*
a5(358) -> 359*
a5(353) -> 354*
a5(333) -> 334*
a5(323) -> 324*
a5(318) -> 319*
a5(288) -> 289*
a5(283) -> 284*
a5(278) -> 279*
a5(355) -> 356*
a5(345) -> 346*
a5(340) -> 341*
a5(335) -> 336*
a5(320) -> 321*
a5(285) -> 286*
a5(280) -> 281*
a5(357) -> 358*
a5(342) -> 343*
a5(337) -> 338*
a5(322) -> 323*
a5(287) -> 288*
a0(2) -> 2*
a0(1) -> 2*
b5(282) -> 283*
b5(277) -> 278*
b5(354) -> 355*
b5(339) -> 340*
b5(334) -> 335*
b5(319) -> 320*
b5(284) -> 285*
b5(401) -> 402*
b5(356) -> 357*
b5(341) -> 342*
b5(321) -> 322*
b5(286) -> 287*
b5(343) -> 344*
b5(273) -> 274*
b5(450) -> 451*
b5(330) -> 331*
b5(275) -> 276*
b5(352) -> 353*
b5(332) -> 333*
b5(317) -> 318*
a1(10) -> 11*
a1(5) -> 6*
a1(7) -> 8*
a1(9) -> 10*
a1(11) -> 12*
a6(459) -> 460*
a6(429) -> 430*
a6(424) -> 425*
a6(419) -> 420*
a6(379) -> 380*
a6(426) -> 427*
a6(421) -> 422*
a6(458) -> 459*
a6(453) -> 454*
a6(428) -> 429*
a6(378) -> 379*
a6(373) -> 374*
a6(455) -> 456*
a6(430) -> 431*
a6(420) -> 421*
a6(415) -> 416*
a6(375) -> 376*
a6(457) -> 458*
a6(417) -> 418*
a6(377) -> 378*
b1(35) -> 36*
b1(57) -> 58*
b1(59) -> 60*
b1(4) -> 5*
b1(31) -> 32*
b1(6) -> 7*
b1(8) -> 9*
b6(454) -> 455*
b6(414) -> 415*
b6(374) -> 375*
b6(456) -> 457*
b6(416) -> 417*
b6(376) -> 377*
b6(423) -> 424*
b6(418) -> 419*
b6(465) -> 466*
b6(425) -> 426*
b6(452) -> 453*
b6(427) -> 428*
b6(372) -> 373*
a2(75) -> 76*
a2(40) -> 41*
a2(77) -> 78*
a2(42) -> 43*
a2(79) -> 80*
a2(44) -> 45*
a2(78) -> 79*
a2(73) -> 74*
a2(43) -> 44*
a2(38) -> 39*
a7(474) -> 475*
a7(473) -> 474*
a7(468) -> 469*
a7(470) -> 471*
a7(472) -> 473*
b2(87) -> 88*
b2(72) -> 73*
b2(37) -> 38*
b2(74) -> 75*
b2(39) -> 40*
b2(81) -> 82*
b2(76) -> 77*
b2(41) -> 42*
b2(85) -> 86*
b7(469) -> 470*
b7(471) -> 472*
b7(467) -> 468*
a3(172) -> 173*
a3(142) -> 143*
a3(137) -> 138*
a3(122) -> 123*
a3(117) -> 118*
a3(92) -> 93*
a3(139) -> 140*
a3(119) -> 120*
a3(94) -> 95*
a3(171) -> 172*
a3(166) -> 167*
a3(141) -> 142*
a3(121) -> 122*
a3(96) -> 97*
a3(168) -> 169*
a3(143) -> 144*
a3(123) -> 124*
a3(170) -> 171*
a3(95) -> 96*
a3(90) -> 91*
1 -> 31*
2 -> 4*
9 -> 85*
10 -> 37*
11 -> 81,35
12 -> 5,7,1
32 -> 5*
36 -> 5*
42 -> 89*
43 -> 87,59
44 -> 163,72,57
45 -> 75,5,1,31,7
58 -> 5*
60 -> 5*
77 -> 165*
78 -> 134*
79 -> 116*
80 -> 38,9
82 -> 73*
86 -> 38*
88 -> 38*
94 -> 231*
96 -> 328,136
97 -> 139,7,75
121 -> 240*
122 -> 180*
123 -> 178*
124 -> 40,42
135 -> 117*
141 -> 293*
142 -> 297,295
143 -> 213,191
144 -> 9,85,42,135,88,60,7,5,40,38,117
164 -> 137*
170 -> 299*
172 -> 246*
173 -> 119*
179 -> 137*
188 -> 92*
192 -> 137*
218 -> 330*
219 -> 282*
220 -> 308*
221 -> 121*
236 -> 352*
238 -> 339,326
239 -> 249,216,139
241 -> 232*
251 -> 317*
253 -> 273*
254 -> 298,296,117,181
278 -> 450*
279 -> 401*
280 -> 399*
281 -> 121,240,185
290 -> 234*
294 -> 232*
296 -> 117*
298 -> 181*
307 -> 249*
316 -> 183*
322 -> 452*
324 -> 423*
325 -> 276*
327 -> 247*
329 -> 247*
338 -> 311*
344 -> 414*
346 -> 372*
347 -> 283*
360 -> 249,342
380 -> 287*
400 -> 309*
402 -> 283*
422 -> 375*
428 -> 467*
430 -> 465*
431 -> 402*
451 -> 331*
460 -> 426*
466 -> 373*
475 -> 375*
problem:
Qed