YES(?,O(1))
0.00/0.10	YES(?,O(1))
0.00/0.10	
0.00/0.10	We are left with following problem, upon which TcT provides the
0.00/0.10	certificate YES(?,O(1)).
0.00/0.10	
0.00/0.10	Strict Trs:
0.00/0.10	  { zeros() -> cons(0(), n__zeros())
0.00/0.10	  , zeros() -> n__zeros()
0.00/0.10	  , tail(cons(X, XS)) -> activate(XS)
0.00/0.10	  , activate(X) -> X
0.00/0.10	  , activate(n__zeros()) -> zeros() }
0.00/0.10	Obligation:
0.00/0.10	  runtime complexity
0.00/0.10	Answer:
0.00/0.10	  YES(?,O(1))
0.00/0.10	
0.00/0.10	The input is overlay and right-linear. Switching to innermost
0.00/0.10	rewriting.
0.00/0.10	
0.00/0.10	We are left with following problem, upon which TcT provides the
0.00/0.10	certificate YES(?,O(1)).
0.00/0.10	
0.00/0.10	Strict Trs:
0.00/0.10	  { zeros() -> cons(0(), n__zeros())
0.00/0.10	  , zeros() -> n__zeros()
0.00/0.10	  , tail(cons(X, XS)) -> activate(XS)
0.00/0.10	  , activate(X) -> X
0.00/0.10	  , activate(n__zeros()) -> zeros() }
0.00/0.10	Obligation:
0.00/0.10	  innermost runtime complexity
0.00/0.10	Answer:
0.00/0.10	  YES(?,O(1))
0.00/0.10	
0.00/0.10	The input was oriented with the instance of 'Small Polynomial Path
0.00/0.10	Order (PS,0-bounded)' as induced by the safe mapping
0.00/0.10	
0.00/0.10	 safe(zeros) = {}, safe(cons) = {1, 2}, safe(0) = {},
0.00/0.10	 safe(n__zeros) = {}, safe(tail) = {1}, safe(activate) = {1}
0.00/0.10	
0.00/0.10	and precedence
0.00/0.10	
0.00/0.10	 tail > zeros, tail > activate, activate > zeros .
0.00/0.10	
0.00/0.10	Following symbols are considered recursive:
0.00/0.10	
0.00/0.10	 {}
0.00/0.10	
0.00/0.10	The recursion depth is 0.
0.00/0.10	
0.00/0.10	For your convenience, here are the satisfied ordering constraints:
0.00/0.10	
0.00/0.10	                 zeros() > cons(; 0(),  n__zeros())
0.00/0.10	                                                   
0.00/0.10	                 zeros() > n__zeros()              
0.00/0.10	                                                   
0.00/0.10	  tail(; cons(; X,  XS)) > activate(; XS)          
0.00/0.10	                                                   
0.00/0.10	           activate(; X) > X                       
0.00/0.10	                                                   
0.00/0.10	  activate(; n__zeros()) > zeros()                 
0.00/0.10	                                                   
0.00/0.10	
0.00/0.10	Hurray, we answered YES(?,O(1))
0.00/0.10	EOF