YES(?,O(n^1))

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

Proof:
 Bounds Processor:
  bound: 2
  enrichment: match
  automaton:
   final states: {3}
   transitions:
    b1(8) -> 9*
    a1(7) -> 8*
    b2(11) -> 12*
    a0(3) -> 3*
    a2(10) -> 11*
    b0(3) -> 3*
    3 -> 7*
    7 -> 10*
    9 -> 3*
    12 -> 11,8
  problem:
   
  Qed