YES(?,O(n^2))

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

Proof:
 RT Transformation Processor:
  strict:
   f(x,a()) -> x
   f(x,g(y)) -> f(g(x),y)
  weak:
   
  Bounds Processor:
   bound: 0
   enrichment: match-rt
   automaton:
    final states: {4,5}
    transitions:
     f0(4,4) -> 4*
     f0(5,5) -> 4*
     f0(4,5) -> 4*
     f0(5,4) -> 4*
     a0() -> 5*
     g0(5) -> 4*
     g0(4) -> 4*
     5 -> 4*
   problem:
    strict:
     f(x,g(y)) -> f(g(x),y)
    weak:
     f(x,a()) -> x
   Matrix Interpretation Processor:
    dimension: 2
    interpretation:
                    [5]
     [g](x0) = x0 + [3],
     
                   [1 1]     [1 8]     [0 ]
     [f](x0, x1) = [0 1]x0 + [0 1]x1 + [12],
     
           [0]
     [a] = [0]
    orientation:
                 [1 1]    [1 8]    [29]    [1 1]    [1 8]    [8 ]            
     f(x,g(y)) = [0 1]x + [0 1]y + [15] >= [0 1]x + [0 1]y + [15] = f(g(x),y)
     
                [1 1]    [0 ]         
     f(x,a()) = [0 1]x + [12] >= x = x
    problem:
     strict:
      
     weak:
      f(x,g(y)) -> f(g(x),y)
      f(x,a()) -> x
    Qed