We are left with following problem, upon which TcT provides the certificate YES(?,O(n^1)). Strict Trs: { sum(0()) -> 0() , sum(s(x)) -> +(sqr(s(x)), sum(x)) , sum(s(x)) -> +(*(s(x), s(x)), sum(x)) , sqr(x) -> *(x, x) } 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(sum) = {}, safe(0) = {}, safe(s) = {1}, safe(+) = {1, 2}, safe(sqr) = {}, safe(*) = {1, 2} and precedence sum > sqr . Following symbols are considered recursive: {sum} The recursion depth is 1. For your convenience, here are the satisfied ordering constraints: sum(0();) > 0() sum(s(; x);) > +(; sqr(s(; x);), sum(x;)) sum(s(; x);) > +(; *(; s(; x), s(; x)), sum(x;)) sqr(x;) > *(; x, x) Hurray, we answered YES(?,O(n^1))