YES(?,O(n^1)) We are left with following problem, upon which TcT provides the certificate YES(?,O(n^1)). 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(?,O(n^1)) The input was oriented with the instance of 'Small Polynomial Path Order (PS)' as induced by the safe mapping safe(p) = {}, safe(s) = {1}, safe(0) = {} and precedence empty . Following symbols are considered recursive: {p} The recursion depth is 1. For your convenience, here are the satisfied ordering constraints: p(m, n, s(; r);) > p(m, r, n;) p(m, s(; n), 0();) > p(0(), n, m;) p(m, 0(), 0();) > m Hurray, we answered YES(?,O(n^1))