YES(?,O(n^1))
14.45/4.20	YES(?,O(n^1))
14.92/4.20	
14.92/4.20	Problem:
14.92/4.20	 half(0()) -> 0()
14.92/4.20	 half(s(s(x))) -> s(half(x))
14.92/4.20	 log(s(0())) -> 0()
14.92/4.20	 log(s(s(x))) -> s(log(s(half(x))))
14.92/4.20	
14.92/4.20	Proof:
14.92/4.20	 Complexity Transformation Processor:
14.92/4.20	  strict:
14.92/4.20	   half(0()) -> 0()
14.92/4.20	   half(s(s(x))) -> s(half(x))
14.92/4.20	   log(s(0())) -> 0()
14.92/4.20	   log(s(s(x))) -> s(log(s(half(x))))
14.92/4.20	  weak:
14.92/4.20	   
14.92/4.20	  Matrix Interpretation Processor: dim=1
14.92/4.20	   
14.92/4.20	   max_matrix:
14.92/4.20	    1
14.92/4.20	   interpretation:
14.92/4.20	    [log](x0) = x0 + 1,
14.92/4.20	    
14.92/4.20	    [s](x0) = x0 + 2,
14.92/4.20	    
14.92/4.20	    [half](x0) = x0 + 223,
14.92/4.20	    
14.92/4.20	    [0] = 71
14.92/4.20	   orientation:
14.92/4.20	    half(0()) = 294 >= 71 = 0()
14.92/4.20	    
14.92/4.20	    half(s(s(x))) = x + 227 >= x + 225 = s(half(x))
14.92/4.20	    
14.92/4.20	    log(s(0())) = 74 >= 71 = 0()
14.92/4.20	    
14.92/4.20	    log(s(s(x))) = x + 5 >= x + 228 = s(log(s(half(x))))
14.92/4.20	   problem:
14.92/4.20	    strict:
14.92/4.20	     log(s(s(x))) -> s(log(s(half(x))))
14.92/4.20	    weak:
14.92/4.20	     half(0()) -> 0()
14.92/4.20	     half(s(s(x))) -> s(half(x))
14.92/4.20	     log(s(0())) -> 0()
14.92/4.20	   Arctic Interpretation Processor:
14.92/4.20	    dimension: 2
14.92/4.20	    interpretation:
14.92/4.20	                 [3 0]  
14.92/4.20	     [log](x0) = [5 2]x0,
14.92/4.20	     
14.92/4.20	               [0 1]  
14.92/4.20	     [s](x0) = [5 0]x0,
14.92/4.20	     
14.92/4.20	                  [0  -&]  
14.92/4.20	     [half](x0) = [0  -&]x0,
14.92/4.20	     
14.92/4.20	           [2]
14.92/4.20	     [0] = [1]
14.92/4.20	    orientation:
14.92/4.20	                    [9  6 ]     [8  -&]                      
14.92/4.20	     log(s(s(x))) = [11 8 ]x >= [10 -&]x = s(log(s(half(x))))
14.92/4.20	     
14.92/4.20	                 [2]    [2]      
14.92/4.20	     half(0()) = [2] >= [1] = 0()
14.92/4.20	     
14.92/4.20	                     [6 1]     [1  -&]              
14.92/4.20	     half(s(s(x))) = [6 1]x >= [5  -&]x = s(half(x))
14.92/4.20	     
14.92/4.20	                   [7]    [2]      
14.92/4.20	     log(s(0())) = [9] >= [1] = 0()
14.92/4.20	    problem:
14.92/4.20	     strict:
14.92/4.20	      
14.92/4.20	     weak:
14.92/4.20	      log(s(s(x))) -> s(log(s(half(x))))
14.92/4.20	      half(0()) -> 0()
14.92/4.20	      half(s(s(x))) -> s(half(x))
14.92/4.20	      log(s(0())) -> 0()
14.92/4.20	    Qed
14.92/4.20	EOF