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:
 Complexity 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
   max_matrix:
    1
    interpretation:
     [f](x0, x1) = x0 + x1,
     
     [h](x0) = x0,
     
     [minus](x0) = x0 + 1
    orientation:
     minus(minus(x)) = x + 2 >= x = x
     
     minus(h(x)) = x + 1 >= x + 1 = h(minus(x))
     
     minus(f(x,y)) = x + y + 1 >= x + y + 2 = 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
     max_matrix:
      [1 1]
      [0 1]
      interpretation:
                            
       [f](x0, x1) = x0 + x1,
       
                      [0]
       [h](x0) = x0 + [1],
       
                     [1 1]  
       [minus](x0) = [0 1]x0
      orientation:
                     [1 1]    [1]    [1 1]    [0]              
       minus(h(x)) = [0 1]x + [1] >= [0 1]x + [1] = h(minus(x))
       
                       [1 1]    [1 1]     [1 1]    [1 1]                        
       minus(f(x,y)) = [0 1]x + [0 1]y >= [0 1]x + [0 1]y = f(minus(y),minus(x))
       
                         [1 2]          
       minus(minus(x)) = [0 1]x >= x = x
      problem:
       strict:
        minus(f(x,y)) -> f(minus(y),minus(x))
       weak:
        minus(h(x)) -> h(minus(x))
        minus(minus(x)) -> x
      Matrix Interpretation Processor:
       dimension: 2
       max_matrix:
        [1 1]
        [0 1]
        interpretation:
                                 [0]
         [f](x0, x1) = x0 + x1 + [1],
         
                        [0]
         [h](x0) = x0 + [1],
         
                       [1 1]  
         [minus](x0) = [0 1]x0
        orientation:
                         [1 1]    [1 1]    [1]    [1 1]    [1 1]    [0]                       
         minus(f(x,y)) = [0 1]x + [0 1]y + [1] >= [0 1]x + [0 1]y + [1] = f(minus(y),minus(x))
         
                       [1 1]    [1]    [1 1]    [0]              
         minus(h(x)) = [0 1]x + [1] >= [0 1]x + [1] = h(minus(x))
         
                           [1 2]          
         minus(minus(x)) = [0 1]x >= x = x
        problem:
         strict:
          
         weak:
          minus(f(x,y)) -> f(minus(y),minus(x))
          minus(h(x)) -> h(minus(x))
          minus(minus(x)) -> x
        Qed