YES(?,O(n^1))

Problem:
 a(f(),a(f(),a(g(),a(g(),x)))) -> a(g(),a(g(),a(g(),a(f(),a(f(),a(f(),x))))))

Proof:
 Bounds Processor:
  bound: 0
  enrichment: match
  automaton:
   final states: {3}
   transitions:
    a0(1,2) -> 3*
    a0(2,1) -> 3*
    a0(1,1) -> 3*
    a0(2,2) -> 3*
    f0() -> 1*
    g0() -> 2*
  problem:
   
  Qed