YES

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

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {2,1}
   transitions:
    b1(60) -> 61*
    b1(55) -> 56*
    b1(20) -> 21*
    b1(15) -> 16*
    b1(5) -> 6*
    b1(67) -> 68*
    b1(57) -> 58*
    b1(17) -> 18*
    b1(12) -> 13*
    b1(7) -> 8*
    b1(109) -> 110*
    b1(64) -> 65*
    b1(59) -> 60*
    b1(19) -> 20*
    b1(14) -> 15*
    b1(9) -> 10*
    b1(4) -> 5*
    b1(111) -> 112*
    b1(66) -> 67*
    b1(61) -> 62*
    b1(21) -> 22*
    b1(11) -> 12*
    b1(6) -> 7*
    b1(103) -> 104*
    b1(63) -> 64*
    b1(58) -> 59*
    b1(18) -> 19*
    b1(8) -> 9*
    b1(95) -> 96*
    a1(65) -> 66*
    a1(10) -> 11*
    a1(72) -> 73*
    a1(62) -> 63*
    a1(16) -> 17*
    a1(68) -> 69*
    a1(13) -> 14*
    b0(2) -> 1*
    b0(1) -> 1*
    a0(2) -> 2*
    a0(1) -> 2*
    1 -> 55*
    2 -> 4*
    6 -> 19,68,16,1,55
    9 -> 72*
    10 -> 109*
    16 -> 57*
    22 -> 20,56,6,5,1
    56 -> 5*
    62 -> 111*
    65 -> 103*
    68 -> 95*
    69 -> 18*
    73 -> 63*
    96 -> 5*
    104 -> 5*
    110 -> 6*
    112 -> 5*
  problem:
   
  Qed