YES(?,O(n^2))

Problem:
 -(-(neg(x),neg(x)),-(neg(y),neg(y))) -> -(-(x,y),-(x,y))

Proof:
 Complexity Transformation Processor:
  strict:
   -(-(neg(x),neg(x)),-(neg(y),neg(y))) -> -(-(x,y),-(x,y))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 2
   max_matrix:
    [1 1]
    [0 1]
    interpretation:
                   [1 1]       
     [-](x0, x1) = [0 0]x0 + x1,
     
                      [0]
     [neg](x0) = x0 + [1]
    orientation:
                                            [2 2]    [2 1]    [3]    [2 2]    [2 1]                    
     -(-(neg(x),neg(x)),-(neg(y),neg(y))) = [0 0]x + [0 1]y + [1] >= [0 0]x + [0 1]y = -(-(x,y),-(x,y))
    problem:
     strict:
      
     weak:
      -(-(neg(x),neg(x)),-(neg(y),neg(y))) -> -(-(x,y),-(x,y))
    Qed