YES(O(1),O(n^2))
162.96/60.02	YES(O(1),O(n^2))
162.96/60.02	
162.96/60.02	We are left with following problem, upon which TcT provides the
162.96/60.02	certificate YES(O(1),O(n^2)).
162.96/60.02	
162.96/60.02	Strict Trs:
162.96/60.02	  { half(0()) -> 0()
162.96/60.02	  , half(s(s(x))) -> s(half(x))
162.96/60.02	  , log(s(0())) -> 0()
162.96/60.02	  , log(s(s(x))) -> s(log(s(half(x)))) }
162.96/60.02	Obligation:
162.96/60.02	  derivational complexity
162.96/60.02	Answer:
162.96/60.02	  YES(O(1),O(n^2))
162.96/60.02	
162.96/60.02	We use the processor 'matrix interpretation of dimension 1' to
162.96/60.02	orient following rules strictly.
162.96/60.02	
162.96/60.02	Trs: { log(s(0())) -> 0() }
162.96/60.02	
162.96/60.02	The induced complexity on above rules (modulo remaining rules) is
162.96/60.02	YES(?,O(n^1)) . These rules are moved into the corresponding weak
162.96/60.02	component(s).
162.96/60.02	
162.96/60.02	Sub-proof:
162.96/60.02	----------
162.96/60.02	  TcT has computed the following triangular matrix interpretation.
162.96/60.02	  
162.96/60.02	    [half](x1) = [1] x1 + [0]
162.96/60.02	                             
162.96/60.02	           [0] = [0]         
162.96/60.02	                             
162.96/60.02	       [s](x1) = [1] x1 + [0]
162.96/60.02	                             
162.96/60.02	     [log](x1) = [1] x1 + [1]
162.96/60.02	  
162.96/60.02	  The order satisfies the following ordering constraints:
162.96/60.02	  
162.96/60.02	        [half(0())] =  [0]                 
162.96/60.02	                    >= [0]                 
162.96/60.02	                    =  [0()]               
162.96/60.02	                                           
162.96/60.02	    [half(s(s(x)))] =  [1] x + [0]         
162.96/60.02	                    >= [1] x + [0]         
162.96/60.02	                    =  [s(half(x))]        
162.96/60.02	                                           
162.96/60.02	      [log(s(0()))] =  [1]                 
162.96/60.02	                    >  [0]                 
162.96/60.02	                    =  [0()]               
162.96/60.02	                                           
162.96/60.02	     [log(s(s(x)))] =  [1] x + [1]         
162.96/60.02	                    >= [1] x + [1]         
162.96/60.02	                    =  [s(log(s(half(x))))]
162.96/60.02	                                           
162.96/60.02	
162.96/60.02	We return to the main proof.
162.96/60.02	
162.96/60.02	We are left with following problem, upon which TcT provides the
162.96/60.02	certificate YES(O(1),O(n^2)).
162.96/60.02	
162.96/60.02	Strict Trs:
162.96/60.02	  { half(0()) -> 0()
162.96/60.02	  , half(s(s(x))) -> s(half(x))
162.96/60.02	  , log(s(s(x))) -> s(log(s(half(x)))) }
162.96/60.02	Weak Trs: { log(s(0())) -> 0() }
162.96/60.02	Obligation:
162.96/60.02	  derivational complexity
162.96/60.02	Answer:
162.96/60.02	  YES(O(1),O(n^2))
162.96/60.02	
162.96/60.02	We use the processor 'matrix interpretation of dimension 1' to
162.96/60.02	orient following rules strictly.
162.96/60.02	
162.96/60.02	Trs: { half(s(s(x))) -> s(half(x)) }
162.96/60.02	
162.96/60.02	The induced complexity on above rules (modulo remaining rules) is
162.96/60.02	YES(?,O(n^1)) . These rules are moved into the corresponding weak
162.96/60.02	component(s).
162.96/60.02	
162.96/60.02	Sub-proof:
162.96/60.02	----------
162.96/60.02	  TcT has computed the following triangular matrix interpretation.
162.96/60.02	  
162.96/60.02	    [half](x1) = [1] x1 + [0]
162.96/60.02	                             
162.96/60.02	           [0] = [1]         
162.96/60.02	                             
162.96/60.02	       [s](x1) = [1] x1 + [1]
162.96/60.02	                             
162.96/60.02	     [log](x1) = [1] x1 + [2]
162.96/60.02	  
162.96/60.02	  The order satisfies the following ordering constraints:
162.96/60.02	  
162.96/60.02	        [half(0())] =  [1]                 
162.96/60.02	                    >= [1]                 
162.96/60.02	                    =  [0()]               
162.96/60.02	                                           
162.96/60.02	    [half(s(s(x)))] =  [1] x + [2]         
162.96/60.02	                    >  [1] x + [1]         
162.96/60.02	                    =  [s(half(x))]        
162.96/60.02	                                           
162.96/60.02	      [log(s(0()))] =  [4]                 
162.96/60.02	                    >  [1]                 
162.96/60.02	                    =  [0()]               
162.96/60.02	                                           
162.96/60.02	     [log(s(s(x)))] =  [1] x + [4]         
162.96/60.02	                    >= [1] x + [4]         
162.96/60.02	                    =  [s(log(s(half(x))))]
162.96/60.02	                                           
162.96/60.02	
162.96/60.02	We return to the main proof.
162.96/60.02	
162.96/60.02	We are left with following problem, upon which TcT provides the
162.96/60.02	certificate YES(O(1),O(n^2)).
162.96/60.02	
162.96/60.02	Strict Trs:
162.96/60.02	  { half(0()) -> 0()
162.96/60.02	  , log(s(s(x))) -> s(log(s(half(x)))) }
162.96/60.02	Weak Trs:
162.96/60.02	  { half(s(s(x))) -> s(half(x))
162.96/60.02	  , log(s(0())) -> 0() }
162.96/60.02	Obligation:
162.96/60.02	  derivational complexity
162.96/60.02	Answer:
162.96/60.02	  YES(O(1),O(n^2))
162.96/60.02	
162.96/60.02	The weightgap principle applies (using the following nonconstant
162.96/60.02	growth matrix-interpretation)
162.96/60.02	
162.96/60.02	TcT has computed the following triangular matrix interpretation.
162.96/60.02	Note that the diagonal of the component-wise maxima of
162.96/60.02	interpretation-entries contains no more than 1 non-zero entries.
162.96/60.02	
162.96/60.02	  [half](x1) = [1] x1 + [1]
162.96/60.02	                           
162.96/60.02	         [0] = [0]         
162.96/60.02	                           
162.96/60.02	     [s](x1) = [1] x1 + [0]
162.96/60.02	                           
162.96/60.02	   [log](x1) = [1] x1 + [0]
162.96/60.02	
162.96/60.02	The order satisfies the following ordering constraints:
162.96/60.02	
162.96/60.02	      [half(0())] =  [1]                 
162.96/60.02	                  >  [0]                 
162.96/60.02	                  =  [0()]               
162.96/60.02	                                         
162.96/60.02	  [half(s(s(x)))] =  [1] x + [1]         
162.96/60.02	                  >= [1] x + [1]         
162.96/60.02	                  =  [s(half(x))]        
162.96/60.02	                                         
162.96/60.02	    [log(s(0()))] =  [0]                 
162.96/60.02	                  >= [0]                 
162.96/60.02	                  =  [0()]               
162.96/60.02	                                         
162.96/60.02	   [log(s(s(x)))] =  [1] x + [0]         
162.96/60.02	                  ?  [1] x + [1]         
162.96/60.02	                  =  [s(log(s(half(x))))]
162.96/60.02	                                         
162.96/60.02	
162.96/60.02	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
162.96/60.02	
162.96/60.02	We are left with following problem, upon which TcT provides the
162.96/60.02	certificate YES(O(1),O(n^2)).
162.96/60.02	
162.96/60.02	Strict Trs: { log(s(s(x))) -> s(log(s(half(x)))) }
162.96/60.02	Weak Trs:
162.96/60.02	  { half(0()) -> 0()
162.96/60.02	  , half(s(s(x))) -> s(half(x))
162.96/60.02	  , log(s(0())) -> 0() }
162.96/60.02	Obligation:
162.96/60.02	  derivational complexity
162.96/60.02	Answer:
162.96/60.02	  YES(O(1),O(n^2))
162.96/60.02	
162.96/60.02	We use the processor 'matrix interpretation of dimension 2' to
162.96/60.02	orient following rules strictly.
162.96/60.02	
162.96/60.02	Trs: { log(s(s(x))) -> s(log(s(half(x)))) }
162.96/60.02	
162.96/60.02	The induced complexity on above rules (modulo remaining rules) is
162.96/60.02	YES(?,O(n^2)) . These rules are moved into the corresponding weak
162.96/60.02	component(s).
162.96/60.02	
162.96/60.02	Sub-proof:
162.96/60.02	----------
162.96/60.02	  TcT has computed the following triangular matrix interpretation.
162.96/60.02	  
162.96/60.02	    [half](x1) = [1 0] x1 + [1]
162.96/60.02	                 [0 1]      [0]
162.96/60.02	                               
162.96/60.02	           [0] = [0]           
162.96/60.02	                 [2]           
162.96/60.02	                               
162.96/60.02	       [s](x1) = [1 0] x1 + [0]
162.96/60.02	                 [0 1]      [2]
162.96/60.02	                               
162.96/60.02	     [log](x1) = [1 1] x1 + [0]
162.96/60.02	                 [0 1]      [0]
162.96/60.02	  
162.96/60.02	  The order satisfies the following ordering constraints:
162.96/60.02	  
162.96/60.02	        [half(0())] =  [1]                 
162.96/60.02	                       [2]                 
162.96/60.02	                    >  [0]                 
162.96/60.02	                       [2]                 
162.96/60.02	                    =  [0()]               
162.96/60.02	                                           
162.96/60.02	    [half(s(s(x)))] =  [1 0] x + [1]       
162.96/60.02	                       [0 1]     [4]       
162.96/60.02	                    >= [1 0] x + [1]       
162.96/60.02	                       [0 1]     [2]       
162.96/60.02	                    =  [s(half(x))]        
162.96/60.02	                                           
162.96/60.02	      [log(s(0()))] =  [4]                 
162.96/60.02	                       [4]                 
162.96/60.02	                    >  [0]                 
162.96/60.02	                       [2]                 
162.96/60.02	                    =  [0()]               
162.96/60.02	                                           
162.96/60.02	     [log(s(s(x)))] =  [1 1] x + [4]       
162.96/60.02	                       [0 1]     [4]       
162.96/60.02	                    >  [1 1] x + [3]       
162.96/60.02	                       [0 1]     [4]       
162.96/60.02	                    =  [s(log(s(half(x))))]
162.96/60.02	                                           
162.96/60.02	
162.96/60.02	We return to the main proof.
162.96/60.02	
162.96/60.02	We are left with following problem, upon which TcT provides the
162.96/60.02	certificate YES(O(1),O(1)).
162.96/60.02	
162.96/60.02	Weak Trs:
162.96/60.02	  { half(0()) -> 0()
162.96/60.02	  , half(s(s(x))) -> s(half(x))
162.96/60.02	  , log(s(0())) -> 0()
162.96/60.02	  , log(s(s(x))) -> s(log(s(half(x)))) }
162.96/60.02	Obligation:
162.96/60.02	  derivational complexity
162.96/60.02	Answer:
162.96/60.02	  YES(O(1),O(1))
162.96/60.02	
162.96/60.02	Empty rules are trivially bounded
162.96/60.02	
162.96/60.02	Hurray, we answered YES(O(1),O(n^2))
162.96/60.02	EOF