YES(?,O(1))
0.00/0.40	YES(?,O(1))
0.00/0.40	
0.00/0.40	We are left with following problem, upon which TcT provides the
0.00/0.40	certificate YES(?,O(1)).
0.00/0.40	
0.00/0.40	Strict Trs:
0.00/0.40	  { terms(N) -> cons(recip(sqr(N)), n__terms(s(N)))
0.00/0.40	  , terms(X) -> n__terms(X)
0.00/0.40	  , sqr(s(X)) -> s(n__add(sqr(activate(X)), dbl(activate(X))))
0.00/0.40	  , sqr(0()) -> 0()
0.00/0.40	  , s(X) -> n__s(X)
0.00/0.40	  , activate(X) -> X
0.00/0.40	  , activate(n__terms(X)) -> terms(X)
0.00/0.40	  , activate(n__add(X1, X2)) -> add(X1, X2)
0.00/0.40	  , activate(n__s(X)) -> s(X)
0.00/0.40	  , activate(n__dbl(X)) -> dbl(X)
0.00/0.40	  , activate(n__first(X1, X2)) -> first(X1, X2)
0.00/0.40	  , dbl(X) -> n__dbl(X)
0.00/0.40	  , dbl(s(X)) -> s(n__s(n__dbl(activate(X))))
0.00/0.40	  , dbl(0()) -> 0()
0.00/0.40	  , add(X1, X2) -> n__add(X1, X2)
0.00/0.40	  , add(s(X), Y) -> s(n__add(activate(X), Y))
0.00/0.40	  , add(0(), X) -> X
0.00/0.40	  , first(X1, X2) -> n__first(X1, X2)
0.00/0.40	  , first(s(X), cons(Y, Z)) ->
0.00/0.40	    cons(Y, n__first(activate(X), activate(Z)))
0.00/0.40	  , first(0(), X) -> nil() }
0.00/0.40	Obligation:
0.00/0.40	  innermost runtime complexity
0.00/0.40	Answer:
0.00/0.40	  YES(?,O(1))
0.00/0.40	
0.00/0.40	Arguments of following rules are not normal-forms:
0.00/0.40	
0.00/0.40	{ sqr(s(X)) -> s(n__add(sqr(activate(X)), dbl(activate(X))))
0.00/0.40	, dbl(s(X)) -> s(n__s(n__dbl(activate(X))))
0.00/0.40	, add(s(X), Y) -> s(n__add(activate(X), Y))
0.00/0.40	, first(s(X), cons(Y, Z)) ->
0.00/0.40	  cons(Y, n__first(activate(X), activate(Z))) }
0.00/0.40	
0.00/0.40	All above mentioned rules can be savely removed.
0.00/0.40	
0.00/0.40	We are left with following problem, upon which TcT provides the
0.00/0.40	certificate YES(?,O(1)).
0.00/0.40	
0.00/0.40	Strict Trs:
0.00/0.40	  { terms(N) -> cons(recip(sqr(N)), n__terms(s(N)))
0.00/0.40	  , terms(X) -> n__terms(X)
0.00/0.40	  , sqr(0()) -> 0()
0.00/0.40	  , s(X) -> n__s(X)
0.00/0.40	  , activate(X) -> X
0.00/0.40	  , activate(n__terms(X)) -> terms(X)
0.00/0.40	  , activate(n__add(X1, X2)) -> add(X1, X2)
0.00/0.40	  , activate(n__s(X)) -> s(X)
0.00/0.40	  , activate(n__dbl(X)) -> dbl(X)
0.00/0.40	  , activate(n__first(X1, X2)) -> first(X1, X2)
0.00/0.40	  , dbl(X) -> n__dbl(X)
0.00/0.40	  , dbl(0()) -> 0()
0.00/0.40	  , add(X1, X2) -> n__add(X1, X2)
0.00/0.40	  , add(0(), X) -> X
0.00/0.40	  , first(X1, X2) -> n__first(X1, X2)
0.00/0.40	  , first(0(), X) -> nil() }
0.00/0.40	Obligation:
0.00/0.40	  innermost runtime complexity
0.00/0.40	Answer:
0.00/0.40	  YES(?,O(1))
0.00/0.40	
0.00/0.40	The input was oriented with the instance of 'Small Polynomial Path
0.00/0.40	Order (PS,0-bounded)' as induced by the safe mapping
0.00/0.40	
0.00/0.40	 safe(terms) = {1}, safe(cons) = {1, 2}, safe(recip) = {1},
0.00/0.40	 safe(sqr) = {1}, safe(n__terms) = {1}, safe(s) = {1}, safe(0) = {},
0.00/0.40	 safe(n__add) = {1, 2}, safe(activate) = {}, safe(dbl) = {1},
0.00/0.40	 safe(n__s) = {1}, safe(n__dbl) = {1}, safe(add) = {1, 2},
0.00/0.40	 safe(first) = {1, 2}, safe(nil) = {}, safe(n__first) = {1, 2}
0.00/0.40	
0.00/0.40	and precedence
0.00/0.40	
0.00/0.40	 terms > sqr, terms > s, activate > terms, activate > sqr,
0.00/0.40	 activate > s, activate > dbl, activate > add, activate > first,
0.00/0.40	 dbl > terms, dbl > sqr, dbl > s, add > terms, add > sqr, add > s,
0.00/0.40	 first > terms, first > sqr, first > s, sqr ~ s, dbl ~ add,
0.00/0.40	 dbl ~ first, add ~ first .
0.00/0.40	
0.00/0.40	Following symbols are considered recursive:
0.00/0.40	
0.00/0.40	 {}
0.00/0.40	
0.00/0.40	The recursion depth is 0.
0.00/0.40	
0.00/0.40	For your convenience, here are the satisfied ordering constraints:
0.00/0.40	
0.00/0.40	                      terms(; N) > cons(; recip(; sqr(; N)),  n__terms(; s(; N)))
0.00/0.40	                                                                                 
0.00/0.40	                      terms(; X) > n__terms(; X)                                 
0.00/0.40	                                                                                 
0.00/0.40	                      sqr(; 0()) > 0()                                           
0.00/0.40	                                                                                 
0.00/0.40	                          s(; X) > n__s(; X)                                     
0.00/0.40	                                                                                 
0.00/0.40	                    activate(X;) > X                                             
0.00/0.40	                                                                                 
0.00/0.40	        activate(n__terms(; X);) > terms(; X)                                    
0.00/0.40	                                                                                 
0.00/0.40	    activate(n__add(; X1,  X2);) > add(; X1,  X2)                                
0.00/0.40	                                                                                 
0.00/0.40	            activate(n__s(; X);) > s(; X)                                        
0.00/0.40	                                                                                 
0.00/0.40	          activate(n__dbl(; X);) > dbl(; X)                                      
0.00/0.40	                                                                                 
0.00/0.40	  activate(n__first(; X1,  X2);) > first(; X1,  X2)                              
0.00/0.40	                                                                                 
0.00/0.40	                        dbl(; X) > n__dbl(; X)                                   
0.00/0.40	                                                                                 
0.00/0.40	                      dbl(; 0()) > 0()                                           
0.00/0.40	                                                                                 
0.00/0.40	                  add(; X1,  X2) > n__add(; X1,  X2)                             
0.00/0.40	                                                                                 
0.00/0.40	                  add(; 0(),  X) > X                                             
0.00/0.40	                                                                                 
0.00/0.40	                first(; X1,  X2) > n__first(; X1,  X2)                           
0.00/0.40	                                                                                 
0.00/0.40	                first(; 0(),  X) > nil()                                         
0.00/0.40	                                                                                 
0.00/0.40	
0.00/0.40	Hurray, we answered YES(?,O(1))
0.00/0.40	EOF