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