YES(?,O(n^1))

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

Proof:
 Bounds Processor:
  bound: 7
  enrichment: match
  automaton:
   final states: {4}
   transitions:
    c3(104) -> 105*
    b3(78) -> 79*
    b3(68) -> 69*
    b3(125) -> 126*
    a4(409) -> 410*
    a4(207) -> 208*
    a4(177) -> 178*
    a4(369) -> 370*
    a4(309) -> 310*
    a4(209) -> 210*
    a4(391) -> 392*
    a4(119) -> 120*
    a4(311) -> 312*
    a4(211) -> 212*
    a4(343) -> 344*
    a4(313) -> 314*
    a4(111) -> 112*
    a4(213) -> 214*
    a4(183) -> 184*
    a4(113) -> 114*
    a4(407) -> 408*
    a4(205) -> 206*
    a4(175) -> 176*
    a4(367) -> 368*
    a4(145) -> 146*
    a4(337) -> 338*
    b4(112) -> 113*
    b4(408) -> 409*
    b4(368) -> 369*
    b4(265) -> 266*
    b4(312) -> 313*
    a0(4) -> 4*
    c4(206) -> 207*
    b0(4) -> 4*
    a5(257) -> 258*
    a5(237) -> 238*
    a5(389) -> 390*
    a5(259) -> 260*
    a5(249) -> 250*
    a5(239) -> 240*
    a5(331) -> 332*
    a5(301) -> 302*
    a5(251) -> 252*
    a5(241) -> 242*
    a5(363) -> 364*
    a5(303) -> 304*
    a5(253) -> 254*
    a5(243) -> 244*
    a5(335) -> 336*
    a5(255) -> 256*
    c0(4) -> 4*
    c5(302) -> 303*
    a1(227) -> 228*
    a1(167) -> 168*
    a1(107) -> 108*
    a1(169) -> 170*
    a1(59) -> 60*
    a1(34) -> 35*
    a1(9) -> 10*
    a1(11) -> 12*
    b5(258) -> 259*
    b5(238) -> 239*
    b5(307) -> 308*
    c1(13) -> 14*
    a6(379) -> 380*
    a6(359) -> 360*
    a6(381) -> 382*
    a6(361) -> 362*
    a6(321) -> 322*
    a6(323) -> 324*
    a6(415) -> 416*
    a6(385) -> 386*
    a6(325) -> 326*
    a6(387) -> 388*
    a6(327) -> 328*
    b1(30) -> 31*
    b1(10) -> 11*
    b6(326) -> 327*
    b6(403) -> 404*
    b6(360) -> 361*
    b6(322) -> 323*
    a2(55) -> 56*
    a2(197) -> 198*
    a2(319) -> 320*
    a2(269) -> 270*
    a2(57) -> 58*
    a2(199) -> 200*
    a2(159) -> 160*
    a2(271) -> 272*
    a2(39) -> 40*
    a2(221) -> 222*
    a2(19) -> 20*
    a2(161) -> 162*
    a2(141) -> 142*
    a2(131) -> 132*
    a2(51) -> 52*
    a2(21) -> 22*
    a2(133) -> 134*
    a2(53) -> 54*
    a2(43) -> 44*
    c6(380) -> 381*
    b2(20) -> 21*
    b2(132) -> 133*
    b2(198) -> 199*
    b2(270) -> 271*
    b2(38) -> 39*
    b2(85) -> 86*
    a7(399) -> 400*
    a7(411) -> 412*
    a7(401) -> 402*
    a7(413) -> 414*
    c2(52) -> 53*
    b7(400) -> 401*
    b7(412) -> 413*
    a3(267) -> 268*
    a3(147) -> 148*
    a3(77) -> 78*
    a3(67) -> 68*
    a3(219) -> 220*
    a3(149) -> 150*
    a3(79) -> 80*
    a3(69) -> 70*
    a3(393) -> 394*
    a3(71) -> 72*
    a3(153) -> 154*
    a3(345) -> 346*
    a3(103) -> 104*
    a3(347) -> 348*
    a3(105) -> 106*
    a3(297) -> 298*
    4 -> 9*
    9 -> 43*
    10 -> 55,34,13
    11 -> 19*
    12 -> 39,44,38,11,10,30,13,4
    14 -> 11*
    19 -> 67*
    20 -> 107,103,57
    21 -> 71*
    22 -> 254,176,170,40,108,56,52,44,60,20,12,4,30,11,35,38,10,13
    30 -> 59,51
    31 -> 11*
    35 -> 13*
    40 -> 56,52,35
    44 -> 38*
    53 -> 77*
    54 -> 239,113,69,39,85,21,31
    56 -> 52*
    58 -> 52*
    60 -> 13*
    67 -> 175*
    68 -> 213,149
    69 -> 145,141
    70 -> 302,254,298,176,104,40,35,13,68,56,44,38,20,58
    71 -> 177*
    72 -> 68*
    77 -> 197,183
    78 -> 209,167,161,147
    79 -> 131,119
    80 -> 256,242,178,222,134,146,70,154,58,162,142,160,104,72,40,68,22
    85 -> 169,159,153
    86 -> 21*
    105 -> 269,111
    106 -> 239,113,133,69,125,21,39
    108 -> 13*
    111 -> 249*
    112 -> 301,297,205
    113 -> 237*
    114 ->
    348,302,254,298,256,242,178,212,176,220,214,210,146,148,70,58,20,44,38,40,103,150,112,72,104,68
    119 -> 243*
    120 -> 112*
    125 -> 227,221,219,211
    126 -> 79*
    134 -> 108*
    142 -> 132*
    145 -> 255*
    146 -> 112*
    148 -> 104*
    150 -> 104*
    154 -> 104*
    160 -> 52*
    162 -> 52*
    168 -> 13*
    170 -> 13*
    175 -> 253*
    176 -> 112*
    177 -> 241*
    178 -> 112*
    183 -> 251*
    184 -> 112*
    200 -> 168*
    207 -> 267,257
    208 -> 239,265,113,69
    210 -> 206*
    212 -> 206*
    214 -> 206*
    220 -> 104*
    222 -> 52*
    228 -> 13*
    240 -> 336,302,214
    242 -> 238*
    244 -> 238*
    250 -> 238*
    252 -> 238*
    254 -> 238*
    256 -> 238*
    257 -> 367,359
    258 -> 385,345,337,331
    259 -> 325,311
    260 -> 392,314,338,344,256,114,148,150,72,70,146
    265 -> 347,343,335
    266 -> 113*
    267 -> 319,309
    268 -> 78*
    272 -> 228*
    298 -> 104*
    303 -> 407,321
    304 -> 313,239,307,113
    307 -> 393,391,389,387
    308 -> 259*
    309 -> 363*
    310 -> 112*
    314 -> 298*
    320 -> 198*
    321 -> 411*
    322 -> 379*
    324 -> 390,388,240,302,214,238
    328 -> 302*
    332 -> 302*
    336 -> 302*
    338 -> 206*
    344 -> 206*
    346 -> 104*
    348 -> 104*
    362 -> 386,380,332
    364 -> 238*
    370 -> 346*
    381 -> 399*
    382 -> 403,327,239
    386 -> 380*
    388 -> 380*
    390 -> 302*
    392 -> 206*
    394 -> 104*
    402 -> 416,380,328
    403 -> 415*
    404 -> 323*
    410 -> 394*
    414 -> 380*
    416 -> 380*
  problem:
   
  Qed