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