YES(?,PRIMREC)

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

Strict Trs:
  { terms(N) -> cons(recip(sqr(N)))
  , sqr(0()) -> 0()
  , sqr(s()) -> s()
  , dbl(0()) -> 0()
  , dbl(s()) -> s()
  , add(0(), X) -> X
  , add(s(), Y) -> s()
  , first(0(), X) -> nil()
  , first(s(), cons(Y)) -> cons(Y) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,PRIMREC)

The input was oriented with the instance of'multiset path order' as
induced by the precedence

 terms > cons, terms > recip, terms > sqr, terms > s, terms > nil,
 cons > sqr, cons > s, recip > sqr, recip > s, sqr > s, 0 > cons,
 0 > recip, 0 > sqr, 0 > s, 0 > nil, dbl > cons, dbl > recip,
 dbl > sqr, dbl > s, dbl > nil, add > cons, add > recip, add > sqr,
 add > s, add > nil, first > cons, first > recip, first > sqr,
 first > s, first > nil, nil > sqr, nil > s, terms ~ 0, terms ~ dbl,
 terms ~ add, terms ~ first, cons ~ recip, cons ~ nil, recip ~ nil,
 0 ~ dbl, 0 ~ add, 0 ~ first, dbl ~ add, dbl ~ first, add ~ first .

Hurray, we answered YES(?,PRIMREC)