YES(?,PRIMREC) We are left with following problem, upon which TcT provides the certificate YES(?,PRIMREC). Strict Trs: { sum(0()) -> 0() , sum(s(x)) -> +(sqr(s(x)), sum(x)) , sum(s(x)) -> +(*(s(x), s(x)), sum(x)) , sqr(x) -> *(x, x) } Obligation: innermost runtime complexity Answer: YES(?,PRIMREC) The input was oriented with the instance of'multiset path order' as induced by the precedence sum > +, sum > sqr, sum > *, 0 > +, 0 > sqr, 0 > *, s > +, s > sqr, s > *, + > *, sqr > *, sum ~ 0, sum ~ s, 0 ~ s, + ~ sqr . Hurray, we answered YES(?,PRIMREC)