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