YES

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:
 Polynomial Interpretation Processor:
  dimension: 1
  interpretation:
   [g](x0, x1) = 4x0 + x1 + 7,
   
   [f](x0, x1) = 3x0 + 3x1 + 7,
   
   [s](x0) = 2x0 + 1,
   
   [a] = 3
  orientation:
   s(a()) = 7 >= 3 = a()
   
   s(s(x)) = 4x + 3 >= x = x
   
   s(f(x,y)) = 6x + 6y + 15 >= 6x + 6y + 13 = f(s(y),s(x))
   
   s(g(x,y)) = 8x + 2y + 15 >= 8x + 2y + 12 = g(s(x),s(y))
   
   f(x,a()) = 3x + 16 >= x = x
   
   f(a(),y) = 3y + 16 >= y = y
   
   f(g(x,y),g(u,v)) = 12u + 3v + 12x + 3y + 49 >= 12u + 3v + 12x + 3y + 42 = g(f(x,u),f(y,v))
   
   g(a(),a()) = 22 >= 3 = a()
  problem:
   
  Qed