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