YES(?,O(n^2))
9.78/6.51	YES(?,O(n^2))
9.78/6.52	
9.78/6.52	Problem:
9.78/6.52	 f(+(x,0())) -> f(x)
9.78/6.52	 +(x,+(y,z)) -> +(+(x,y),z)
9.78/6.52	
9.78/6.52	Proof:
9.78/6.52	 Complexity Transformation Processor:
9.78/6.52	  strict:
9.78/6.52	   f(+(x,0())) -> f(x)
9.78/6.52	   +(x,+(y,z)) -> +(+(x,y),z)
9.78/6.52	  weak:
9.78/6.52	   
9.78/6.52	  Matrix Interpretation Processor: dim=1
9.78/6.52	   
9.78/6.52	   max_matrix:
9.78/6.52	    1
9.78/6.52	   interpretation:
9.78/6.52	    [f](x0) = x0 + 24,
9.78/6.52	    
9.78/6.52	    [+](x0, x1) = x0 + x1 + 2,
9.78/6.52	    
9.78/6.52	    [0] = 63
9.78/6.52	   orientation:
9.78/6.52	    f(+(x,0())) = x + 89 >= x + 24 = f(x)
9.78/6.52	    
9.78/6.52	    +(x,+(y,z)) = x + y + z + 4 >= x + y + z + 4 = +(+(x,y),z)
9.78/6.52	   problem:
9.78/6.52	    strict:
9.78/6.52	     +(x,+(y,z)) -> +(+(x,y),z)
9.78/6.52	    weak:
9.78/6.52	     f(+(x,0())) -> f(x)
9.78/6.52	   Matrix Interpretation Processor: dim=4
9.78/6.52	    
9.78/6.52	    max_matrix:
9.78/6.52	     [1 1 0 1]
9.78/6.52	     [0 1 0 0]
9.78/6.52	     [0 0 0 0]
9.78/6.52	     [0 0 0 0]
9.78/6.52	    interpretation:
9.78/6.52	               [1 0 0 0]     [0]
9.78/6.52	               [0 1 0 0]     [0]
9.78/6.52	     [f](x0) = [0 0 0 0]x0 + [0]
9.78/6.52	               [0 0 0 0]     [1],
9.78/6.52	     
9.78/6.52	                   [1 0 0 1]     [1 1 0 0]     [1]
9.78/6.52	                   [0 1 0 0]     [0 1 0 0]     [1]
9.78/6.52	     [+](x0, x1) = [0 0 0 0]x0 + [0 0 0 0]x1 + [0]
9.78/6.52	                   [0 0 0 0]     [0 0 0 0]     [0],
9.78/6.52	     
9.78/6.52	           [1]
9.78/6.52	           [0]
9.78/6.52	     [0] = [0]
9.78/6.52	           [0]
9.78/6.52	    orientation:
9.78/6.52	                   [1 0 0 1]    [1 1 0 1]    [1 2 0 0]    [3]    [1 0 0 1]    [1 1 0 0]    [1 1 0 0]    [2]              
9.78/6.52	                   [0 1 0 0]    [0 1 0 0]    [0 1 0 0]    [2]    [0 1 0 0]    [0 1 0 0]    [0 1 0 0]    [2]              
9.78/6.52	     +(x,+(y,z)) = [0 0 0 0]x + [0 0 0 0]y + [0 0 0 0]z + [0] >= [0 0 0 0]x + [0 0 0 0]y + [0 0 0 0]z + [0] = +(+(x,y),z)
9.78/6.52	                   [0 0 0 0]    [0 0 0 0]    [0 0 0 0]    [0]    [0 0 0 0]    [0 0 0 0]    [0 0 0 0]    [0]              
9.78/6.52	     
9.78/6.52	                   [1 0 0 1]    [2]    [1 0 0 0]    [0]       
9.78/6.52	                   [0 1 0 0]    [1]    [0 1 0 0]    [0]       
9.78/6.52	     f(+(x,0())) = [0 0 0 0]x + [0] >= [0 0 0 0]x + [0] = f(x)
9.78/6.52	                   [0 0 0 0]    [1]    [0 0 0 0]    [1]       
9.78/6.52	    problem:
9.78/6.52	     strict:
9.78/6.52	      
9.78/6.52	     weak:
9.78/6.52	      +(x,+(y,z)) -> +(+(x,y),z)
9.78/6.52	      f(+(x,0())) -> f(x)
9.78/6.52	    Qed
9.78/6.52	EOF