YES(?,O(n^1))

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

Proof:
 RT Transformation Processor:
  strict:
   b(a(b(a(c(b(a(x1))))))) -> a(b(a(c(b(b(a(b(a(c(x1))))))))))
  weak:
   
  Bounds Processor:
   bound: 3
   enrichment: match-rt
   automaton:
    final states: {4}
    transitions:
     a3(92) -> 93*
     a3(96) -> 97*
     a3(98) -> 99*
     a3(90) -> 91*
     a1(25) -> 26*
     a1(17) -> 18*
     a1(19) -> 20*
     a1(23) -> 24*
     b3(97) -> 98*
     b3(94) -> 95*
     b3(91) -> 92*
     b3(93) -> 94*
     b1(20) -> 21*
     b1(24) -> 25*
     b1(21) -> 22*
     b1(18) -> 19*
     c3(89) -> 90*
     c3(95) -> 96*
     c1(57) -> 58*
     c1(27) -> 28*
     c1(22) -> 23*
     c1(16) -> 17*
     a2(55) -> 56*
     a2(40) -> 41*
     a2(47) -> 48*
     a2(42) -> 43*
     a2(49) -> 50*
     a2(34) -> 35*
     a2(36) -> 37*
     a2(53) -> 54*
     b0(4) -> 4*
     b2(50) -> 51*
     b2(35) -> 36*
     b2(37) -> 38*
     b2(54) -> 55*
     b2(51) -> 52*
     b2(41) -> 42*
     b2(48) -> 49*
     b2(38) -> 39*
     a0(4) -> 4*
     c2(87) -> 88*
     c2(52) -> 53*
     c2(39) -> 40*
     c2(81) -> 82*
     c2(46) -> 47*
     c2(33) -> 34*
     c0(4) -> 4*
     4 -> 16*
     23 -> 46*
     25 -> 33,27
     26 -> 21,4
     28 -> 17*
     43 -> 22*
     53 -> 89,87
     55 -> 81,57
     56 -> 38,21
     58 -> 17*
     82 -> 34*
     88 -> 47*
     99 -> 38*
   problem:
    strict:
     
    weak:
     b(a(b(a(c(b(a(x1))))))) -> a(b(a(c(b(b(a(b(a(c(x1))))))))))
   Qed