YES(?,O(n^1))

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:
    f3() -> 21*
    g3() -> 17*
    a4(27,26) -> 28*
    a4(25,13) -> 26*
    a4(25,15) -> 26*
    a4(25,23) -> 26*
    a4(25,28) -> 14*
    a4(25,32) -> 26*
    f4() -> 25*
    a0(4,4) -> 4*
    g4() -> 27*
    f0() -> 4*
    g0() -> 4*
    a1(4,6) -> 14,8,4
    a1(4,32) -> 15*
    a1(6,6) -> 14,8,4
    a1(6,8) -> 6*
    a1(23,6) -> 4*
    a1(13,6) -> 4*
    a1(4,7) -> 8*
    a1(4,9) -> 31*
    a1(4,13) -> 8*
    a1(15,6) -> 4*
    a1(32,6) -> 31,26,14,4,8,22
    a1(7,4) -> 8*
    a1(6,31) -> 32*
    f1() -> 4,7
    g1() -> 6*
    a2(23,9) -> 8*
    a2(13,9) -> 8*
    a2(13,13) -> 4*
    a2(13,15) -> 22,26,31,14,8,4
    a2(13,21) -> 29*
    a2(9,4) -> 15*
    a2(9,14) -> 15*
    a2(15,9) -> 8*
    a2(32,9) -> 31,26,14,4,8,22
    a2(13,4) -> 14*
    a2(13,6) -> 14*
    a2(13,30) -> 22*
    a2(13,32) -> 4*
    a2(9,29) -> 30*
    a2(6,9) -> 14,8
    f2() -> 13*
    g2() -> 9*
    a3(17,22) -> 23*
    a3(23,17) -> 14*
    a3(13,17) -> 14*
    a3(15,17) -> 14*
    a3(21,6) -> 22*
    a3(21,32) -> 22*
    a3(32,17) -> 14*
    a3(21,13) -> 22*
    a3(21,15) -> 22*
    a3(21,23) -> 31,22,4,26,14,8
  problem:
   
  Qed