YES(?,O(n^1))

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

Proof:
 Bounds Processor:
  bound: 5
  enrichment: match
  automaton:
   final states: {3}
   transitions:
    a3(162) -> 163*
    a3(152) -> 153*
    a3(117) -> 118*
    a3(87) -> 88*
    a3(199) -> 200*
    a3(169) -> 170*
    a3(149) -> 150*
    a3(119) -> 120*
    a3(89) -> 90*
    a3(201) -> 202*
    a3(171) -> 172*
    a3(161) -> 162*
    a3(151) -> 152*
    a3(153) -> 154*
    a3(118) -> 119*
    a3(88) -> 89*
    a3(200) -> 201*
    a3(170) -> 171*
    a3(160) -> 161*
    b4(232) -> 233*
    b4(197) -> 198*
    b4(239) -> 240*
    b4(234) -> 235*
    b4(224) -> 225*
    b4(179) -> 180*
    b4(241) -> 242*
    b4(196) -> 197*
    b4(181) -> 182*
    b4(233) -> 234*
    b4(223) -> 224*
    b4(240) -> 241*
    b4(225) -> 226*
    b4(195) -> 196*
    b4(180) -> 181*
    a4(237) -> 238*
    a4(222) -> 223*
    a4(192) -> 193*
    a4(177) -> 178*
    a4(229) -> 230*
    a4(194) -> 195*
    a4(236) -> 237*
    a4(231) -> 232*
    a4(221) -> 222*
    a4(176) -> 177*
    a4(238) -> 239*
    a4(193) -> 194*
    a4(178) -> 179*
    a4(230) -> 231*
    a4(220) -> 221*
    a0(3) -> 3*
    b5(254) -> 255*
    b5(253) -> 254*
    b5(255) -> 256*
    b0(3) -> 3*
    a5(252) -> 253*
    a5(251) -> 252*
    a5(250) -> 251*
    b1(15) -> 16*
    b1(22) -> 23*
    b1(14) -> 15*
    b1(21) -> 22*
    b1(16) -> 17*
    b1(23) -> 24*
    a1(20) -> 21*
    a1(67) -> 68*
    a1(27) -> 28*
    a1(12) -> 13*
    a1(69) -> 70*
    a1(19) -> 20*
    a1(11) -> 12*
    a1(18) -> 19*
    a1(13) -> 14*
    b2(50) -> 51*
    b2(45) -> 46*
    b2(127) -> 128*
    b2(107) -> 108*
    b2(82) -> 83*
    b2(52) -> 53*
    b2(129) -> 130*
    b2(44) -> 45*
    b2(106) -> 107*
    b2(81) -> 82*
    b2(51) -> 52*
    b2(128) -> 129*
    b2(108) -> 109*
    b2(83) -> 84*
    b2(43) -> 44*
    a2(40) -> 41*
    a2(47) -> 48*
    a2(42) -> 43*
    a2(124) -> 125*
    a2(104) -> 105*
    a2(79) -> 80*
    a2(49) -> 50*
    a2(126) -> 127*
    a2(41) -> 42*
    a2(138) -> 139*
    a2(103) -> 104*
    a2(78) -> 79*
    a2(63) -> 64*
    a2(48) -> 49*
    a2(125) -> 126*
    a2(105) -> 106*
    a2(85) -> 86*
    a2(80) -> 81*
    b3(202) -> 203*
    b3(172) -> 173*
    b3(122) -> 123*
    b3(92) -> 93*
    b3(204) -> 205*
    b3(174) -> 175*
    b3(164) -> 165*
    b3(154) -> 155*
    b3(156) -> 157*
    b3(121) -> 122*
    b3(91) -> 92*
    b3(203) -> 204*
    b3(173) -> 174*
    b3(163) -> 164*
    b3(165) -> 166*
    b3(155) -> 156*
    b3(120) -> 121*
    b3(90) -> 91*
    3 -> 11*
    14 -> 47*
    15 -> 40,18
    16 -> 27*
    17 -> 13,12,3
    21 -> 85*
    22 -> 67,63
    23 -> 69*
    24 -> 13,3,11,12
    28 -> 19*
    43 -> 117*
    44 -> 103,87
    45 -> 78*
    46 -> 48,14,13
    51 -> 124*
    53 -> 20*
    64 -> 41*
    68 -> 12*
    70 -> 12*
    82 -> 169,138
    84 -> 20,42
    86 -> 41*
    90 -> 220*
    92 -> 160*
    93 -> 50,49
    107 -> 149*
    109 -> 48*
    123 -> 80*
    128 -> 151*
    130 -> 86*
    139 -> 125*
    150 -> 88*
    154 -> 229*
    155 -> 192*
    156 -> 199*
    157 -> 43,117
    166 -> 126*
    173 -> 176*
    175 -> 118*
    182 -> 120*
    198 -> 119*
    203 -> 236*
    205 -> 89,105
    226 -> 162*
    235 -> 201*
    240 -> 250*
    242 -> 221*
    256 -> 223*
  problem:
   
  Qed