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: { dec(Cons(Cons(x', xs'), Cons(x, xs))) -> dec(Cons(x, xs)) , dec(Cons(Cons(x, xs), Nil())) -> dec(Nil()) , dec(Cons(Nil(), Cons(x, xs))) -> dec(Cons(x, xs)) , dec(Cons(Nil(), Nil())) -> Nil() , isNilNil(Cons(Cons(x', xs'), Cons(x, xs))) -> False() , isNilNil(Cons(Cons(x, xs), Nil())) -> False() , isNilNil(Cons(Nil(), Cons(x, xs))) -> False() , isNilNil(Cons(Nil(), Nil())) -> True() , nestdec(Cons(x, xs)) -> nestdec(dec(Cons(x, xs))) , nestdec(Nil()) -> Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Nil()))))))))))))))))) , number17(n) -> Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Nil()))))))))))))))))) , goal(x) -> nestdec(x) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We add the following innermost weak dependency pairs: Strict DPs: { dec^#(Cons(Cons(x', xs'), Cons(x, xs))) -> c_1(dec^#(Cons(x, xs))) , dec^#(Cons(Cons(x, xs), Nil())) -> c_2(dec^#(Nil())) , dec^#(Cons(Nil(), Cons(x, xs))) -> c_3(dec^#(Cons(x, xs))) , dec^#(Cons(Nil(), Nil())) -> c_4() , isNilNil^#(Cons(Cons(x', xs'), Cons(x, xs))) -> c_5() , isNilNil^#(Cons(Cons(x, xs), Nil())) -> c_6() , isNilNil^#(Cons(Nil(), Cons(x, xs))) -> c_7() , isNilNil^#(Cons(Nil(), Nil())) -> c_8() , nestdec^#(Cons(x, xs)) -> c_9(nestdec^#(dec(Cons(x, xs)))) , nestdec^#(Nil()) -> c_10() , number17^#(n) -> c_11() , goal^#(x) -> c_12(nestdec^#(x)) } 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: { dec^#(Cons(Cons(x', xs'), Cons(x, xs))) -> c_1(dec^#(Cons(x, xs))) , dec^#(Cons(Cons(x, xs), Nil())) -> c_2(dec^#(Nil())) , dec^#(Cons(Nil(), Cons(x, xs))) -> c_3(dec^#(Cons(x, xs))) , dec^#(Cons(Nil(), Nil())) -> c_4() , isNilNil^#(Cons(Cons(x', xs'), Cons(x, xs))) -> c_5() , isNilNil^#(Cons(Cons(x, xs), Nil())) -> c_6() , isNilNil^#(Cons(Nil(), Cons(x, xs))) -> c_7() , isNilNil^#(Cons(Nil(), Nil())) -> c_8() , nestdec^#(Cons(x, xs)) -> c_9(nestdec^#(dec(Cons(x, xs)))) , nestdec^#(Nil()) -> c_10() , number17^#(n) -> c_11() , goal^#(x) -> c_12(nestdec^#(x)) } Strict Trs: { dec(Cons(Cons(x', xs'), Cons(x, xs))) -> dec(Cons(x, xs)) , dec(Cons(Cons(x, xs), Nil())) -> dec(Nil()) , dec(Cons(Nil(), Cons(x, xs))) -> dec(Cons(x, xs)) , dec(Cons(Nil(), Nil())) -> Nil() , isNilNil(Cons(Cons(x', xs'), Cons(x, xs))) -> False() , isNilNil(Cons(Cons(x, xs), Nil())) -> False() , isNilNil(Cons(Nil(), Cons(x, xs))) -> False() , isNilNil(Cons(Nil(), Nil())) -> True() , nestdec(Cons(x, xs)) -> nestdec(dec(Cons(x, xs))) , nestdec(Nil()) -> Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Nil()))))))))))))))))) , number17(n) -> Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Nil()))))))))))))))))) , goal(x) -> nestdec(x) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We replace rewrite rules by usable rules: Strict Usable Rules: { dec(Cons(Cons(x', xs'), Cons(x, xs))) -> dec(Cons(x, xs)) , dec(Cons(Cons(x, xs), Nil())) -> dec(Nil()) , dec(Cons(Nil(), Cons(x, xs))) -> dec(Cons(x, xs)) , dec(Cons(Nil(), Nil())) -> Nil() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { dec^#(Cons(Cons(x', xs'), Cons(x, xs))) -> c_1(dec^#(Cons(x, xs))) , dec^#(Cons(Cons(x, xs), Nil())) -> c_2(dec^#(Nil())) , dec^#(Cons(Nil(), Cons(x, xs))) -> c_3(dec^#(Cons(x, xs))) , dec^#(Cons(Nil(), Nil())) -> c_4() , isNilNil^#(Cons(Cons(x', xs'), Cons(x, xs))) -> c_5() , isNilNil^#(Cons(Cons(x, xs), Nil())) -> c_6() , isNilNil^#(Cons(Nil(), Cons(x, xs))) -> c_7() , isNilNil^#(Cons(Nil(), Nil())) -> c_8() , nestdec^#(Cons(x, xs)) -> c_9(nestdec^#(dec(Cons(x, xs)))) , nestdec^#(Nil()) -> c_10() , number17^#(n) -> c_11() , goal^#(x) -> c_12(nestdec^#(x)) } Strict Trs: { dec(Cons(Cons(x', xs'), Cons(x, xs))) -> dec(Cons(x, xs)) , dec(Cons(Cons(x, xs), Nil())) -> dec(Nil()) , dec(Cons(Nil(), Cons(x, xs))) -> dec(Cons(x, xs)) , dec(Cons(Nil(), Nil())) -> Nil() } 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}, Uargs(nestdec^#) = {1}, Uargs(c_9) = {1}, Uargs(c_12) = {1} TcT has computed the following constructor-restricted matrix interpretation. [dec](x1) = [0 1] x1 + [2] [2 0] [2] [Cons](x1, x2) = [0 0] x2 + [1] [0 1] [1] [Nil] = [1] [2] [dec^#](x1) = [0] [0] [c_1](x1) = [1 0] x1 + [2] [0 1] [2] [c_2](x1) = [2] [2] [c_3](x1) = [1 0] x1 + [2] [0 1] [2] [c_4] = [1] [1] [isNilNil^#](x1) = [0] [0] [c_5] = [1] [1] [c_6] = [1] [1] [c_7] = [1] [0] [c_8] = [1] [0] [nestdec^#](x1) = [1 1] x1 + [0] [0 0] [0] [c_9](x1) = [1 0] x1 + [0] [0 1] [2] [c_10] = [2] [1] [number17^#](x1) = [1] [1] [c_11] = [0] [1] [goal^#](x1) = [1 2] x1 + [1] [1 1] [1] [c_12](x1) = [1 0] x1 + [2] [0 1] [2] The following symbols are considered usable {dec, dec^#, isNilNil^#, nestdec^#, number17^#, goal^#} The order satisfies the following ordering constraints: [dec(Cons(Cons(x', xs'), Cons(x, xs)))] = [0 1] xs + [4] [0 0] [4] > [0 1] xs + [3] [0 0] [4] = [dec(Cons(x, xs))] [dec(Cons(Cons(x, xs), Nil()))] = [5] [4] > [4] [4] = [dec(Nil())] [dec(Cons(Nil(), Cons(x, xs)))] = [0 1] xs + [4] [0 0] [4] > [0 1] xs + [3] [0 0] [4] = [dec(Cons(x, xs))] [dec(Cons(Nil(), Nil()))] = [5] [4] > [1] [2] = [Nil()] [dec^#(Cons(Cons(x', xs'), Cons(x, xs)))] = [0] [0] ? [2] [2] = [c_1(dec^#(Cons(x, xs)))] [dec^#(Cons(Cons(x, xs), Nil()))] = [0] [0] ? [2] [2] = [c_2(dec^#(Nil()))] [dec^#(Cons(Nil(), Cons(x, xs)))] = [0] [0] ? [2] [2] = [c_3(dec^#(Cons(x, xs)))] [dec^#(Cons(Nil(), Nil()))] = [0] [0] ? [1] [1] = [c_4()] [isNilNil^#(Cons(Cons(x', xs'), Cons(x, xs)))] = [0] [0] ? [1] [1] = [c_5()] [isNilNil^#(Cons(Cons(x, xs), Nil()))] = [0] [0] ? [1] [1] = [c_6()] [isNilNil^#(Cons(Nil(), Cons(x, xs)))] = [0] [0] ? [1] [0] = [c_7()] [isNilNil^#(Cons(Nil(), Nil()))] = [0] [0] ? [1] [0] = [c_8()] [nestdec^#(Cons(x, xs))] = [0 1] xs + [2] [0 0] [0] ? [0 1] xs + [7] [0 0] [2] = [c_9(nestdec^#(dec(Cons(x, xs))))] [nestdec^#(Nil())] = [3] [0] ? [2] [1] = [c_10()] [number17^#(n)] = [1] [1] > [0] [1] = [c_11()] [goal^#(x)] = [1 2] x + [1] [1 1] [1] ? [1 1] x + [2] [0 0] [2] = [c_12(nestdec^#(x))] 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: { dec^#(Cons(Cons(x', xs'), Cons(x, xs))) -> c_1(dec^#(Cons(x, xs))) , dec^#(Cons(Cons(x, xs), Nil())) -> c_2(dec^#(Nil())) , dec^#(Cons(Nil(), Cons(x, xs))) -> c_3(dec^#(Cons(x, xs))) , dec^#(Cons(Nil(), Nil())) -> c_4() , isNilNil^#(Cons(Cons(x', xs'), Cons(x, xs))) -> c_5() , isNilNil^#(Cons(Cons(x, xs), Nil())) -> c_6() , isNilNil^#(Cons(Nil(), Cons(x, xs))) -> c_7() , isNilNil^#(Cons(Nil(), Nil())) -> c_8() , nestdec^#(Cons(x, xs)) -> c_9(nestdec^#(dec(Cons(x, xs)))) , nestdec^#(Nil()) -> c_10() , goal^#(x) -> c_12(nestdec^#(x)) } Weak DPs: { number17^#(n) -> c_11() } Weak Trs: { dec(Cons(Cons(x', xs'), Cons(x, xs))) -> dec(Cons(x, xs)) , dec(Cons(Cons(x, xs), Nil())) -> dec(Nil()) , dec(Cons(Nil(), Cons(x, xs))) -> dec(Cons(x, xs)) , dec(Cons(Nil(), Nil())) -> Nil() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We estimate the number of application of {2,4,5,6,7,8,10} by applications of Pre({2,4,5,6,7,8,10}) = {1,3,9,11}. Here rules are labeled as follows: DPs: { 1: dec^#(Cons(Cons(x', xs'), Cons(x, xs))) -> c_1(dec^#(Cons(x, xs))) , 2: dec^#(Cons(Cons(x, xs), Nil())) -> c_2(dec^#(Nil())) , 3: dec^#(Cons(Nil(), Cons(x, xs))) -> c_3(dec^#(Cons(x, xs))) , 4: dec^#(Cons(Nil(), Nil())) -> c_4() , 5: isNilNil^#(Cons(Cons(x', xs'), Cons(x, xs))) -> c_5() , 6: isNilNil^#(Cons(Cons(x, xs), Nil())) -> c_6() , 7: isNilNil^#(Cons(Nil(), Cons(x, xs))) -> c_7() , 8: isNilNil^#(Cons(Nil(), Nil())) -> c_8() , 9: nestdec^#(Cons(x, xs)) -> c_9(nestdec^#(dec(Cons(x, xs)))) , 10: nestdec^#(Nil()) -> c_10() , 11: goal^#(x) -> c_12(nestdec^#(x)) , 12: number17^#(n) -> c_11() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { dec^#(Cons(Cons(x', xs'), Cons(x, xs))) -> c_1(dec^#(Cons(x, xs))) , dec^#(Cons(Nil(), Cons(x, xs))) -> c_3(dec^#(Cons(x, xs))) , nestdec^#(Cons(x, xs)) -> c_9(nestdec^#(dec(Cons(x, xs)))) , goal^#(x) -> c_12(nestdec^#(x)) } Weak DPs: { dec^#(Cons(Cons(x, xs), Nil())) -> c_2(dec^#(Nil())) , dec^#(Cons(Nil(), Nil())) -> c_4() , isNilNil^#(Cons(Cons(x', xs'), Cons(x, xs))) -> c_5() , isNilNil^#(Cons(Cons(x, xs), Nil())) -> c_6() , isNilNil^#(Cons(Nil(), Cons(x, xs))) -> c_7() , isNilNil^#(Cons(Nil(), Nil())) -> c_8() , nestdec^#(Nil()) -> c_10() , number17^#(n) -> c_11() } Weak Trs: { dec(Cons(Cons(x', xs'), Cons(x, xs))) -> dec(Cons(x, xs)) , dec(Cons(Cons(x, xs), Nil())) -> dec(Nil()) , dec(Cons(Nil(), Cons(x, xs))) -> dec(Cons(x, xs)) , dec(Cons(Nil(), Nil())) -> Nil() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We estimate the number of application of {3} by applications of Pre({3}) = {4}. Here rules are labeled as follows: DPs: { 1: dec^#(Cons(Cons(x', xs'), Cons(x, xs))) -> c_1(dec^#(Cons(x, xs))) , 2: dec^#(Cons(Nil(), Cons(x, xs))) -> c_3(dec^#(Cons(x, xs))) , 3: nestdec^#(Cons(x, xs)) -> c_9(nestdec^#(dec(Cons(x, xs)))) , 4: goal^#(x) -> c_12(nestdec^#(x)) , 5: dec^#(Cons(Cons(x, xs), Nil())) -> c_2(dec^#(Nil())) , 6: dec^#(Cons(Nil(), Nil())) -> c_4() , 7: isNilNil^#(Cons(Cons(x', xs'), Cons(x, xs))) -> c_5() , 8: isNilNil^#(Cons(Cons(x, xs), Nil())) -> c_6() , 9: isNilNil^#(Cons(Nil(), Cons(x, xs))) -> c_7() , 10: isNilNil^#(Cons(Nil(), Nil())) -> c_8() , 11: nestdec^#(Nil()) -> c_10() , 12: number17^#(n) -> c_11() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { dec^#(Cons(Cons(x', xs'), Cons(x, xs))) -> c_1(dec^#(Cons(x, xs))) , dec^#(Cons(Nil(), Cons(x, xs))) -> c_3(dec^#(Cons(x, xs))) , goal^#(x) -> c_12(nestdec^#(x)) } Weak DPs: { dec^#(Cons(Cons(x, xs), Nil())) -> c_2(dec^#(Nil())) , dec^#(Cons(Nil(), Nil())) -> c_4() , isNilNil^#(Cons(Cons(x', xs'), Cons(x, xs))) -> c_5() , isNilNil^#(Cons(Cons(x, xs), Nil())) -> c_6() , isNilNil^#(Cons(Nil(), Cons(x, xs))) -> c_7() , isNilNil^#(Cons(Nil(), Nil())) -> c_8() , nestdec^#(Cons(x, xs)) -> c_9(nestdec^#(dec(Cons(x, xs)))) , nestdec^#(Nil()) -> c_10() , number17^#(n) -> c_11() } Weak Trs: { dec(Cons(Cons(x', xs'), Cons(x, xs))) -> dec(Cons(x, xs)) , dec(Cons(Cons(x, xs), Nil())) -> dec(Nil()) , dec(Cons(Nil(), Cons(x, xs))) -> dec(Cons(x, xs)) , dec(Cons(Nil(), Nil())) -> Nil() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We estimate the number of application of {3} by applications of Pre({3}) = {}. Here rules are labeled as follows: DPs: { 1: dec^#(Cons(Cons(x', xs'), Cons(x, xs))) -> c_1(dec^#(Cons(x, xs))) , 2: dec^#(Cons(Nil(), Cons(x, xs))) -> c_3(dec^#(Cons(x, xs))) , 3: goal^#(x) -> c_12(nestdec^#(x)) , 4: dec^#(Cons(Cons(x, xs), Nil())) -> c_2(dec^#(Nil())) , 5: dec^#(Cons(Nil(), Nil())) -> c_4() , 6: isNilNil^#(Cons(Cons(x', xs'), Cons(x, xs))) -> c_5() , 7: isNilNil^#(Cons(Cons(x, xs), Nil())) -> c_6() , 8: isNilNil^#(Cons(Nil(), Cons(x, xs))) -> c_7() , 9: isNilNil^#(Cons(Nil(), Nil())) -> c_8() , 10: nestdec^#(Cons(x, xs)) -> c_9(nestdec^#(dec(Cons(x, xs)))) , 11: nestdec^#(Nil()) -> c_10() , 12: number17^#(n) -> c_11() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { dec^#(Cons(Cons(x', xs'), Cons(x, xs))) -> c_1(dec^#(Cons(x, xs))) , dec^#(Cons(Nil(), Cons(x, xs))) -> c_3(dec^#(Cons(x, xs))) } Weak DPs: { dec^#(Cons(Cons(x, xs), Nil())) -> c_2(dec^#(Nil())) , dec^#(Cons(Nil(), Nil())) -> c_4() , isNilNil^#(Cons(Cons(x', xs'), Cons(x, xs))) -> c_5() , isNilNil^#(Cons(Cons(x, xs), Nil())) -> c_6() , isNilNil^#(Cons(Nil(), Cons(x, xs))) -> c_7() , isNilNil^#(Cons(Nil(), Nil())) -> c_8() , nestdec^#(Cons(x, xs)) -> c_9(nestdec^#(dec(Cons(x, xs)))) , nestdec^#(Nil()) -> c_10() , number17^#(n) -> c_11() , goal^#(x) -> c_12(nestdec^#(x)) } Weak Trs: { dec(Cons(Cons(x', xs'), Cons(x, xs))) -> dec(Cons(x, xs)) , dec(Cons(Cons(x, xs), Nil())) -> dec(Nil()) , dec(Cons(Nil(), Cons(x, xs))) -> dec(Cons(x, xs)) , dec(Cons(Nil(), Nil())) -> Nil() } 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. { dec^#(Cons(Cons(x, xs), Nil())) -> c_2(dec^#(Nil())) , dec^#(Cons(Nil(), Nil())) -> c_4() , isNilNil^#(Cons(Cons(x', xs'), Cons(x, xs))) -> c_5() , isNilNil^#(Cons(Cons(x, xs), Nil())) -> c_6() , isNilNil^#(Cons(Nil(), Cons(x, xs))) -> c_7() , isNilNil^#(Cons(Nil(), Nil())) -> c_8() , nestdec^#(Cons(x, xs)) -> c_9(nestdec^#(dec(Cons(x, xs)))) , nestdec^#(Nil()) -> c_10() , number17^#(n) -> c_11() , goal^#(x) -> c_12(nestdec^#(x)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { dec^#(Cons(Cons(x', xs'), Cons(x, xs))) -> c_1(dec^#(Cons(x, xs))) , dec^#(Cons(Nil(), Cons(x, xs))) -> c_3(dec^#(Cons(x, xs))) } Weak Trs: { dec(Cons(Cons(x', xs'), Cons(x, xs))) -> dec(Cons(x, xs)) , dec(Cons(Cons(x, xs), Nil())) -> dec(Nil()) , dec(Cons(Nil(), Cons(x, xs))) -> dec(Cons(x, xs)) , dec(Cons(Nil(), Nil())) -> Nil() } 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: { dec^#(Cons(Cons(x', xs'), Cons(x, xs))) -> c_1(dec^#(Cons(x, xs))) , dec^#(Cons(Nil(), Cons(x, xs))) -> c_3(dec^#(Cons(x, 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: dec^#(Cons(Cons(x', xs'), Cons(x, xs))) -> c_1(dec^#(Cons(x, xs))) , 2: dec^#(Cons(Nil(), Cons(x, xs))) -> c_3(dec^#(Cons(x, 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(dec) = {}, safe(Cons) = {1, 2}, safe(Nil) = {}, safe(isNilNil) = {}, safe(True) = {}, safe(False) = {}, safe(nestdec) = {}, safe(number17) = {}, safe(goal) = {}, safe(dec^#) = {}, safe(c_1) = {}, safe(c_2) = {}, safe(c_3) = {}, safe(c_4) = {}, safe(isNilNil^#) = {}, safe(c_5) = {}, safe(c_6) = {}, safe(c_7) = {}, safe(c_8) = {}, safe(nestdec^#) = {}, safe(c_9) = {}, safe(c_10) = {}, safe(number17^#) = {}, safe(c_11) = {}, safe(goal^#) = {}, safe(c_12) = {} and precedence empty . Following symbols are considered recursive: {dec^#} The recursion depth is 1. Further, following argument filtering is employed: pi(dec) = [], pi(Cons) = [2], pi(Nil) = [], pi(isNilNil) = [], pi(True) = [], pi(False) = [], pi(nestdec) = [], pi(number17) = [], pi(goal) = [], pi(dec^#) = [1], pi(c_1) = [1], pi(c_2) = [], pi(c_3) = [1], pi(c_4) = [], pi(isNilNil^#) = [], pi(c_5) = [], pi(c_6) = [], pi(c_7) = [], pi(c_8) = [], pi(nestdec^#) = [], pi(c_9) = [], pi(c_10) = [], pi(number17^#) = [], pi(c_11) = [], pi(goal^#) = [], pi(c_12) = [] Usable defined function symbols are a subset of: {dec^#, isNilNil^#, nestdec^#, number17^#, goal^#} For your convenience, here are the satisfied ordering constraints: pi(dec^#(Cons(Cons(x', xs'), Cons(x, xs)))) = dec^#(Cons(; Cons(; xs));) > c_1(dec^#(Cons(; xs););) = pi(c_1(dec^#(Cons(x, xs)))) pi(dec^#(Cons(Nil(), Cons(x, xs)))) = dec^#(Cons(; Cons(; xs));) > c_3(dec^#(Cons(; xs););) = pi(c_3(dec^#(Cons(x, 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: { dec^#(Cons(Cons(x', xs'), Cons(x, xs))) -> c_1(dec^#(Cons(x, xs))) , dec^#(Cons(Nil(), Cons(x, xs))) -> c_3(dec^#(Cons(x, 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. { dec^#(Cons(Cons(x', xs'), Cons(x, xs))) -> c_1(dec^#(Cons(x, xs))) , dec^#(Cons(Nil(), Cons(x, xs))) -> c_3(dec^#(Cons(x, 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))