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