YES(?,O(n^1))

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

Proof:
 Bounds Processor:
  bound: 4
  enrichment: match
  automaton:
   final states: {3}
   transitions:
    b3(172) -> 173*
    b3(147) -> 148*
    b3(122) -> 123*
    b3(144) -> 145*
    b3(124) -> 125*
    b3(156) -> 157*
    b3(121) -> 122*
    b3(158) -> 159*
    b3(148) -> 149*
    b3(118) -> 119*
    b3(200) -> 201*
    b3(150) -> 151*
    a4(187) -> 188*
    a4(182) -> 183*
    a4(181) -> 182*
    a4(188) -> 189*
    a4(185) -> 186*
    b4(184) -> 185*
    b4(186) -> 187*
    b4(183) -> 184*
    b4(180) -> 181*
    b0(3) -> 3*
    a0(3) -> 3*
    a1(25) -> 26*
    a1(15) -> 16*
    a1(32) -> 33*
    a1(22) -> 23*
    a1(29) -> 30*
    a1(19) -> 20*
    a1(31) -> 32*
    a1(26) -> 27*
    a1(21) -> 22*
    a1(16) -> 17*
    b1(30) -> 31*
    b1(20) -> 21*
    b1(27) -> 28*
    b1(17) -> 18*
    b1(24) -> 25*
    b1(14) -> 15*
    b1(46) -> 47*
    b1(178) -> 179*
    b1(128) -> 129*
    b1(28) -> 29*
    b1(18) -> 19*
    a2(65) -> 66*
    a2(60) -> 61*
    a2(107) -> 108*
    a2(87) -> 88*
    a2(114) -> 115*
    a2(89) -> 90*
    a2(84) -> 85*
    a2(59) -> 60*
    a2(111) -> 112*
    a2(66) -> 67*
    a2(113) -> 114*
    a2(108) -> 109*
    a2(83) -> 84*
    a2(63) -> 64*
    a2(90) -> 91*
    b2(142) -> 143*
    b2(112) -> 113*
    b2(82) -> 83*
    b2(62) -> 63*
    b2(194) -> 195*
    b2(109) -> 110*
    b2(94) -> 95*
    b2(64) -> 65*
    b2(196) -> 197*
    b2(106) -> 107*
    b2(86) -> 87*
    b2(61) -> 62*
    b2(88) -> 89*
    b2(68) -> 69*
    b2(58) -> 59*
    b2(160) -> 161*
    b2(110) -> 111*
    b2(85) -> 86*
    a3(152) -> 153*
    a3(149) -> 150*
    a3(119) -> 120*
    a3(151) -> 152*
    a3(146) -> 147*
    a3(126) -> 127*
    a3(123) -> 124*
    a3(145) -> 146*
    a3(125) -> 126*
    a3(120) -> 121*
    3 -> 14*
    19 -> 82*
    22 -> 68,24
    23 -> 18,15,3
    29 -> 106*
    32 -> 58,46
    33 -> 18,3,14,15
    47 -> 15*
    63 -> 160*
    66 -> 128*
    67 -> 3,14,15,19
    69 -> 59*
    87 -> 118*
    90 -> 156,94
    91 -> 62,28
    95 -> 59*
    111 -> 172*
    114 -> 144,142
    115 -> 62,18
    123 -> 180*
    126 -> 158*
    127 -> 148,62
    129 -> 15*
    143 -> 59*
    149 -> 196*
    152 -> 178*
    153 -> 3,14,15,83
    157 -> 145*
    159 -> 145*
    161 -> 107*
    173 -> 119*
    179 -> 15*
    185 -> 200*
    188 -> 194*
    189 -> 148*
    195 -> 59*
    197 -> 107*
    201 -> 119*
  problem:
   
  Qed