YES(?,O(n^2))
14.09/7.66	YES(?,O(n^2))
14.09/7.67	
14.09/7.67	Problem:
14.09/7.67	 +(*(x,y),*(a(),y)) -> *(+(x,a()),y)
14.09/7.67	 *(*(x,y),z) -> *(x,*(y,z))
14.09/7.67	
14.09/7.67	Proof:
14.09/7.67	 Complexity Transformation Processor:
14.09/7.67	  strict:
14.09/7.67	   +(*(x,y),*(a(),y)) -> *(+(x,a()),y)
14.09/7.67	   *(*(x,y),z) -> *(x,*(y,z))
14.09/7.67	  weak:
14.09/7.67	   
14.09/7.67	  Matrix Interpretation Processor: dim=1
14.09/7.67	   
14.09/7.67	   max_matrix:
14.09/7.67	    1
14.09/7.67	   interpretation:
14.09/7.67	    [+](x0, x1) = x0 + x1 + 32,
14.09/7.67	    
14.09/7.67	    [a] = 224,
14.09/7.67	    
14.09/7.67	    [*](x0, x1) = x0 + x1 + 32
14.09/7.67	   orientation:
14.09/7.67	    +(*(x,y),*(a(),y)) = x + 2y + 320 >= x + y + 288 = *(+(x,a()),y)
14.09/7.67	    
14.09/7.67	    *(*(x,y),z) = x + y + z + 64 >= x + y + z + 64 = *(x,*(y,z))
14.09/7.67	   problem:
14.09/7.67	    strict:
14.09/7.67	     *(*(x,y),z) -> *(x,*(y,z))
14.09/7.67	    weak:
14.09/7.67	     +(*(x,y),*(a(),y)) -> *(+(x,a()),y)
14.09/7.67	   Matrix Interpretation Processor: dim=4
14.09/7.67	    
14.09/7.67	    max_matrix:
14.09/7.67	     [1 1 1 1]
14.09/7.67	     [0 1 0 1]
14.09/7.67	     [0 0 0 1]
14.09/7.67	     [0 0 0 0]
14.09/7.67	    interpretation:
14.09/7.67	                   [1 1 1 0]     [1 0 0 0]     [0]
14.09/7.67	                   [0 1 0 0]     [0 0 0 1]     [0]
14.09/7.67	     [+](x0, x1) = [0 0 0 1]x0 + [0 0 0 1]x1 + [0]
14.09/7.67	                   [0 0 0 0]     [0 0 0 0]     [1],
14.09/7.67	     
14.09/7.67	           [0]
14.09/7.67	           [0]
14.09/7.67	     [a] = [0]
14.09/7.67	           [0],
14.09/7.67	     
14.09/7.67	                   [1 1 1 1]     [1 0 1 0]     [0]
14.09/7.67	                   [0 1 0 1]     [0 1 0 1]     [1]
14.09/7.67	     [*](x0, x1) = [0 0 0 0]x0 + [0 0 0 0]x1 + [1]
14.09/7.67	                   [0 0 0 0]     [0 0 0 0]     [1]
14.09/7.67	    orientation:
14.09/7.67	                   [1 2 1 2]    [1 1 1 1]    [1 0 1 0]    [3]    [1 1 1 1]    [1 1 1 1]    [1 0 1 0]    [1]              
14.09/7.67	                   [0 1 0 1]    [0 1 0 1]    [0 1 0 1]    [3]    [0 1 0 1]    [0 1 0 1]    [0 1 0 1]    [3]              
14.09/7.67	     *(*(x,y),z) = [0 0 0 0]x + [0 0 0 0]y + [0 0 0 0]z + [1] >= [0 0 0 0]x + [0 0 0 0]y + [0 0 0 0]z + [1] = *(x,*(y,z))
14.09/7.67	                   [0 0 0 0]    [0 0 0 0]    [0 0 0 0]    [1]    [0 0 0 0]    [0 0 0 0]    [0 0 0 0]    [1]              
14.09/7.67	     
14.09/7.67	                          [1 2 1 2]    [2 1 2 1]    [2]    [1 2 1 1]    [1 0 1 0]    [1]                
14.09/7.67	                          [0 1 0 1]    [0 1 0 1]    [2]    [0 1 0 0]    [0 1 0 1]    [2]                
14.09/7.67	     +(*(x,y),*(a(),y)) = [0 0 0 0]x + [0 0 0 0]y + [2] >= [0 0 0 0]x + [0 0 0 0]y + [1] = *(+(x,a()),y)
14.09/7.67	                          [0 0 0 0]    [0 0 0 0]    [1]    [0 0 0 0]    [0 0 0 0]    [1]                
14.09/7.67	    problem:
14.09/7.67	     strict:
14.09/7.67	      
14.09/7.67	     weak:
14.09/7.67	      *(*(x,y),z) -> *(x,*(y,z))
14.09/7.67	      +(*(x,y),*(a(),y)) -> *(+(x,a()),y)
14.09/7.67	    Qed
14.09/7.67	EOF