YES(?,O(n^2))

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

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