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