YES(?,O(n^2))

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

Proof:
 RT Transformation Processor:
  strict:
   g(f(x),y) -> f(h(x,y))
   h(x,y) -> g(x,f(y))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [h](x0, x1) = x0 + x1 + 31,
    
    [g](x0, x1) = x0 + x1 + 2,
    
    [f](x0) = x0
   orientation:
    g(f(x),y) = x + y + 2 >= x + y + 31 = f(h(x,y))
    
    h(x,y) = x + y + 31 >= x + y + 2 = g(x,f(y))
   problem:
    strict:
     g(f(x),y) -> f(h(x,y))
    weak:
     h(x,y) -> g(x,f(y))
   Matrix Interpretation Processor:
    dimension: 2
    interpretation:
                   [1 1]     [1 0]     [9]
     [h](x0, x1) = [0 1]x0 + [0 0]x1 + [0],
     
                   [1 1]     [1 0]     [3]
     [g](x0, x1) = [0 1]x0 + [0 0]x1 + [0],
     
                    [6]
     [f](x0) = x0 + [7]
    orientation:
                 [1 1]    [1 0]    [16]    [1 1]    [1 0]    [15]            
     g(f(x),y) = [0 1]x + [0 0]y + [7 ] >= [0 1]x + [0 0]y + [7 ] = f(h(x,y))
     
              [1 1]    [1 0]    [9]    [1 1]    [1 0]    [9]            
     h(x,y) = [0 1]x + [0 0]y + [0] >= [0 1]x + [0 0]y + [0] = g(x,f(y))
    problem:
     strict:
      
     weak:
      g(f(x),y) -> f(h(x,y))
      h(x,y) -> g(x,f(y))
    Qed