YES(?,O(1))

We are left with following problem, upon which TcT provides the
certificate YES(?,O(1)).

Strict Trs:
  { terms(N) -> cons(recip(sqr(N)), n__terms(s(N)))
  , terms(X) -> n__terms(X)
  , sqr(s(X)) -> s(n__add(sqr(activate(X)), dbl(activate(X))))
  , sqr(0()) -> 0()
  , s(X) -> n__s(X)
  , activate(X) -> X
  , activate(n__terms(X)) -> terms(X)
  , activate(n__add(X1, X2)) -> add(X1, X2)
  , activate(n__s(X)) -> s(X)
  , activate(n__dbl(X)) -> dbl(X)
  , activate(n__first(X1, X2)) -> first(X1, X2)
  , dbl(X) -> n__dbl(X)
  , dbl(s(X)) -> s(n__s(n__dbl(activate(X))))
  , dbl(0()) -> 0()
  , add(X1, X2) -> n__add(X1, X2)
  , add(s(X), Y) -> s(n__add(activate(X), Y))
  , add(0(), X) -> X
  , first(X1, X2) -> n__first(X1, X2)
  , first(s(X), cons(Y, Z)) ->
    cons(Y, n__first(activate(X), activate(Z)))
  , first(0(), X) -> nil() }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(1))

Arguments of following rules are not normal-forms:

{ sqr(s(X)) -> s(n__add(sqr(activate(X)), dbl(activate(X))))
, dbl(s(X)) -> s(n__s(n__dbl(activate(X))))
, add(s(X), Y) -> s(n__add(activate(X), Y))
, first(s(X), cons(Y, Z)) ->
  cons(Y, n__first(activate(X), activate(Z))) }

All above mentioned rules can be savely removed.

We are left with following problem, upon which TcT provides the
certificate YES(?,O(1)).

Strict Trs:
  { terms(N) -> cons(recip(sqr(N)), n__terms(s(N)))
  , terms(X) -> n__terms(X)
  , sqr(0()) -> 0()
  , s(X) -> n__s(X)
  , activate(X) -> X
  , activate(n__terms(X)) -> terms(X)
  , activate(n__add(X1, X2)) -> add(X1, X2)
  , activate(n__s(X)) -> s(X)
  , activate(n__dbl(X)) -> dbl(X)
  , activate(n__first(X1, X2)) -> first(X1, X2)
  , dbl(X) -> n__dbl(X)
  , dbl(0()) -> 0()
  , add(X1, X2) -> n__add(X1, X2)
  , add(0(), X) -> X
  , first(X1, X2) -> n__first(X1, X2)
  , first(0(), X) -> nil() }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(1))

The input was oriented with the instance of 'Small Polynomial Path
Order (PS,0-bounded)' as induced by the safe mapping

 safe(terms) = {1}, safe(cons) = {1, 2}, safe(recip) = {1},
 safe(sqr) = {1}, safe(n__terms) = {1}, safe(s) = {1}, safe(0) = {},
 safe(n__add) = {1, 2}, safe(activate) = {}, safe(dbl) = {1},
 safe(n__s) = {1}, safe(n__dbl) = {1}, safe(add) = {1, 2},
 safe(first) = {1, 2}, safe(nil) = {}, safe(n__first) = {1, 2}

and precedence

 terms > sqr, terms > s, activate > terms, activate > sqr,
 activate > s, activate > dbl, activate > add, activate > first,
 dbl > terms, dbl > sqr, dbl > s, add > terms, add > sqr, add > s,
 first > terms, first > sqr, first > s, sqr ~ s, dbl ~ add,
 dbl ~ first, add ~ first .

Following symbols are considered recursive:

 {}

The recursion depth is 0.

For your convenience, here are the satisfied ordering constraints:

                      terms(; N) > cons(; recip(; sqr(; N)),  n__terms(; s(; N)))
                                                                                 
                      terms(; X) > n__terms(; X)                                 
                                                                                 
                      sqr(; 0()) > 0()                                           
                                                                                 
                          s(; X) > n__s(; X)                                     
                                                                                 
                    activate(X;) > X                                             
                                                                                 
        activate(n__terms(; X);) > terms(; X)                                    
                                                                                 
    activate(n__add(; X1,  X2);) > add(; X1,  X2)                                
                                                                                 
            activate(n__s(; X);) > s(; X)                                        
                                                                                 
          activate(n__dbl(; X);) > dbl(; X)                                      
                                                                                 
  activate(n__first(; X1,  X2);) > first(; X1,  X2)                              
                                                                                 
                        dbl(; X) > n__dbl(; X)                                   
                                                                                 
                      dbl(; 0()) > 0()                                           
                                                                                 
                  add(; X1,  X2) > n__add(; X1,  X2)                             
                                                                                 
                  add(; 0(),  X) > X                                             
                                                                                 
                first(; X1,  X2) > n__first(; X1,  X2)                           
                                                                                 
                first(; 0(),  X) > nil()                                         
                                                                                 

Hurray, we answered YES(?,O(1))