YES(?,PRIMREC)

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

Strict Trs:
  { fst(X1, X2) -> n__fst(X1, X2)
  , fst(0(), Z) -> nil()
  , fst(s(X), cons(Y, Z)) ->
    cons(Y, n__fst(activate(X), activate(Z)))
  , activate(X) -> X
  , activate(n__fst(X1, X2)) -> fst(X1, X2)
  , activate(n__from(X)) -> from(X)
  , activate(n__add(X1, X2)) -> add(X1, X2)
  , activate(n__len(X)) -> len(X)
  , from(X) -> cons(X, n__from(s(X)))
  , from(X) -> n__from(X)
  , add(X1, X2) -> n__add(X1, X2)
  , add(0(), X) -> X
  , add(s(X), Y) -> s(n__add(activate(X), Y))
  , len(X) -> n__len(X)
  , len(nil()) -> 0()
  , len(cons(X, Z)) -> s(n__len(activate(Z))) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,PRIMREC)

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

 fst > 0, fst > s, fst > cons, fst > n__fst, fst > n__from,
 fst > n__add, fst > n__len, nil > 0, nil > s, nil > cons,
 nil > n__fst, nil > n__from, nil > n__add, nil > n__len,
 n__fst > 0, n__fst > s, n__fst > cons, n__fst > n__len,
 activate > 0, activate > s, activate > cons, activate > n__fst,
 activate > n__from, activate > n__add, activate > n__len, from > 0,
 from > s, from > cons, from > n__fst, from > n__from,
 from > n__add, from > n__len, n__from > 0, n__from > s,
 n__from > cons, n__from > n__len, add > 0, add > s, add > cons,
 add > n__fst, add > n__from, add > n__add, add > n__len,
 n__add > 0, n__add > s, n__add > cons, n__add > n__len, len > s,
 len > cons, len > n__fst, len > n__from, len > n__add,
 len > n__len, fst ~ nil, fst ~ activate, fst ~ from, fst ~ add,
 fst ~ len, 0 ~ s, 0 ~ cons, 0 ~ n__len, nil ~ activate, nil ~ from,
 nil ~ add, nil ~ len, s ~ cons, s ~ n__len, cons ~ n__len,
 n__fst ~ n__from, n__fst ~ n__add, activate ~ from, activate ~ add,
 activate ~ len, from ~ add, from ~ len, n__from ~ n__add,
 add ~ len .

Hurray, we answered YES(?,PRIMREC)