YES(?,O(n^1))
64.38/17.43	YES(?,O(n^1))
64.38/17.43	
64.38/17.43	Problem:
64.38/17.43	 half(0()) -> 0()
64.38/17.43	 half(s(0())) -> 0()
64.38/17.43	 half(s(s(x))) -> s(half(x))
64.38/17.43	 s(log(0())) -> s(0())
64.38/17.43	 log(s(x)) -> s(log(half(s(x))))
64.38/17.43	
64.38/17.43	Proof:
64.38/17.43	 Complexity Transformation Processor:
64.38/17.43	  strict:
64.38/17.43	   half(0()) -> 0()
64.38/17.43	   half(s(0())) -> 0()
64.38/17.43	   half(s(s(x))) -> s(half(x))
64.38/17.43	   s(log(0())) -> s(0())
64.38/17.43	   log(s(x)) -> s(log(half(s(x))))
64.38/17.43	  weak:
64.38/17.43	   
64.38/17.43	  Matrix Interpretation Processor: dim=1
64.38/17.43	   
64.38/17.43	   max_matrix:
64.38/17.43	    1
64.38/17.43	   interpretation:
64.38/17.43	    [log](x0) = x0 + 248,
64.38/17.43	    
64.38/17.43	    [s](x0) = x0 + 20,
64.38/17.43	    
64.38/17.43	    [half](x0) = x0 + 44,
64.38/17.43	    
64.38/17.43	    [0] = 16
64.38/17.43	   orientation:
64.38/17.43	    half(0()) = 60 >= 16 = 0()
64.38/17.43	    
64.38/17.43	    half(s(0())) = 80 >= 16 = 0()
64.38/17.43	    
64.38/17.43	    half(s(s(x))) = x + 84 >= x + 64 = s(half(x))
64.38/17.43	    
64.38/17.43	    s(log(0())) = 284 >= 36 = s(0())
64.38/17.43	    
64.38/17.43	    log(s(x)) = x + 268 >= x + 332 = s(log(half(s(x))))
64.38/17.43	   problem:
64.38/17.43	    strict:
64.38/17.43	     log(s(x)) -> s(log(half(s(x))))
64.38/17.43	    weak:
64.38/17.43	     half(0()) -> 0()
64.38/17.43	     half(s(0())) -> 0()
64.38/17.43	     half(s(s(x))) -> s(half(x))
64.38/17.43	     s(log(0())) -> s(0())
64.38/17.43	   Arctic Interpretation Processor:
64.38/17.43	    dimension: 3
64.38/17.43	    interpretation:
64.38/17.43	                 [0 0 0]  
64.38/17.44	     [log](x0) = [1 0 3]x0
64.38/17.44	                 [0 1 1]  ,
64.38/17.44	     
64.38/17.44	               [0  -& 0 ]  
64.38/17.44	     [s](x0) = [0  0  2 ]x0
64.38/17.44	               [2  -& 1 ]  ,
64.38/17.44	     
64.38/17.44	                  [0  -& -&]  
64.38/17.44	     [half](x0) = [0  -& -&]x0
64.38/17.44	                  [0  -& -&]  ,
64.38/17.44	     
64.38/17.44	           [0 ]
64.38/17.44	     [0] = [-&]
64.38/17.44	           [-&]
64.38/17.44	    orientation:
64.38/17.44	                 [2 0 2]     [1  -& 1 ]                      
64.38/17.44	     log(s(x)) = [5 0 4]x >= [3  -& 3 ]x = s(log(half(s(x))))
64.38/17.44	                 [3 1 3]     [2  -& 2 ]                      
64.38/17.44	     
64.38/17.44	                 [0]    [0 ]      
64.38/17.44	     half(0()) = [0] >= [-&] = 0()
64.38/17.44	                 [0]    [-&]      
64.38/17.44	     
64.38/17.44	                    [0]    [0 ]      
64.38/17.44	     half(s(0())) = [0] >= [-&] = 0()
64.38/17.44	                    [0]    [-&]      
64.38/17.44	     
64.38/17.44	                     [2  -& 1 ]     [0  -& -&]              
64.38/17.44	     half(s(s(x))) = [2  -& 1 ]x >= [2  -& -&]x = s(half(x))
64.38/17.44	                     [2  -& 1 ]     [2  -& -&]              
64.38/17.44	     
64.38/17.44	                   [0]    [0]         
64.38/17.44	     s(log(0())) = [2] >= [0] = s(0())
64.38/17.44	                   [2]    [2]         
64.38/17.44	    problem:
64.38/17.44	     strict:
64.38/17.44	      
64.38/17.44	     weak:
64.38/17.44	      log(s(x)) -> s(log(half(s(x))))
64.38/17.44	      half(0()) -> 0()
64.38/17.44	      half(s(0())) -> 0()
64.38/17.44	      half(s(s(x))) -> s(half(x))
64.38/17.44	      s(log(0())) -> s(0())
64.38/17.44	    Qed
64.38/17.44	EOF