YES(?,O(n^1))
Problem:
b(c(b(c(a(a(x1)))))) -> a(a(a(b(c(b(c(b(c(x1)))))))))
Proof:
Bounds Processor:
bound: 6
enrichment: match
automaton:
final states: {4}
transitions:
b3(182) -> 183*
b3(122) -> 123*
b3(214) -> 215*
b3(184) -> 185*
b3(124) -> 125*
b3(216) -> 217*
b3(136) -> 137*
b3(218) -> 219*
b3(138) -> 139*
b3(180) -> 181*
b3(140) -> 141*
b3(120) -> 121*
c3(257) -> 258*
c3(217) -> 218*
c3(551) -> 552*
c3(137) -> 138*
c3(299) -> 300*
c3(461) -> 462*
c3(179) -> 180*
c3(139) -> 140*
c3(119) -> 120*
c3(483) -> 484*
c3(271) -> 272*
c3(181) -> 182*
c3(161) -> 162*
c3(131) -> 132*
c3(121) -> 122*
c3(505) -> 506*
c3(243) -> 244*
c3(213) -> 214*
c3(183) -> 184*
c3(123) -> 124*
c3(215) -> 216*
c3(165) -> 166*
c3(559) -> 560*
c3(135) -> 136*
a4(349) -> 350*
a4(339) -> 340*
a4(319) -> 320*
a4(239) -> 240*
a4(241) -> 242*
a4(348) -> 349*
a4(338) -> 339*
a4(318) -> 319*
a4(240) -> 241*
a4(347) -> 348*
a4(337) -> 338*
a4(317) -> 318*
b4(344) -> 345*
b4(334) -> 335*
b4(314) -> 315*
b4(234) -> 235*
b4(346) -> 347*
b4(336) -> 337*
b4(316) -> 317*
b4(236) -> 237*
b4(238) -> 239*
b4(342) -> 343*
b4(332) -> 333*
b4(312) -> 313*
b0(4) -> 4*
c4(237) -> 238*
c4(379) -> 380*
c4(541) -> 542*
c4(381) -> 382*
c4(351) -> 352*
c4(341) -> 342*
c4(331) -> 332*
c4(311) -> 312*
c4(565) -> 566*
c4(555) -> 556*
c4(353) -> 354*
c4(343) -> 344*
c4(333) -> 334*
c4(313) -> 314*
c4(233) -> 234*
c4(567) -> 568*
c4(345) -> 346*
c4(335) -> 336*
c4(315) -> 316*
c4(507) -> 508*
c4(235) -> 236*
c4(367) -> 368*
c0(4) -> 4*
a5(454) -> 455*
a5(444) -> 445*
a5(516) -> 517*
a5(376) -> 377*
a5(538) -> 539*
a5(453) -> 454*
a5(443) -> 444*
a5(515) -> 516*
a5(455) -> 456*
a5(445) -> 446*
a5(375) -> 376*
a5(537) -> 538*
a5(517) -> 518*
a5(377) -> 378*
a5(539) -> 540*
a0(4) -> 4*
b5(374) -> 375*
b5(536) -> 537*
b5(448) -> 449*
b5(438) -> 439*
b5(510) -> 511*
b5(450) -> 451*
b5(440) -> 441*
b5(370) -> 371*
b5(532) -> 533*
b5(512) -> 513*
b5(452) -> 453*
b5(442) -> 443*
b5(372) -> 373*
b5(534) -> 535*
b5(514) -> 515*
a1(22) -> 23*
a1(21) -> 22*
a1(23) -> 24*
c5(489) -> 490*
c5(449) -> 450*
c5(439) -> 440*
c5(369) -> 370*
c5(561) -> 562*
c5(531) -> 532*
c5(511) -> 512*
c5(451) -> 452*
c5(441) -> 442*
c5(573) -> 574*
c5(371) -> 372*
c5(533) -> 534*
c5(513) -> 514*
c5(373) -> 374*
c5(535) -> 536*
c5(577) -> 578*
c5(557) -> 558*
c5(447) -> 448*
c5(437) -> 438*
c5(509) -> 510*
b1(20) -> 21*
b1(16) -> 17*
b1(18) -> 19*
a6(526) -> 527*
a6(525) -> 526*
a6(527) -> 528*
c1(429) -> 430*
c1(15) -> 16*
c1(147) -> 148*
c1(17) -> 18*
c1(39) -> 40*
c1(19) -> 20*
c1(203) -> 204*
c1(497) -> 498*
c1(73) -> 74*
c1(357) -> 358*
c1(499) -> 500*
b6(520) -> 521*
b6(522) -> 523*
b6(524) -> 525*
a2(60) -> 61*
a2(32) -> 33*
a2(84) -> 85*
a2(59) -> 60*
a2(61) -> 62*
a2(31) -> 32*
a2(83) -> 84*
a2(33) -> 34*
a2(85) -> 86*
c6(581) -> 582*
c6(521) -> 522*
c6(523) -> 524*
c6(519) -> 520*
b2(30) -> 31*
b2(82) -> 83*
b2(54) -> 55*
b2(56) -> 57*
b2(26) -> 27*
b2(78) -> 79*
b2(58) -> 59*
b2(28) -> 29*
b2(80) -> 81*
c2(55) -> 56*
c2(25) -> 26*
c2(117) -> 118*
c2(87) -> 88*
c2(481) -> 482*
c2(77) -> 78*
c2(57) -> 58*
c2(431) -> 432*
c2(27) -> 28*
c2(209) -> 210*
c2(503) -> 504*
c2(89) -> 90*
c2(79) -> 80*
c2(433) -> 434*
c2(29) -> 30*
c2(545) -> 546*
c2(111) -> 112*
c2(81) -> 82*
c2(53) -> 54*
c2(205) -> 206*
c2(549) -> 550*
c2(297) -> 298*
a3(187) -> 188*
a3(142) -> 143*
a3(127) -> 128*
a3(219) -> 220*
a3(221) -> 222*
a3(186) -> 187*
a3(141) -> 142*
a3(126) -> 127*
a3(143) -> 144*
a3(220) -> 221*
a3(185) -> 186*
a3(125) -> 126*
4 -> 15*
21 -> 77*
22 -> 25*
23 -> 39*
24 -> 17,19,4
31 -> 165,117
32 -> 131,53
33 -> 89,73
34 -> 79,21,17,4,15,19
40 -> 26*
59 -> 161*
60 -> 119,111
61 -> 87*
62 -> 79,17,4,15,19,21
74 -> 16*
83 -> 205*
84 -> 135*
85 -> 147*
86 -> 19,4,17,29
88 -> 78*
90 -> 78*
112 -> 26*
118 -> 26*
125 -> 311*
126 -> 381,271
127 -> 213*
128 -> 31,117,165,121,79,19,4,17,21,29,27,83,81
132 -> 120*
141 -> 299,297
142 -> 233,179
143 -> 209,203
144 -> 121,79,19,4,17,21,27
148 -> 16*
162 -> 120*
166 -> 120*
185 -> 353*
186 -> 331,257
187 -> 243*
188 -> 31,117,21,17,4,15,19,77,81,79,83,165
204 -> 16*
206 -> 26*
210 -> 78*
219 -> 431*
220 -> 351*
221 -> 357*
222 -> 123,57,19,4,17,29,139
239 -> 447*
240 -> 369*
241 -> 367*
242 -> 237,121,57,29,27,139,123,31,117,21,17,4,15,19,77,81,79,83,165,125
244 -> 214*
258 -> 120*
272 -> 120*
298 -> 26*
300 -> 120*
318 -> 461*
320 -> 217*
337 -> 549*
338 -> 509,341
339 -> 499*
340 -> 57,19,4,17,29,139,237,123
347 -> 483,481
348 -> 437,379
349 -> 433,429
350 -> 27,21,17,4,15,19,77,79,121,313
352 -> 342*
354 -> 312*
358 -> 16*
368 -> 332*
375 -> 577,555,551,545
376 -> 581,489
377 -> 565,505,503,497
378 -> 449,125,121,31,311,313,83,79,81,19,4,17,21,29,27,205,123,315
380 -> 234*
382 -> 234*
430 -> 16*
432 -> 26*
434 -> 78*
443 -> 531*
444 -> 557,541
445 -> 507*
446 -> 125,311,123,315,31,117,27,29,21,17,4,15,19,77,81,79,83,165,121,313,317
454 -> 559*
456 -> 335*
462 -> 120*
482 -> 26*
484 -> 120*
490 -> 438*
498 -> 16*
500 -> 16*
504 -> 78*
506 -> 214*
508 -> 234*
516 -> 519*
518 -> 449*
525 -> 573*
527 -> 567*
528 -> 453*
538 -> 561*
540 -> 237*
542 -> 234*
546 -> 26*
550 -> 26*
552 -> 120*
556 -> 312*
558 -> 438*
560 -> 120*
562 -> 510*
566 -> 332*
568 -> 234*
574 -> 532*
578 -> 448*
582 -> 520*
problem:
Qed