YES(?,O(n^2))
9.71/6.22	YES(?,O(n^2))
9.71/6.22	
9.71/6.22	Problem:
9.71/6.22	 rev(a()) -> a()
9.71/6.22	 rev(b()) -> b()
9.71/6.22	 rev(++(x,y)) -> ++(rev(y),rev(x))
9.71/6.22	 rev(++(x,x)) -> rev(x)
9.71/6.22	
9.71/6.22	Proof:
9.71/6.22	 Complexity Transformation Processor:
9.71/6.22	  strict:
9.71/6.22	   rev(a()) -> a()
9.71/6.22	   rev(b()) -> b()
9.71/6.22	   rev(++(x,y)) -> ++(rev(y),rev(x))
9.71/6.22	   rev(++(x,x)) -> rev(x)
9.71/6.22	  weak:
9.71/6.22	   
9.71/6.22	  Matrix Interpretation Processor: dim=1
9.71/6.22	   
9.71/6.22	   max_matrix:
9.71/6.22	    1
9.71/6.22	   interpretation:
9.71/6.22	    [++](x0, x1) = x0 + x1 + 193,
9.71/6.22	    
9.71/6.22	    [b] = 30,
9.71/6.22	    
9.71/6.22	    [rev](x0) = x0 + 4,
9.71/6.22	    
9.71/6.22	    [a] = 32
9.71/6.22	   orientation:
9.71/6.22	    rev(a()) = 36 >= 32 = a()
9.71/6.22	    
9.71/6.22	    rev(b()) = 34 >= 30 = b()
9.71/6.22	    
9.71/6.22	    rev(++(x,y)) = x + y + 197 >= x + y + 201 = ++(rev(y),rev(x))
9.71/6.22	    
9.71/6.22	    rev(++(x,x)) = 2x + 197 >= x + 4 = rev(x)
9.71/6.22	   problem:
9.71/6.22	    strict:
9.71/6.22	     rev(++(x,y)) -> ++(rev(y),rev(x))
9.71/6.22	    weak:
9.71/6.22	     rev(a()) -> a()
9.71/6.22	     rev(b()) -> b()
9.71/6.22	     rev(++(x,x)) -> rev(x)
9.71/6.22	   Matrix Interpretation Processor: dim=4
9.71/6.22	    
9.71/6.22	    max_matrix:
9.71/6.22	     [1 1 0 1]
9.71/6.22	     [0 0 1 0]
9.71/6.22	     [0 0 0 0]
9.71/6.22	     [0 0 0 1]
9.71/6.22	    interpretation:
9.71/6.22	                    [1 1 0 0]     [1 1 0 0]     [0]
9.71/6.22	                    [0 0 0 0]     [0 0 1 0]     [0]
9.71/6.22	     [++](x0, x1) = [0 0 0 0]x0 + [0 0 0 0]x1 + [0]
9.71/6.22	                    [0 0 0 1]     [0 0 0 1]     [1],
9.71/6.22	     
9.71/6.22	           [1]
9.71/6.22	           [0]
9.71/6.22	     [b] = [0]
9.71/6.22	           [1],
9.71/6.22	     
9.71/6.22	                 [1 1 0 1]  
9.71/6.22	                 [0 0 0 0]  
9.71/6.22	     [rev](x0) = [0 0 0 0]x0
9.71/6.22	                 [0 0 0 1]  ,
9.71/6.22	     
9.71/6.22	           [1]
9.71/6.22	           [0]
9.71/6.22	     [a] = [0]
9.71/6.22	           [1]
9.71/6.22	    orientation:
9.71/6.22	                    [1 1 0 1]    [1 1 1 1]    [1]    [1 1 0 1]    [1 1 0 1]    [0]                    
9.71/6.22	                    [0 0 0 0]    [0 0 0 0]    [0]    [0 0 0 0]    [0 0 0 0]    [0]                    
9.71/6.22	     rev(++(x,y)) = [0 0 0 0]x + [0 0 0 0]y + [0] >= [0 0 0 0]x + [0 0 0 0]y + [0] = ++(rev(y),rev(x))
9.71/6.22	                    [0 0 0 1]    [0 0 0 1]    [1]    [0 0 0 1]    [0 0 0 1]    [1]                    
9.71/6.22	     
9.71/6.22	                [2]    [1]      
9.71/6.22	                [0]    [0]      
9.71/6.22	     rev(a()) = [0] >= [0] = a()
9.71/6.22	                [1]    [1]      
9.71/6.22	     
9.71/6.22	                [2]    [1]      
9.71/6.22	                [0]    [0]      
9.71/6.22	     rev(b()) = [0] >= [0] = b()
9.71/6.22	                [1]    [1]      
9.71/6.22	     
9.71/6.22	                    [2 2 1 2]    [1]    [1 1 0 1]          
9.71/6.22	                    [0 0 0 0]    [0]    [0 0 0 0]          
9.71/6.22	     rev(++(x,x)) = [0 0 0 0]x + [0] >= [0 0 0 0]x = rev(x)
9.71/6.22	                    [0 0 0 2]    [1]    [0 0 0 1]          
9.71/6.22	    problem:
9.71/6.22	     strict:
9.71/6.22	      
9.71/6.22	     weak:
9.71/6.22	      rev(++(x,y)) -> ++(rev(y),rev(x))
9.71/6.22	      rev(a()) -> a()
9.71/6.22	      rev(b()) -> b()
9.71/6.22	      rev(++(x,x)) -> rev(x)
9.71/6.22	    Qed
9.71/6.22	EOF