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: 1
  enrichment: match
  automaton:
   final states: {3}
   transitions:
    a1(4,2) -> 5*
    a1(4,4) -> 12*
    a1(6,12) -> 1*
    a1(4,1) -> 5*
    a1(4,7) -> 3*
    a1(6,5) -> 7*
    f1() -> 4*
    g1() -> 6*
    a0(1,2) -> 3*
    a0(2,1) -> 3*
    a0(1,1) -> 3*
    a0(2,2) -> 3*
    f0() -> 1*
    g0() -> 2*
  problem:
   
  Qed