YES

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

Proof:
 Bounds Processor:
  bound: 4
  enrichment: match
  automaton:
   final states: {4}
   transitions:
    g2() -> 9*
    a3(18,15) -> 19*
    a3(16,8) -> 20*
    a3(18,6) -> 19*
    a3(18,20) -> 14,8
    a3(20,16) -> 14*
    a3(15,16) -> 14*
    a3(16,19) -> 20*
    f3() -> 18*
    g3() -> 16*
    a4(27,26) -> 28*
    a4(25,15) -> 26*
    a4(25,20) -> 26*
    a4(25,28) -> 14*
    a0(4,4) -> 4*
    f4() -> 25*
    g4() -> 27*
    f0() -> 4*
    g0() -> 4*
    a1(4,6) -> 14,8,4
    a1(6,6) -> 4*
    a1(6,8) -> 6*
    a1(4,7) -> 8*
    a1(4,13) -> 8*
    a1(20,6) -> 4*
    a1(15,6) -> 4*
    a1(7,4) -> 8*
    f1() -> 4,7
    g1() -> 6*
    a2(13,15) -> 14,8,4
    a2(9,14) -> 15*
    a2(20,9) -> 8*
    a2(15,9) -> 8*
    a2(13,4) -> 14*
    a2(13,18) -> 29*
    a2(13,20) -> 4*
    a2(13,30) -> 19*
    a2(9,29) -> 30*
    a2(6,9) -> 14,8
    f2() -> 13*
  problem:
   
  Qed