YES(?,O(n^2)) We are left with following problem, upon which TcT provides the certificate YES(?,O(n^2)). Strict Trs: { add(0(), x) -> x , add(s(x), y) -> s(add(x, y)) , mult(0(), x) -> 0() , mult(s(x), y) -> add(y, mult(x, y)) } Obligation: innermost runtime complexity Answer: YES(?,O(n^2)) The input was oriented with the instance of 'Small Polynomial Path Order (PS)' as induced by the safe mapping safe(add) = {2}, safe(0) = {}, safe(s) = {1}, safe(mult) = {} and precedence mult > add . Following symbols are considered recursive: {add, mult} The recursion depth is 2. For your convenience, here are the satisfied ordering constraints: add(0(); x) > x add(s(; x); y) > s(; add(x; y)) mult(0(), x;) > 0() mult(s(; x), y;) > add(y; mult(x, y;)) Hurray, we answered YES(?,O(n^2))