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: { even(Cons(x', Cons(x, xs))) -> even(xs) , even(Cons(x, Nil())) -> False() , even(Nil()) -> True() , lte(Cons(x', xs'), Cons(x, xs)) -> lte(xs', xs) , lte(Cons(x, xs), Nil()) -> False() , lte(Nil(), y) -> True() , notEmpty(Cons(x, xs)) -> True() , notEmpty(Nil()) -> False() , goal(x, y) -> and(lte(x, y), even(x)) } Weak Trs: { and(True(), True()) -> True() , and(True(), False()) -> False() , and(False(), True()) -> False() , and(False(), False()) -> False() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We add the following innermost weak dependency pairs: Strict DPs: { even^#(Cons(x', Cons(x, xs))) -> c_1(even^#(xs)) , even^#(Cons(x, Nil())) -> c_2() , even^#(Nil()) -> c_3() , lte^#(Cons(x', xs'), Cons(x, xs)) -> c_4(lte^#(xs', xs)) , lte^#(Cons(x, xs), Nil()) -> c_5() , lte^#(Nil(), y) -> c_6() , notEmpty^#(Cons(x, xs)) -> c_7() , notEmpty^#(Nil()) -> c_8() , goal^#(x, y) -> c_9(and^#(lte(x, y), even(x))) } Weak DPs: { and^#(True(), True()) -> c_10() , and^#(True(), False()) -> c_11() , and^#(False(), True()) -> c_12() , and^#(False(), False()) -> c_13() } 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: { even^#(Cons(x', Cons(x, xs))) -> c_1(even^#(xs)) , even^#(Cons(x, Nil())) -> c_2() , even^#(Nil()) -> c_3() , lte^#(Cons(x', xs'), Cons(x, xs)) -> c_4(lte^#(xs', xs)) , lte^#(Cons(x, xs), Nil()) -> c_5() , lte^#(Nil(), y) -> c_6() , notEmpty^#(Cons(x, xs)) -> c_7() , notEmpty^#(Nil()) -> c_8() , goal^#(x, y) -> c_9(and^#(lte(x, y), even(x))) } Strict Trs: { even(Cons(x', Cons(x, xs))) -> even(xs) , even(Cons(x, Nil())) -> False() , even(Nil()) -> True() , lte(Cons(x', xs'), Cons(x, xs)) -> lte(xs', xs) , lte(Cons(x, xs), Nil()) -> False() , lte(Nil(), y) -> True() , notEmpty(Cons(x, xs)) -> True() , notEmpty(Nil()) -> False() , goal(x, y) -> and(lte(x, y), even(x)) } Weak DPs: { and^#(True(), True()) -> c_10() , and^#(True(), False()) -> c_11() , and^#(False(), True()) -> c_12() , and^#(False(), False()) -> c_13() } Weak Trs: { and(True(), True()) -> True() , and(True(), False()) -> False() , and(False(), True()) -> False() , and(False(), False()) -> False() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We replace rewrite rules by usable rules: Strict Usable Rules: { even(Cons(x', Cons(x, xs))) -> even(xs) , even(Cons(x, Nil())) -> False() , even(Nil()) -> True() , lte(Cons(x', xs'), Cons(x, xs)) -> lte(xs', xs) , lte(Cons(x, xs), Nil()) -> False() , lte(Nil(), y) -> True() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { even^#(Cons(x', Cons(x, xs))) -> c_1(even^#(xs)) , even^#(Cons(x, Nil())) -> c_2() , even^#(Nil()) -> c_3() , lte^#(Cons(x', xs'), Cons(x, xs)) -> c_4(lte^#(xs', xs)) , lte^#(Cons(x, xs), Nil()) -> c_5() , lte^#(Nil(), y) -> c_6() , notEmpty^#(Cons(x, xs)) -> c_7() , notEmpty^#(Nil()) -> c_8() , goal^#(x, y) -> c_9(and^#(lte(x, y), even(x))) } Strict Trs: { even(Cons(x', Cons(x, xs))) -> even(xs) , even(Cons(x, Nil())) -> False() , even(Nil()) -> True() , lte(Cons(x', xs'), Cons(x, xs)) -> lte(xs', xs) , lte(Cons(x, xs), Nil()) -> False() , lte(Nil(), y) -> True() } Weak DPs: { and^#(True(), True()) -> c_10() , and^#(True(), False()) -> c_11() , and^#(False(), True()) -> c_12() , and^#(False(), False()) -> c_13() } 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_4) = {1}, Uargs(c_9) = {1}, Uargs(and^#) = {1, 2} TcT has computed the following constructor-restricted matrix interpretation. [even](x1) = [0 1] x1 + [2] [0 0] [0] [lte](x1, x2) = [0 1] x1 + [0 1] x2 + [2] [0 0] [0 0] [0] [True] = [0] [0] [Cons](x1, x2) = [0 0] x2 + [0] [0 1] [1] [Nil] = [0] [2] [False] = [0] [0] [even^#](x1) = [0] [0] [c_1](x1) = [1 0] x1 + [2] [0 1] [2] [c_2] = [1] [1] [c_3] = [1] [1] [lte^#](x1, x2) = [0] [0] [c_4](x1) = [1 0] x1 + [2] [0 1] [2] [c_5] = [1] [1] [c_6] = [1] [1] [notEmpty^#](x1) = [1 1] x1 + [1] [2 1] [1] [c_7] = [1] [1] [c_8] = [1] [1] [goal^#](x1, x2) = [1 2] x1 + [2 2] x2 + [1] [2 1] [1 1] [1] [c_9](x1) = [1 0] x1 + [2] [0 1] [2] [and^#](x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [0] [c_10] = [0] [0] [c_11] = [0] [0] [c_12] = [0] [0] [c_13] = [0] [0] The following symbols are considered usable {even, lte, even^#, lte^#, notEmpty^#, goal^#, and^#} The order satisfies the following ordering constraints: [even(Cons(x', Cons(x, xs)))] = [0 1] xs + [4] [0 0] [0] > [0 1] xs + [2] [0 0] [0] = [even(xs)] [even(Cons(x, Nil()))] = [5] [0] > [0] [0] = [False()] [even(Nil())] = [4] [0] > [0] [0] = [True()] [lte(Cons(x', xs'), Cons(x, xs))] = [0 1] xs' + [0 1] xs + [4] [0 0] [0 0] [0] > [0 1] xs' + [0 1] xs + [2] [0 0] [0 0] [0] = [lte(xs', xs)] [lte(Cons(x, xs), Nil())] = [0 1] xs + [5] [0 0] [0] > [0] [0] = [False()] [lte(Nil(), y)] = [0 1] y + [4] [0 0] [0] > [0] [0] = [True()] [even^#(Cons(x', Cons(x, xs)))] = [0] [0] ? [2] [2] = [c_1(even^#(xs))] [even^#(Cons(x, Nil()))] = [0] [0] ? [1] [1] = [c_2()] [even^#(Nil())] = [0] [0] ? [1] [1] = [c_3()] [lte^#(Cons(x', xs'), Cons(x, xs))] = [0] [0] ? [2] [2] = [c_4(lte^#(xs', xs))] [lte^#(Cons(x, xs), Nil())] = [0] [0] ? [1] [1] = [c_5()] [lte^#(Nil(), y)] = [0] [0] ? [1] [1] = [c_6()] [notEmpty^#(Cons(x, xs))] = [0 1] xs + [2] [0 1] [2] > [1] [1] = [c_7()] [notEmpty^#(Nil())] = [3] [3] > [1] [1] = [c_8()] [goal^#(x, y)] = [1 2] x + [2 2] y + [1] [2 1] [1 1] [1] ? [0 2] x + [0 1] y + [6] [0 0] [0 0] [2] = [c_9(and^#(lte(x, y), even(x)))] [and^#(True(), True())] = [0] [0] >= [0] [0] = [c_10()] [and^#(True(), False())] = [0] [0] >= [0] [0] = [c_11()] [and^#(False(), True())] = [0] [0] >= [0] [0] = [c_12()] [and^#(False(), False())] = [0] [0] >= [0] [0] = [c_13()] 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(1),O(n^1)). Strict DPs: { even^#(Cons(x', Cons(x, xs))) -> c_1(even^#(xs)) , even^#(Cons(x, Nil())) -> c_2() , even^#(Nil()) -> c_3() , lte^#(Cons(x', xs'), Cons(x, xs)) -> c_4(lte^#(xs', xs)) , lte^#(Cons(x, xs), Nil()) -> c_5() , lte^#(Nil(), y) -> c_6() , goal^#(x, y) -> c_9(and^#(lte(x, y), even(x))) } Weak DPs: { notEmpty^#(Cons(x, xs)) -> c_7() , notEmpty^#(Nil()) -> c_8() , and^#(True(), True()) -> c_10() , and^#(True(), False()) -> c_11() , and^#(False(), True()) -> c_12() , and^#(False(), False()) -> c_13() } Weak Trs: { even(Cons(x', Cons(x, xs))) -> even(xs) , even(Cons(x, Nil())) -> False() , even(Nil()) -> True() , lte(Cons(x', xs'), Cons(x, xs)) -> lte(xs', xs) , lte(Cons(x, xs), Nil()) -> False() , lte(Nil(), y) -> True() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We estimate the number of application of {2,3,5,6,7} by applications of Pre({2,3,5,6,7}) = {1,4}. Here rules are labeled as follows: DPs: { 1: even^#(Cons(x', Cons(x, xs))) -> c_1(even^#(xs)) , 2: even^#(Cons(x, Nil())) -> c_2() , 3: even^#(Nil()) -> c_3() , 4: lte^#(Cons(x', xs'), Cons(x, xs)) -> c_4(lte^#(xs', xs)) , 5: lte^#(Cons(x, xs), Nil()) -> c_5() , 6: lte^#(Nil(), y) -> c_6() , 7: goal^#(x, y) -> c_9(and^#(lte(x, y), even(x))) , 8: notEmpty^#(Cons(x, xs)) -> c_7() , 9: notEmpty^#(Nil()) -> c_8() , 10: and^#(True(), True()) -> c_10() , 11: and^#(True(), False()) -> c_11() , 12: and^#(False(), True()) -> c_12() , 13: and^#(False(), False()) -> c_13() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { even^#(Cons(x', Cons(x, xs))) -> c_1(even^#(xs)) , lte^#(Cons(x', xs'), Cons(x, xs)) -> c_4(lte^#(xs', xs)) } Weak DPs: { even^#(Cons(x, Nil())) -> c_2() , even^#(Nil()) -> c_3() , lte^#(Cons(x, xs), Nil()) -> c_5() , lte^#(Nil(), y) -> c_6() , notEmpty^#(Cons(x, xs)) -> c_7() , notEmpty^#(Nil()) -> c_8() , goal^#(x, y) -> c_9(and^#(lte(x, y), even(x))) , and^#(True(), True()) -> c_10() , and^#(True(), False()) -> c_11() , and^#(False(), True()) -> c_12() , and^#(False(), False()) -> c_13() } Weak Trs: { even(Cons(x', Cons(x, xs))) -> even(xs) , even(Cons(x, Nil())) -> False() , even(Nil()) -> True() , lte(Cons(x', xs'), Cons(x, xs)) -> lte(xs', xs) , lte(Cons(x, xs), Nil()) -> False() , lte(Nil(), y) -> True() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { even^#(Cons(x, Nil())) -> c_2() , even^#(Nil()) -> c_3() , lte^#(Cons(x, xs), Nil()) -> c_5() , lte^#(Nil(), y) -> c_6() , notEmpty^#(Cons(x, xs)) -> c_7() , notEmpty^#(Nil()) -> c_8() , goal^#(x, y) -> c_9(and^#(lte(x, y), even(x))) , and^#(True(), True()) -> c_10() , and^#(True(), False()) -> c_11() , and^#(False(), True()) -> c_12() , and^#(False(), False()) -> c_13() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { even^#(Cons(x', Cons(x, xs))) -> c_1(even^#(xs)) , lte^#(Cons(x', xs'), Cons(x, xs)) -> c_4(lte^#(xs', xs)) } Weak Trs: { even(Cons(x', Cons(x, xs))) -> even(xs) , even(Cons(x, Nil())) -> False() , even(Nil()) -> True() , lte(Cons(x', xs'), Cons(x, xs)) -> lte(xs', xs) , lte(Cons(x, xs), Nil()) -> False() , lte(Nil(), y) -> True() } 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: { even^#(Cons(x', Cons(x, xs))) -> c_1(even^#(xs)) , lte^#(Cons(x', xs'), Cons(x, xs)) -> c_4(lte^#(xs', xs)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'Small Polynomial Path Order (PS,1-bounded)' to orient following rules strictly. DPs: { 1: even^#(Cons(x', Cons(x, xs))) -> c_1(even^#(xs)) , 2: lte^#(Cons(x', xs'), Cons(x, xs)) -> c_4(lte^#(xs', xs)) } Sub-proof: ---------- The input was oriented with the instance of 'Small Polynomial Path Order (PS,1-bounded)' as induced by the safe mapping safe(even) = {}, safe(lte) = {}, safe(True) = {}, safe(Cons) = {1, 2}, safe(Nil) = {}, safe(notEmpty) = {}, safe(and) = {}, safe(goal) = {}, safe(False) = {}, safe(even^#) = {}, safe(c_1) = {}, safe(c_2) = {}, safe(c_3) = {}, safe(lte^#) = {2}, safe(c_4) = {}, safe(c_5) = {}, safe(c_6) = {}, safe(notEmpty^#) = {}, safe(c_7) = {}, safe(c_8) = {}, safe(goal^#) = {}, safe(c_9) = {}, safe(and^#) = {}, safe(c_10) = {}, safe(c_11) = {}, safe(c_12) = {}, safe(c_13) = {} and precedence empty . Following symbols are considered recursive: {even^#, lte^#} The recursion depth is 1. Further, following argument filtering is employed: pi(even) = [], pi(lte) = [], pi(True) = [], pi(Cons) = [2], pi(Nil) = [], pi(notEmpty) = [], pi(and) = [], pi(goal) = [], pi(False) = [], pi(even^#) = [1], pi(c_1) = [1], pi(c_2) = [], pi(c_3) = [], pi(lte^#) = [1], pi(c_4) = [1], pi(c_5) = [], pi(c_6) = [], pi(notEmpty^#) = [], pi(c_7) = [], pi(c_8) = [], pi(goal^#) = [], pi(c_9) = [], pi(and^#) = [], pi(c_10) = [], pi(c_11) = [], pi(c_12) = [], pi(c_13) = [] Usable defined function symbols are a subset of: {even^#, lte^#, notEmpty^#, goal^#, and^#} For your convenience, here are the satisfied ordering constraints: pi(even^#(Cons(x', Cons(x, xs)))) = even^#(Cons(; Cons(; xs));) > c_1(even^#(xs;);) = pi(c_1(even^#(xs))) pi(lte^#(Cons(x', xs'), Cons(x, xs))) = lte^#(Cons(; xs');) > c_4(lte^#(xs';);) = pi(c_4(lte^#(xs', xs))) The strictly oriented rules are moved into the weak component. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak DPs: { even^#(Cons(x', Cons(x, xs))) -> c_1(even^#(xs)) , lte^#(Cons(x', xs'), Cons(x, xs)) -> c_4(lte^#(xs', xs)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { even^#(Cons(x', Cons(x, xs))) -> c_1(even^#(xs)) , lte^#(Cons(x', xs'), Cons(x, xs)) -> c_4(lte^#(xs', xs)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded Hurray, we answered YES(O(1),O(n^1))