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