Problem:
 s(a()) -> a()
 s(s(x)) -> x
 s(f(x,y)) -> f(s(y),s(x))
 s(g(x,y)) -> g(s(x),s(y))
 f(x,a()) -> x
 f(a(),y) -> y
 f(g(x,y),g(u,v)) -> g(f(x,u),f(y,v))
 g(a(),a()) -> a()

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {4,3,2}
   transitions:
    a1() -> 4,2
    s0(1) -> 2*
    a0() -> 1*
    f0(1,1) -> 3*
    g0(1,1) -> 4*
    1 -> 3*
  problem:
   
  Qed