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