YES(?,O(n^1))

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

Proof:
 Bounds Processor:
  bound: 3
  enrichment: match
  automaton:
   final states: {4}
   transitions:
    a3(127) -> 128*
    a3(122) -> 123*
    a3(87) -> 88*
    a3(82) -> 83*
    a3(126) -> 127*
    a3(121) -> 122*
    a3(86) -> 87*
    a3(81) -> 82*
    a1(22) -> 23*
    a1(17) -> 18*
    a1(23) -> 24*
    a1(18) -> 19*
    b3(80) -> 81*
    b3(125) -> 126*
    b3(120) -> 121*
    b3(85) -> 86*
    b1(21) -> 22*
    b1(16) -> 17*
    c3(129) -> 130*
    c3(124) -> 125*
    c3(119) -> 120*
    c3(84) -> 85*
    c3(79) -> 80*
    c3(151) -> 152*
    c3(123) -> 124*
    c3(83) -> 84*
    c3(145) -> 146*
    c1(20) -> 21*
    c1(15) -> 16*
    c1(19) -> 20*
    a2(77) -> 78*
    a2(72) -> 73*
    a2(57) -> 58*
    a2(52) -> 53*
    a2(32) -> 33*
    a2(27) -> 28*
    a2(76) -> 77*
    a2(71) -> 72*
    a2(56) -> 57*
    a2(51) -> 52*
    a2(33) -> 34*
    a2(28) -> 29*
    c0(4) -> 4*
    b2(75) -> 76*
    b2(70) -> 71*
    b2(55) -> 56*
    b2(50) -> 51*
    b2(31) -> 32*
    b2(26) -> 27*
    a0(4) -> 4*
    c2(30) -> 31*
    c2(25) -> 26*
    c2(89) -> 90*
    c2(74) -> 75*
    c2(69) -> 70*
    c2(54) -> 55*
    c2(49) -> 50*
    c2(29) -> 30*
    c2(143) -> 144*
    c2(103) -> 104*
    c2(73) -> 74*
    c2(53) -> 54*
    c2(105) -> 106*
    b0(4) -> 4*
    4 -> 15*
    22 -> 69*
    23 -> 25*
    24 -> 16,20,4
    32 -> 79*
    33 -> 49*
    34 -> 21,16,4,15,20
    56 -> 129*
    57 -> 103*
    58 -> 16,4,15,20,21
    76 -> 119*
    77 -> 89*
    78 -> 30*
    86 -> 145*
    87 -> 105*
    88 -> 54*
    90 -> 26*
    104 -> 26*
    106 -> 26*
    126 -> 151*
    127 -> 143*
    128 -> 30*
    130 -> 120*
    144 -> 26*
    146 -> 120*
    152 -> 120*
  problem:
   
  Qed