YES(?,O(n^2))
11.99/7.08	YES(?,O(n^2))
11.99/7.09	
11.99/7.09	Problem:
11.99/7.09	 *(i(x),x) -> 1()
11.99/7.09	 *(1(),y) -> y
11.99/7.09	 *(x,0()) -> 0()
11.99/7.09	 *(*(x,y),z) -> *(x,*(y,z))
11.99/7.09	
11.99/7.09	Proof:
11.99/7.09	 Complexity Transformation Processor:
11.99/7.09	  strict:
11.99/7.09	   *(i(x),x) -> 1()
11.99/7.09	   *(1(),y) -> y
11.99/7.09	   *(x,0()) -> 0()
11.99/7.09	   *(*(x,y),z) -> *(x,*(y,z))
11.99/7.09	  weak:
11.99/7.09	   
11.99/7.09	  Matrix Interpretation Processor: dim=1
11.99/7.09	   
11.99/7.09	   max_matrix:
11.99/7.09	    1
11.99/7.09	   interpretation:
11.99/7.09	    [0] = 254,
11.99/7.09	    
11.99/7.09	    [1] = 0,
11.99/7.09	    
11.99/7.09	    [*](x0, x1) = x0 + x1 + 2,
11.99/7.09	    
11.99/7.09	    [i](x0) = x0 + 4
11.99/7.09	   orientation:
11.99/7.09	    *(i(x),x) = 2x + 6 >= 0 = 1()
11.99/7.09	    
11.99/7.09	    *(1(),y) = y + 2 >= y = y
11.99/7.09	    
11.99/7.09	    *(x,0()) = x + 256 >= 254 = 0()
11.99/7.09	    
11.99/7.09	    *(*(x,y),z) = x + y + z + 4 >= x + y + z + 4 = *(x,*(y,z))
11.99/7.09	   problem:
11.99/7.09	    strict:
11.99/7.09	     *(*(x,y),z) -> *(x,*(y,z))
11.99/7.09	    weak:
11.99/7.09	     *(i(x),x) -> 1()
11.99/7.09	     *(1(),y) -> y
11.99/7.09	     *(x,0()) -> 0()
11.99/7.09	   Matrix Interpretation Processor: dim=2
11.99/7.09	    
11.99/7.09	    max_matrix:
11.99/7.09	     [1 1]
11.99/7.09	     [0 1]
11.99/7.09	    interpretation:
11.99/7.09	           [0]
11.99/7.09	     [0] = [1],
11.99/7.09	     
11.99/7.09	           [0]
11.99/7.09	     [1] = [2],
11.99/7.09	     
11.99/7.09	                   [1 1]          [0]
11.99/7.09	     [*](x0, x1) = [0 1]x0 + x1 + [2],
11.99/7.09	     
11.99/7.09	               [1 1]     [3]
11.99/7.09	     [i](x0) = [0 1]x0 + [1]
11.99/7.09	    orientation:
11.99/7.09	                   [1 2]    [1 1]        [2]    [1 1]    [1 1]        [0]              
11.99/7.09	     *(*(x,y),z) = [0 1]x + [0 1]y + z + [4] >= [0 1]x + [0 1]y + z + [4] = *(x,*(y,z))
11.99/7.09	     
11.99/7.09	                 [2 2]    [4]    [0]      
11.99/7.09	     *(i(x),x) = [0 2]x + [3] >= [2] = 1()
11.99/7.09	     
11.99/7.09	                    [2]         
11.99/7.09	     *(1(),y) = y + [4] >= y = y
11.99/7.09	     
11.99/7.09	                [1 1]    [0]    [0]      
11.99/7.09	     *(x,0()) = [0 1]x + [3] >= [1] = 0()
11.99/7.09	    problem:
11.99/7.09	     strict:
11.99/7.09	      
11.99/7.09	     weak:
11.99/7.09	      *(*(x,y),z) -> *(x,*(y,z))
11.99/7.09	      *(i(x),x) -> 1()
11.99/7.09	      *(1(),y) -> y
11.99/7.09	      *(x,0()) -> 0()
11.99/7.09	    Qed
11.99/7.09	EOF