YES(?,O(n^2))

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

Proof:
 RT Transformation Processor:
  strict:
   f(x,g(x)) -> x
   f(x,h(y)) -> f(h(x),y)
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [h](x0) = x0,
    
    [f](x0, x1) = x0 + x1 + 17,
    
    [g](x0) = x0 + 1
   orientation:
    f(x,g(x)) = 2x + 18 >= x = x
    
    f(x,h(y)) = x + y + 17 >= x + y + 17 = f(h(x),y)
   problem:
    strict:
     f(x,h(y)) -> f(h(x),y)
    weak:
     f(x,g(x)) -> x
   Matrix Interpretation Processor:
    dimension: 2
    interpretation:
                    [1]
     [h](x0) = x0 + [4],
     
                   [1 5]     [1 6]     [4 ]
     [f](x0, x1) = [0 1]x0 + [0 1]x1 + [13],
     
               [1 0]  
     [g](x0) = [0 0]x0
    orientation:
                 [1 5]    [1 6]    [29]    [1 5]    [1 6]    [25]            
     f(x,h(y)) = [0 1]x + [0 1]y + [17] >= [0 1]x + [0 1]y + [17] = f(h(x),y)
     
                 [2 5]    [4 ]         
     f(x,g(x)) = [0 1]x + [13] >= x = x
    problem:
     strict:
      
     weak:
      f(x,h(y)) -> f(h(x),y)
      f(x,g(x)) -> x
    Qed