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