YES(?,O(n^2))
10.22/6.68	YES(?,O(n^2))
10.22/6.68	
10.22/6.68	Problem:
10.22/6.68	 +(-(x,y),z) -> -(+(x,z),y)
10.22/6.68	 -(+(x,y),y) -> x
10.22/6.68	
10.22/6.68	Proof:
10.22/6.68	 Complexity Transformation Processor:
10.22/6.68	  strict:
10.22/6.68	   +(-(x,y),z) -> -(+(x,z),y)
10.22/6.68	   -(+(x,y),y) -> x
10.22/6.68	  weak:
10.22/6.68	   
10.22/6.68	  Matrix Interpretation Processor: dim=1
10.22/6.68	   
10.22/6.68	   max_matrix:
10.22/6.68	    1
10.22/6.68	   interpretation:
10.22/6.68	    [+](x0, x1) = x0 + x1 + 20,
10.22/6.68	    
10.22/6.68	    [-](x0, x1) = x0 + x1 + 129
10.22/6.68	   orientation:
10.22/6.68	    +(-(x,y),z) = x + y + z + 149 >= x + y + z + 149 = -(+(x,z),y)
10.22/6.68	    
10.22/6.68	    -(+(x,y),y) = x + 2y + 149 >= x = x
10.22/6.68	   problem:
10.22/6.68	    strict:
10.22/6.68	     +(-(x,y),z) -> -(+(x,z),y)
10.22/6.68	    weak:
10.22/6.68	     -(+(x,y),y) -> x
10.22/6.68	   Matrix Interpretation Processor: dim=2
10.22/6.68	    
10.22/6.68	    max_matrix:
10.22/6.68	     [1  16]
10.22/6.68	     [0  1 ]
10.22/6.68	    interpretation:
10.22/6.68	                   [1 3]     [1 4]     [0]
10.22/6.68	     [+](x0, x1) = [0 1]x0 + [0 1]x1 + [8],
10.22/6.68	     
10.22/6.68	                        [1  16]     [0]
10.22/6.68	     [-](x0, x1) = x0 + [0  0 ]x1 + [3]
10.22/6.68	    orientation:
10.22/6.68	                   [1 3]    [1  16]    [1 4]    [9 ]    [1 3]    [1  16]    [1 4]    [0 ]              
10.22/6.68	     +(-(x,y),z) = [0 1]x + [0  0 ]y + [0 1]z + [11] >= [0 1]x + [0  0 ]y + [0 1]z + [11] = -(+(x,z),y)
10.22/6.68	     
10.22/6.68	                   [1 3]    [2  20]    [0 ]         
10.22/6.68	     -(+(x,y),y) = [0 1]x + [0  1 ]y + [11] >= x = x
10.22/6.68	    problem:
10.22/6.68	     strict:
10.22/6.68	      
10.22/6.68	     weak:
10.22/6.68	      +(-(x,y),z) -> -(+(x,z),y)
10.22/6.68	      -(+(x,y),y) -> x
10.22/6.68	    Qed
10.22/6.68	EOF