YES

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

Proof:
 Bounds Processor:
  bound: 3
  enrichment: match
  automaton:
   final states: {8,1}
   transitions:
    b1(15) -> 16*
    b1(27) -> 28*
    b1(17) -> 18*
    b1(59) -> 60*
    b1(71) -> 72*
    b1(26) -> 27*
    b1(73) -> 74*
    a1(55) -> 56*
    a1(25) -> 26*
    a1(37) -> 38*
    a1(29) -> 30*
    a1(31) -> 32*
    a1(16) -> 17*
    a1(28) -> 29*
    b2(42) -> 43*
    b2(119) -> 120*
    b2(109) -> 110*
    b2(99) -> 100*
    b2(84) -> 85*
    b2(79) -> 80*
    b2(101) -> 102*
    b2(61) -> 62*
    b2(41) -> 42*
    b2(83) -> 84*
    b2(63) -> 64*
    a2(40) -> 41*
    a2(97) -> 98*
    a2(82) -> 83*
    a2(62) -> 63*
    a2(44) -> 45*
    a2(39) -> 40*
    a2(111) -> 112*
    a2(86) -> 87*
    a2(81) -> 82*
    a2(43) -> 44*
    a2(100) -> 101*
    a2(85) -> 86*
    f20() -> 2*
    b3(127) -> 128*
    b3(129) -> 130*
    b3(113) -> 114*
    b3(115) -> 116*
    a0(7) -> 1*
    a0(2) -> 3*
    a0(9) -> 10*
    a0(6) -> 7*
    a0(3) -> 4*
    a3(114) -> 115*
    a3(128) -> 129*
    b0(10) -> 8*
    b0(5) -> 6*
    b0(2) -> 9*
    b0(4) -> 5*
    1 -> 38,3,10
    2 -> 73*
    5 -> 15*
    7 -> 31*
    8 -> 74,9,5
    9 -> 37*
    10 -> 71*
    15 -> 79*
    16 -> 39*
    17 -> 61,25
    18 -> 72,8
    27 -> 99*
    28 -> 97*
    29 -> 81,59
    30 -> 26,38,25,55,10
    32 -> 25*
    38 -> 25*
    42 -> 113*
    45 -> 26,63,38,25
    56 -> 41*
    59 -> 109*
    60 -> 8*
    64 -> 42,27
    72 -> 25*
    74 -> 25*
    80 -> 62*
    86 -> 119*
    87 -> 26*
    98 -> 40*
    99 -> 127*
    101 -> 111*
    102 -> 27,99,42,72
    110 -> 44*
    112 -> 83*
    116 -> 64,27,99,42
    120 -> 27,99
    130 -> 84*
  problem:
   
  Qed