YES(O(1),O(n^1)) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict Trs: { rev(ls) -> r1(ls, empty()) , r1(empty(), a) -> a , r1(cons(x, k), a) -> r1(k, cons(x, a)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We add following weak dependency pairs: Strict DPs: { rev^#(ls) -> c_1(r1^#(ls, empty())) , r1^#(empty(), a) -> c_2() , r1^#(cons(x, k), a) -> c_3(r1^#(k, cons(x, a))) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { rev^#(ls) -> c_1(r1^#(ls, empty())) , r1^#(empty(), a) -> c_2() , r1^#(cons(x, k), a) -> c_3(r1^#(k, cons(x, a))) } Strict Trs: { rev(ls) -> r1(ls, empty()) , r1(empty(), a) -> a , r1(cons(x, k), a) -> r1(k, cons(x, a)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { rev^#(ls) -> c_1(r1^#(ls, empty())) , r1^#(empty(), a) -> c_2() , r1^#(cons(x, k), a) -> c_3(r1^#(k, cons(x, a))) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) The weightgap principle applies (using the following constant growth matrix-interpretation) The following argument positions are usable: Uargs(c_1) = {1}, Uargs(c_3) = {1} TcT has computed following constructor-restricted matrix interpretation. [empty] = [0] [cons](x1, x2) = [1] x2 + [0] [rev^#](x1) = [1] x1 + [2] [c_1](x1) = [1] x1 + [1] [r1^#](x1, x2) = [2] x2 + [0] [c_2] = [1] [c_3](x1) = [1] x1 + [1] This order satisfies following ordering constraints: Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate YES(?,O(n^1)). Strict DPs: { r1^#(empty(), a) -> c_2() , r1^#(cons(x, k), a) -> c_3(r1^#(k, cons(x, a))) } Weak DPs: { rev^#(ls) -> c_1(r1^#(ls, empty())) } Obligation: innermost runtime complexity Answer: YES(?,O(n^1)) Consider the dependency graph 1: r1^#(empty(), a) -> c_2() 2: r1^#(cons(x, k), a) -> c_3(r1^#(k, cons(x, a))) -->_1 r1^#(cons(x, k), a) -> c_3(r1^#(k, cons(x, a))) :2 -->_1 r1^#(empty(), a) -> c_2() :1 3: rev^#(ls) -> c_1(r1^#(ls, empty())) -->_1 r1^#(cons(x, k), a) -> c_3(r1^#(k, cons(x, a))) :2 -->_1 r1^#(empty(), a) -> c_2() :1 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). { rev^#(ls) -> c_1(r1^#(ls, empty())) } We are left with following problem, upon which TcT provides the certificate YES(?,O(n^1)). Strict DPs: { r1^#(empty(), a) -> c_2() , r1^#(cons(x, k), a) -> c_3(r1^#(k, cons(x, a))) } 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(empty) = {}, safe(cons) = {1, 2}, safe(r1^#) = {2}, safe(c_2) = {}, safe(c_3) = {} and precedence empty . Following symbols are considered recursive: {r1^#} The recursion depth is 1. Further, following argument filtering is employed: pi(empty) = [], pi(cons) = [1, 2], pi(r1^#) = [1, 2], pi(c_2) = [], pi(c_3) = [1] Usable defined function symbols are a subset of: {r1^#} For your convenience, here are the satisfied ordering constraints: pi(r1^#(empty(), a)) = r1^#(empty(); a) > c_2() = pi(c_2()) pi(r1^#(cons(x, k), a)) = r1^#(cons(; x, k); a) > c_3(r1^#(k; cons(; x, a));) = pi(c_3(r1^#(k, cons(x, a)))) Hurray, we answered YES(O(1),O(n^1))