YES

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

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {4,1}
   transitions:
    g0() -> 2*
    f0() -> 5*
    a1(12,3) -> 13*
    a1(12,15) -> 1,6
    a1(14,13) -> 15*
    f1() -> 12*
    g1() -> 14*
    f50() -> 3*
    a0(5,3) -> 6*
    a0(5,5) -> 6*
    a0(5,7) -> 1,4
    a0(3,2) -> 1*
    a0(2,6) -> 7*
    1 -> 6*
  problem:
   
  Qed