YES(?,O(n^2))
78.27/63.72	YES(?,O(n^2))
78.27/63.72	
78.27/63.72	Problem:
78.27/63.72	 *(x,*(minus(y),y)) -> *(minus(*(y,y)),x)
78.27/63.72	
78.27/63.72	Proof:
78.27/63.72	 Complexity Transformation Processor:
78.27/63.72	  strict:
78.27/63.72	   *(x,*(minus(y),y)) -> *(minus(*(y,y)),x)
78.27/63.72	  weak:
78.27/63.72	   
78.27/63.72	  Matrix Interpretation Processor: dim=2
78.27/63.72	   
78.27/63.72	   max_matrix:
78.27/63.72	    [1 1]
78.27/63.72	    [0 1]
78.27/63.72	   interpretation:
78.27/63.72	                  [1 1]     [1 1]  
78.27/63.72	    [*](x0, x1) = [0 1]x0 + [0 1]x1,
78.27/63.72	    
78.27/63.72	                  [1 0]     [0]
78.27/63.72	    [minus](x0) = [0 0]x0 + [1]
78.27/63.72	   orientation:
78.27/63.72	                         [1 1]    [2 2]    [2]    [1 1]    [2 2]    [1]                     
78.27/63.72	    *(x,*(minus(y),y)) = [0 1]x + [0 1]y + [1] >= [0 1]x + [0 0]y + [1] = *(minus(*(y,y)),x)
78.27/63.72	   problem:
78.27/63.72	    strict:
78.27/63.72	     
78.27/63.72	    weak:
78.27/63.72	     *(x,*(minus(y),y)) -> *(minus(*(y,y)),x)
78.27/63.72	   Qed
78.27/63.73	EOF