YES(?,O(n^1))

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

Proof:
 Bounds Processor:
  bound: 3
  enrichment: match
  automaton:
   final states: {4}
   transitions:
    a3(117) -> 118*
    a3(112) -> 113*
    a3(94) -> 95*
    a3(96) -> 97*
    a3(91) -> 92*
    a3(118) -> 119*
    a3(93) -> 94*
    a3(88) -> 89*
    a3(120) -> 121*
    a3(115) -> 116*
    a1(25) -> 26*
    a1(20) -> 21*
    a1(22) -> 23*
    a1(17) -> 18*
    a1(23) -> 24*
    b3(87) -> 88*
    b3(119) -> 120*
    b3(114) -> 115*
    b3(111) -> 112*
    b3(98) -> 99*
    b3(95) -> 96*
    b3(90) -> 91*
    b1(27) -> 28*
    b1(24) -> 25*
    b1(19) -> 20*
    b1(16) -> 17*
    b1(33) -> 34*
    c3(92) -> 93*
    c3(89) -> 90*
    c3(116) -> 117*
    c3(113) -> 114*
    c1(21) -> 22*
    c1(18) -> 19*
    a2(70) -> 71*
    a2(72) -> 73*
    a2(67) -> 68*
    a2(42) -> 43*
    a2(69) -> 70*
    a2(64) -> 65*
    a2(44) -> 45*
    a2(39) -> 40*
    a2(41) -> 42*
    a2(36) -> 37*
    c0(4) -> 4*
    b2(50) -> 51*
    b2(35) -> 36*
    b2(71) -> 72*
    b2(66) -> 67*
    b2(63) -> 64*
    b2(43) -> 44*
    b2(38) -> 39*
    a0(4) -> 4*
    c2(65) -> 66*
    c2(40) -> 41*
    c2(37) -> 38*
    c2(68) -> 69*
    b0(4) -> 4*
    4 -> 16*
    22 -> 50*
    23 -> 27*
    25 -> 35,33
    26 -> 19,4
    28 -> 17*
    34 -> 17*
    44 -> 98,63
    45 -> 22,19
    51 -> 36*
    72 -> 87*
    73 -> 22*
    96 -> 111*
    97 -> 38*
    99 -> 88*
    121 -> 41*
  problem:
   
  Qed