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: 2
  enrichment: match
  automaton:
   final states: {3}
   transitions:
    a1(22) -> 23*
    a1(24) -> 25*
    a1(19) -> 20*
    a1(21) -> 22*
    a1(16) -> 17*
    b1(15) -> 16*
    b1(26) -> 27*
    b1(23) -> 24*
    b1(18) -> 19*
    c1(20) -> 21*
    c1(17) -> 18*
    a2(37) -> 38*
    a2(39) -> 40*
    a2(34) -> 35*
    a2(36) -> 37*
    a2(31) -> 32*
    c0(2) -> 3*
    c0(1) -> 3*
    b2(30) -> 31*
    b2(38) -> 39*
    b2(33) -> 34*
    a0(2) -> 1*
    a0(1) -> 1*
    c2(35) -> 36*
    c2(32) -> 33*
    b0(2) -> 2*
    b0(1) -> 2*
    1 -> 26*
    2 -> 15*
    24 -> 30*
    25 -> 18,3
    27 -> 16*
    40 -> 21*
  problem:
   
  Qed