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(172) -> 173*
    a3(157) -> 158*
    a3(142) -> 143*
    a3(92) -> 93*
    a3(199) -> 200*
    a3(149) -> 150*
    a3(139) -> 140*
    a3(94) -> 95*
    a3(201) -> 202*
    a3(171) -> 172*
    a3(156) -> 157*
    a3(141) -> 142*
    a3(173) -> 174*
    a3(148) -> 149*
    a3(143) -> 144*
    a3(93) -> 94*
    a3(200) -> 201*
    a3(155) -> 156*
    a3(150) -> 151*
    b4(232) -> 233*
    b4(197) -> 198*
    b4(182) -> 183*
    b4(239) -> 240*
    b4(234) -> 235*
    b4(219) -> 220*
    b4(241) -> 242*
    b4(196) -> 197*
    b4(181) -> 182*
    b4(233) -> 234*
    b4(218) -> 219*
    b4(183) -> 184*
    b4(240) -> 241*
    b4(220) -> 221*
    b4(195) -> 196*
    a4(237) -> 238*
    a4(217) -> 218*
    a4(192) -> 193*
    a4(229) -> 230*
    a4(194) -> 195*
    a4(179) -> 180*
    a4(236) -> 237*
    a4(231) -> 232*
    a4(216) -> 217*
    a4(238) -> 239*
    a4(193) -> 194*
    a4(178) -> 179*
    a4(230) -> 231*
    a4(215) -> 216*
    a4(180) -> 181*
    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(65) -> 66*
    a1(20) -> 21*
    a1(67) -> 68*
    a1(12) -> 13*
    a1(34) -> 35*
    a1(19) -> 20*
    a1(11) -> 12*
    a1(18) -> 19*
    a1(13) -> 14*
    b2(55) -> 56*
    b2(50) -> 51*
    b2(122) -> 123*
    b2(112) -> 113*
    b2(57) -> 58*
    b2(124) -> 125*
    b2(79) -> 80*
    b2(49) -> 50*
    b2(111) -> 112*
    b2(81) -> 82*
    b2(56) -> 57*
    b2(123) -> 124*
    b2(113) -> 114*
    b2(48) -> 49*
    b2(80) -> 81*
    a2(45) -> 46*
    a2(77) -> 78*
    a2(52) -> 53*
    a2(47) -> 48*
    a2(119) -> 120*
    a2(109) -> 110*
    a2(59) -> 60*
    a2(54) -> 55*
    a2(126) -> 127*
    a2(121) -> 122*
    a2(76) -> 77*
    a2(46) -> 47*
    a2(108) -> 109*
    a2(83) -> 84*
    a2(78) -> 79*
    a2(53) -> 54*
    a2(120) -> 121*
    a2(110) -> 111*
    b3(202) -> 203*
    b3(152) -> 153*
    b3(97) -> 98*
    b3(204) -> 205*
    b3(174) -> 175*
    b3(159) -> 160*
    b3(144) -> 145*
    b3(176) -> 177*
    b3(151) -> 152*
    b3(146) -> 147*
    b3(96) -> 97*
    b3(203) -> 204*
    b3(158) -> 159*
    b3(153) -> 154*
    b3(175) -> 176*
    b3(160) -> 161*
    b3(145) -> 146*
    b3(95) -> 96*
    3 -> 11*
    14 -> 52*
    15 -> 45,18
    16 -> 34*
    17 -> 13,12,3
    21 -> 83*
    22 -> 65,59
    23 -> 67*
    24 -> 13,3,11,12
    35 -> 19*
    48 -> 141*
    49 -> 108,92
    50 -> 76*
    51 -> 53,14,13
    56 -> 119*
    58 -> 20*
    60 -> 46*
    66 -> 12*
    68 -> 12*
    80 -> 171,126
    82 -> 20,47
    84 -> 46*
    95 -> 178*
    97 -> 155*
    98 -> 55,54
    112 -> 139*
    114 -> 53*
    123 -> 148*
    125 -> 84,46
    127 -> 120*
    140 -> 93*
    147 -> 78*
    151 -> 229*
    152 -> 215*
    153 -> 199*
    154 -> 48*
    161 -> 121*
    175 -> 192*
    177 -> 142*
    184 -> 157*
    198 -> 144*
    203 -> 236*
    205 -> 94,110
    221 -> 143*
    235 -> 201*
    240 -> 250*
    242 -> 179*
    256 -> 181*
  problem:
   
  Qed