YES(?,O(n^2))

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

Proof:
 RT Transformation Processor:
  strict:
   minus(minus(x)) -> x
   minus(h(x)) -> h(minus(x))
   minus(f(x,y)) -> f(minus(y),minus(x))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [f](x0, x1) = x0 + x1 + 19,
    
    [h](x0) = x0,
    
    [minus](x0) = x0 + 5
   orientation:
    minus(minus(x)) = x + 10 >= x = x
    
    minus(h(x)) = x + 5 >= x + 5 = h(minus(x))
    
    minus(f(x,y)) = x + y + 24 >= x + y + 29 = f(minus(y),minus(x))
   problem:
    strict:
     minus(h(x)) -> h(minus(x))
     minus(f(x,y)) -> f(minus(y),minus(x))
    weak:
     minus(minus(x)) -> x
   Matrix Interpretation Processor:
    dimension: 2
    interpretation:
                             [4 ]
     [f](x0, x1) = x0 + x1 + [12],
     
                    [1]
     [h](x0) = x0 + [0],
     
                   [1 2]  
     [minus](x0) = [0 1]x0
    orientation:
                   [1 2]    [1]    [1 2]    [1]              
     minus(h(x)) = [0 1]x + [0] >= [0 1]x + [0] = h(minus(x))
     
                     [1 2]    [1 2]    [28]    [1 2]    [1 2]    [4 ]                       
     minus(f(x,y)) = [0 1]x + [0 1]y + [12] >= [0 1]x + [0 1]y + [12] = f(minus(y),minus(x))
     
                       [1 4]          
     minus(minus(x)) = [0 1]x >= x = x
    problem:
     strict:
      minus(h(x)) -> h(minus(x))
     weak:
      minus(f(x,y)) -> f(minus(y),minus(x))
      minus(minus(x)) -> x
    Matrix Interpretation Processor:
     dimension: 2
     interpretation:
                              [4]
      [f](x0, x1) = x0 + x1 + [0],
      
                [1 2]     [0]
      [h](x0) = [0 1]x0 + [1],
      
                    [1 1]  
      [minus](x0) = [0 1]x0
     orientation:
                    [1 3]    [1]    [1 3]    [0]              
      minus(h(x)) = [0 1]x + [1] >= [0 1]x + [1] = h(minus(x))
      
                      [1 1]    [1 1]    [4]    [1 1]    [1 1]    [4]                       
      minus(f(x,y)) = [0 1]x + [0 1]y + [0] >= [0 1]x + [0 1]y + [0] = f(minus(y),minus(x))
      
                        [1 2]          
      minus(minus(x)) = [0 1]x >= x = x
     problem:
      strict:
       
      weak:
       minus(h(x)) -> h(minus(x))
       minus(f(x,y)) -> f(minus(y),minus(x))
       minus(minus(x)) -> x
     Qed