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