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(X)) -> s(add(sqr(X), dbl(X)))
  , add(0(), X) -> X
  , add(s(X), Y) -> s(add(X, Y))
  , dbl(0()) -> 0()
  , dbl(s(X)) -> s(s(dbl(X)))
  , first(0(), X) -> nil()
  , first(s(X), 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 > add,
 terms > dbl, cons > sqr, cons > s, cons > add, cons > dbl,
 recip > sqr, recip > s, recip > add, recip > dbl, sqr > s,
 sqr > add, sqr > dbl, 0 > cons, 0 > recip, 0 > sqr, 0 > s, 0 > add,
 0 > dbl, add > s, dbl > s, first > cons, first > recip,
 first > sqr, first > s, first > add, first > dbl, nil > cons,
 nil > recip, nil > sqr, nil > s, nil > add, nil > dbl, terms ~ 0,
 terms ~ first, terms ~ nil, cons ~ recip, 0 ~ first, 0 ~ nil,
 add ~ dbl, first ~ nil .

Hurray, we answered YES(?,PRIMREC)