Problem:
 a(f(),a(g(),a(f(),x))) -> a(f(),a(g(),a(g(),a(f(),x))))
 a(g(),a(f(),a(g(),x))) -> a(g(),a(f(),a(f(),a(g(),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