YES(?,PRIMREC)

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

Strict Trs:
  { fst(0(), Z) -> nil()
  , fst(s(), cons(Y)) -> cons(Y)
  , from(X) -> cons(X)
  , add(0(), X) -> X
  , add(s(), Y) -> s()
  , len(nil()) -> 0()
  , len(cons(X)) -> s() }
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 > cons, nil > 0, nil > cons, s > 0, s > cons,
 from > 0, from > cons, add > 0, add > cons, len > 0, len > cons,
 fst ~ nil, fst ~ s, fst ~ from, fst ~ add, fst ~ len, 0 ~ cons,
 nil ~ s, nil ~ from, nil ~ add, nil ~ len, s ~ from, s ~ add,
 s ~ len, from ~ add, from ~ len, add ~ len .

Hurray, we answered YES(?,PRIMREC)