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