YES(O(1),O(n^3)) 244.40/124.92 YES(O(1),O(n^3)) 244.40/124.92 244.40/124.92 We are left with following problem, upon which TcT provides the 244.40/124.92 certificate YES(O(1),O(n^3)). 244.40/124.92 244.40/124.92 Strict Trs: 244.40/124.92 { terms(N) -> cons(recip(sqr(N)), n__terms(s(N))) 244.40/124.92 , terms(X) -> n__terms(X) 244.40/124.92 , sqr(s(X)) -> s(add(sqr(X), dbl(X))) 244.40/124.92 , sqr(0()) -> 0() 244.40/124.92 , add(s(X), Y) -> s(add(X, Y)) 244.40/124.92 , add(0(), X) -> X 244.40/124.92 , dbl(s(X)) -> s(s(dbl(X))) 244.40/124.92 , dbl(0()) -> 0() 244.40/124.92 , first(X1, X2) -> n__first(X1, X2) 244.40/124.92 , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))) 244.40/124.92 , first(0(), X) -> nil() 244.40/124.92 , activate(X) -> X 244.40/124.92 , activate(n__terms(X)) -> terms(X) 244.40/124.92 , activate(n__first(X1, X2)) -> first(X1, X2) 244.40/124.92 , half(s(s(X))) -> s(half(X)) 244.40/124.92 , half(s(0())) -> 0() 244.40/124.92 , half(0()) -> 0() 244.40/124.92 , half(dbl(X)) -> X } 244.40/124.92 Obligation: 244.40/124.92 innermost runtime complexity 244.40/124.92 Answer: 244.40/124.92 YES(O(1),O(n^3)) 244.40/124.92 244.40/124.92 We add the following dependency tuples: 244.40/124.92 244.40/124.92 Strict DPs: 244.40/124.92 { terms^#(N) -> c_1(sqr^#(N)) 244.40/124.92 , terms^#(X) -> c_2() 244.40/124.92 , sqr^#(s(X)) -> c_3(add^#(sqr(X), dbl(X)), sqr^#(X), dbl^#(X)) 244.40/124.92 , sqr^#(0()) -> c_4() 244.40/124.92 , add^#(s(X), Y) -> c_5(add^#(X, Y)) 244.40/124.92 , add^#(0(), X) -> c_6() 244.40/124.93 , dbl^#(s(X)) -> c_7(dbl^#(X)) 244.40/124.93 , dbl^#(0()) -> c_8() 244.40/124.93 , first^#(X1, X2) -> c_9() 244.40/124.93 , first^#(s(X), cons(Y, Z)) -> c_10(activate^#(Z)) 244.40/124.93 , first^#(0(), X) -> c_11() 244.40/124.93 , activate^#(X) -> c_12() 244.40/124.93 , activate^#(n__terms(X)) -> c_13(terms^#(X)) 244.40/124.93 , activate^#(n__first(X1, X2)) -> c_14(first^#(X1, X2)) 244.40/124.93 , half^#(s(s(X))) -> c_15(half^#(X)) 244.40/124.93 , half^#(s(0())) -> c_16() 244.40/124.93 , half^#(0()) -> c_17() 244.40/124.93 , half^#(dbl(X)) -> c_18() } 244.40/124.93 244.40/124.93 and mark the set of starting terms. 244.40/124.93 244.40/124.93 We are left with following problem, upon which TcT provides the 244.40/124.93 certificate YES(O(1),O(n^3)). 244.40/124.93 244.40/124.93 Strict DPs: 244.40/124.93 { terms^#(N) -> c_1(sqr^#(N)) 244.40/124.93 , terms^#(X) -> c_2() 244.40/124.93 , sqr^#(s(X)) -> c_3(add^#(sqr(X), dbl(X)), sqr^#(X), dbl^#(X)) 244.40/124.93 , sqr^#(0()) -> c_4() 244.40/124.93 , add^#(s(X), Y) -> c_5(add^#(X, Y)) 244.40/124.93 , add^#(0(), X) -> c_6() 244.40/124.93 , dbl^#(s(X)) -> c_7(dbl^#(X)) 244.40/124.93 , dbl^#(0()) -> c_8() 244.40/124.93 , first^#(X1, X2) -> c_9() 244.40/124.93 , first^#(s(X), cons(Y, Z)) -> c_10(activate^#(Z)) 244.40/124.93 , first^#(0(), X) -> c_11() 244.40/124.93 , activate^#(X) -> c_12() 244.40/124.93 , activate^#(n__terms(X)) -> c_13(terms^#(X)) 244.40/124.93 , activate^#(n__first(X1, X2)) -> c_14(first^#(X1, X2)) 244.40/124.93 , half^#(s(s(X))) -> c_15(half^#(X)) 244.40/124.93 , half^#(s(0())) -> c_16() 244.40/124.93 , half^#(0()) -> c_17() 244.40/124.93 , half^#(dbl(X)) -> c_18() } 244.40/124.93 Weak Trs: 244.40/124.93 { terms(N) -> cons(recip(sqr(N)), n__terms(s(N))) 244.40/124.93 , terms(X) -> n__terms(X) 244.40/124.93 , sqr(s(X)) -> s(add(sqr(X), dbl(X))) 244.40/124.93 , sqr(0()) -> 0() 244.40/124.93 , add(s(X), Y) -> s(add(X, Y)) 244.40/124.93 , add(0(), X) -> X 244.40/124.93 , dbl(s(X)) -> s(s(dbl(X))) 244.40/124.93 , dbl(0()) -> 0() 244.40/124.93 , first(X1, X2) -> n__first(X1, X2) 244.40/124.93 , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))) 244.40/124.93 , first(0(), X) -> nil() 244.40/124.93 , activate(X) -> X 244.40/124.93 , activate(n__terms(X)) -> terms(X) 244.40/124.93 , activate(n__first(X1, X2)) -> first(X1, X2) 244.40/124.93 , half(s(s(X))) -> s(half(X)) 244.40/124.93 , half(s(0())) -> 0() 244.40/124.93 , half(0()) -> 0() 244.40/124.93 , half(dbl(X)) -> X } 244.40/124.93 Obligation: 244.40/124.93 innermost runtime complexity 244.40/124.93 Answer: 244.40/124.93 YES(O(1),O(n^3)) 244.40/124.93 244.40/124.93 We estimate the number of application of {2,4,6,8,9,11,12,16,17,18} 244.40/124.93 by applications of Pre({2,4,6,8,9,11,12,16,17,18}) = 244.40/124.93 {1,3,5,7,10,13,14,15}. Here rules are labeled as follows: 244.40/124.93 244.40/124.93 DPs: 244.40/124.93 { 1: terms^#(N) -> c_1(sqr^#(N)) 244.40/124.93 , 2: terms^#(X) -> c_2() 244.40/124.93 , 3: sqr^#(s(X)) -> c_3(add^#(sqr(X), dbl(X)), sqr^#(X), dbl^#(X)) 244.40/124.93 , 4: sqr^#(0()) -> c_4() 244.40/124.93 , 5: add^#(s(X), Y) -> c_5(add^#(X, Y)) 244.40/124.93 , 6: add^#(0(), X) -> c_6() 244.40/124.93 , 7: dbl^#(s(X)) -> c_7(dbl^#(X)) 244.40/124.93 , 8: dbl^#(0()) -> c_8() 244.40/124.93 , 9: first^#(X1, X2) -> c_9() 244.40/124.93 , 10: first^#(s(X), cons(Y, Z)) -> c_10(activate^#(Z)) 244.40/124.93 , 11: first^#(0(), X) -> c_11() 244.40/124.93 , 12: activate^#(X) -> c_12() 244.40/124.93 , 13: activate^#(n__terms(X)) -> c_13(terms^#(X)) 244.40/124.93 , 14: activate^#(n__first(X1, X2)) -> c_14(first^#(X1, X2)) 244.40/124.93 , 15: half^#(s(s(X))) -> c_15(half^#(X)) 244.40/124.93 , 16: half^#(s(0())) -> c_16() 244.40/124.93 , 17: half^#(0()) -> c_17() 244.40/124.93 , 18: half^#(dbl(X)) -> c_18() } 244.40/124.93 244.40/124.93 We are left with following problem, upon which TcT provides the 244.40/124.93 certificate YES(O(1),O(n^3)). 244.40/124.93 244.40/124.93 Strict DPs: 244.40/124.93 { terms^#(N) -> c_1(sqr^#(N)) 244.40/124.93 , sqr^#(s(X)) -> c_3(add^#(sqr(X), dbl(X)), sqr^#(X), dbl^#(X)) 244.40/124.93 , add^#(s(X), Y) -> c_5(add^#(X, Y)) 244.40/124.93 , dbl^#(s(X)) -> c_7(dbl^#(X)) 244.40/124.93 , first^#(s(X), cons(Y, Z)) -> c_10(activate^#(Z)) 244.40/124.93 , activate^#(n__terms(X)) -> c_13(terms^#(X)) 244.40/124.93 , activate^#(n__first(X1, X2)) -> c_14(first^#(X1, X2)) 244.40/124.93 , half^#(s(s(X))) -> c_15(half^#(X)) } 244.40/124.93 Weak DPs: 244.40/124.93 { terms^#(X) -> c_2() 244.40/124.93 , sqr^#(0()) -> c_4() 244.40/124.93 , add^#(0(), X) -> c_6() 244.40/124.93 , dbl^#(0()) -> c_8() 244.40/124.93 , first^#(X1, X2) -> c_9() 244.40/124.93 , first^#(0(), X) -> c_11() 244.40/124.93 , activate^#(X) -> c_12() 244.40/124.93 , half^#(s(0())) -> c_16() 244.40/124.93 , half^#(0()) -> c_17() 244.40/124.93 , half^#(dbl(X)) -> c_18() } 244.40/124.93 Weak Trs: 244.40/124.93 { terms(N) -> cons(recip(sqr(N)), n__terms(s(N))) 244.40/124.93 , terms(X) -> n__terms(X) 244.40/124.93 , sqr(s(X)) -> s(add(sqr(X), dbl(X))) 244.40/124.93 , sqr(0()) -> 0() 244.40/124.93 , add(s(X), Y) -> s(add(X, Y)) 244.40/124.93 , add(0(), X) -> X 244.40/124.93 , dbl(s(X)) -> s(s(dbl(X))) 244.40/124.93 , dbl(0()) -> 0() 244.40/124.93 , first(X1, X2) -> n__first(X1, X2) 244.40/124.93 , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))) 244.40/124.93 , first(0(), X) -> nil() 244.40/124.93 , activate(X) -> X 244.40/124.93 , activate(n__terms(X)) -> terms(X) 244.40/124.93 , activate(n__first(X1, X2)) -> first(X1, X2) 244.40/124.93 , half(s(s(X))) -> s(half(X)) 244.40/124.93 , half(s(0())) -> 0() 244.40/124.93 , half(0()) -> 0() 244.40/124.93 , half(dbl(X)) -> X } 244.40/124.93 Obligation: 244.40/124.93 innermost runtime complexity 244.40/124.93 Answer: 244.40/124.93 YES(O(1),O(n^3)) 244.40/124.93 244.40/124.93 The following weak DPs constitute a sub-graph of the DG that is 244.40/124.93 closed under successors. The DPs are removed. 244.40/124.93 244.40/124.93 { terms^#(X) -> c_2() 244.40/124.93 , sqr^#(0()) -> c_4() 244.40/124.93 , add^#(0(), X) -> c_6() 244.40/124.93 , dbl^#(0()) -> c_8() 244.40/124.93 , first^#(X1, X2) -> c_9() 244.40/124.93 , first^#(0(), X) -> c_11() 244.40/124.93 , activate^#(X) -> c_12() 244.40/124.93 , half^#(s(0())) -> c_16() 244.40/124.93 , half^#(0()) -> c_17() 244.40/124.93 , half^#(dbl(X)) -> c_18() } 244.40/124.93 244.40/124.93 We are left with following problem, upon which TcT provides the 244.40/124.93 certificate YES(O(1),O(n^3)). 244.40/124.93 244.40/124.93 Strict DPs: 244.40/124.93 { terms^#(N) -> c_1(sqr^#(N)) 244.40/124.93 , sqr^#(s(X)) -> c_3(add^#(sqr(X), dbl(X)), sqr^#(X), dbl^#(X)) 244.40/124.93 , add^#(s(X), Y) -> c_5(add^#(X, Y)) 244.40/124.93 , dbl^#(s(X)) -> c_7(dbl^#(X)) 244.40/124.93 , first^#(s(X), cons(Y, Z)) -> c_10(activate^#(Z)) 244.40/124.93 , activate^#(n__terms(X)) -> c_13(terms^#(X)) 244.40/124.93 , activate^#(n__first(X1, X2)) -> c_14(first^#(X1, X2)) 244.40/124.93 , half^#(s(s(X))) -> c_15(half^#(X)) } 244.40/124.93 Weak Trs: 244.40/124.93 { terms(N) -> cons(recip(sqr(N)), n__terms(s(N))) 244.40/124.93 , terms(X) -> n__terms(X) 244.40/124.93 , sqr(s(X)) -> s(add(sqr(X), dbl(X))) 244.40/124.93 , sqr(0()) -> 0() 244.40/124.93 , add(s(X), Y) -> s(add(X, Y)) 244.40/124.93 , add(0(), X) -> X 244.40/124.93 , dbl(s(X)) -> s(s(dbl(X))) 244.40/124.93 , dbl(0()) -> 0() 244.40/124.93 , first(X1, X2) -> n__first(X1, X2) 244.40/124.93 , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))) 244.40/124.93 , first(0(), X) -> nil() 244.40/124.93 , activate(X) -> X 244.40/124.93 , activate(n__terms(X)) -> terms(X) 244.40/124.93 , activate(n__first(X1, X2)) -> first(X1, X2) 244.40/124.93 , half(s(s(X))) -> s(half(X)) 244.40/124.93 , half(s(0())) -> 0() 244.40/124.93 , half(0()) -> 0() 244.40/124.93 , half(dbl(X)) -> X } 244.40/124.93 Obligation: 244.40/124.93 innermost runtime complexity 244.40/124.93 Answer: 244.40/124.93 YES(O(1),O(n^3)) 244.40/124.93 244.40/124.93 We replace rewrite rules by usable rules: 244.40/124.93 244.40/124.93 Weak Usable Rules: 244.40/124.93 { sqr(s(X)) -> s(add(sqr(X), dbl(X))) 244.40/124.93 , sqr(0()) -> 0() 244.40/124.93 , add(s(X), Y) -> s(add(X, Y)) 244.40/124.93 , add(0(), X) -> X 244.40/124.93 , dbl(s(X)) -> s(s(dbl(X))) 244.40/124.93 , dbl(0()) -> 0() } 244.40/124.93 244.40/124.93 We are left with following problem, upon which TcT provides the 244.40/124.93 certificate YES(O(1),O(n^3)). 244.40/124.93 244.40/124.93 Strict DPs: 244.40/124.93 { terms^#(N) -> c_1(sqr^#(N)) 244.40/124.93 , sqr^#(s(X)) -> c_3(add^#(sqr(X), dbl(X)), sqr^#(X), dbl^#(X)) 244.40/124.93 , add^#(s(X), Y) -> c_5(add^#(X, Y)) 244.40/124.93 , dbl^#(s(X)) -> c_7(dbl^#(X)) 244.40/124.93 , first^#(s(X), cons(Y, Z)) -> c_10(activate^#(Z)) 244.40/124.93 , activate^#(n__terms(X)) -> c_13(terms^#(X)) 244.40/124.93 , activate^#(n__first(X1, X2)) -> c_14(first^#(X1, X2)) 244.40/124.93 , half^#(s(s(X))) -> c_15(half^#(X)) } 244.40/124.93 Weak Trs: 244.40/124.93 { sqr(s(X)) -> s(add(sqr(X), dbl(X))) 244.40/124.93 , sqr(0()) -> 0() 244.40/124.93 , add(s(X), Y) -> s(add(X, Y)) 244.40/124.93 , add(0(), X) -> X 244.40/124.93 , dbl(s(X)) -> s(s(dbl(X))) 244.40/124.93 , dbl(0()) -> 0() } 244.40/124.93 Obligation: 244.40/124.93 innermost runtime complexity 244.40/124.93 Answer: 244.40/124.93 YES(O(1),O(n^3)) 244.40/124.93 244.40/124.93 We use the processor 'matrix interpretation of dimension 1' to 244.40/124.93 orient following rules strictly. 244.40/124.93 244.40/124.93 DPs: 244.40/124.93 { 8: half^#(s(s(X))) -> c_15(half^#(X)) } 244.40/124.93 244.40/124.93 Sub-proof: 244.40/124.93 ---------- 244.40/124.93 The following argument positions are usable: 244.40/124.93 Uargs(c_1) = {1}, Uargs(c_3) = {1, 2, 3}, Uargs(c_5) = {1}, 244.40/124.93 Uargs(c_7) = {1}, Uargs(c_10) = {1}, Uargs(c_13) = {1}, 244.40/124.93 Uargs(c_14) = {1}, Uargs(c_15) = {1} 244.40/124.93 244.40/124.93 TcT has computed the following constructor-based matrix 244.40/124.93 interpretation satisfying not(EDA). 244.40/124.93 244.40/124.93 [cons](x1, x2) = [1] x1 + [1] x2 + [7] 244.40/124.93 244.40/124.93 [sqr](x1) = [0] 244.40/124.93 244.40/124.93 [n__terms](x1) = [1] x1 + [7] 244.40/124.93 244.40/124.93 [s](x1) = [1] x1 + [4] 244.40/124.93 244.40/124.93 [0] = [0] 244.40/124.93 244.40/124.93 [add](x1, x2) = [4] 244.40/124.93 244.40/124.93 [dbl](x1) = [0] 244.40/124.93 244.40/124.93 [n__first](x1, x2) = [1] x1 + [1] x2 + [7] 244.40/124.93 244.40/124.93 [terms^#](x1) = [0] 244.40/124.93 244.40/124.93 [c_1](x1) = [4] x1 + [0] 244.40/124.93 244.40/124.93 [sqr^#](x1) = [0] 244.40/124.93 244.40/124.93 [c_3](x1, x2, x3) = [4] x1 + [4] x2 + [1] x3 + [0] 244.40/124.93 244.40/124.93 [add^#](x1, x2) = [0] 244.40/124.93 244.40/124.93 [dbl^#](x1) = [0] 244.40/124.93 244.40/124.93 [c_5](x1) = [2] x1 + [0] 244.40/124.93 244.40/124.93 [c_7](x1) = [2] x1 + [0] 244.40/124.93 244.40/124.93 [first^#](x1, x2) = [0] 244.40/124.93 244.40/124.93 [c_10](x1) = [2] x1 + [0] 244.40/124.93 244.40/124.93 [activate^#](x1) = [0] 244.40/124.93 244.40/124.93 [c_13](x1) = [2] x1 + [0] 244.40/124.93 244.40/124.93 [c_14](x1) = [1] x1 + [0] 244.40/124.93 244.40/124.93 [half^#](x1) = [1] x1 + [0] 244.40/124.93 244.40/124.93 [c_15](x1) = [1] x1 + [5] 244.40/124.93 244.40/124.93 The order satisfies the following ordering constraints: 244.40/124.93 244.40/124.93 [sqr(s(X))] = [0] 244.40/124.93 ? [8] 244.40/124.93 = [s(add(sqr(X), dbl(X)))] 244.40/124.93 244.40/124.93 [sqr(0())] = [0] 244.40/124.93 >= [0] 244.40/124.93 = [0()] 244.40/124.93 244.40/124.93 [add(s(X), Y)] = [4] 244.40/124.93 ? [8] 244.40/124.93 = [s(add(X, Y))] 244.40/124.93 244.40/124.93 [add(0(), X)] = [4] 244.40/124.93 ? [1] X + [0] 244.40/124.93 = [X] 244.40/124.93 244.40/124.93 [dbl(s(X))] = [0] 244.40/124.93 ? [8] 244.40/124.93 = [s(s(dbl(X)))] 244.40/124.93 244.40/124.93 [dbl(0())] = [0] 244.40/124.93 >= [0] 244.40/124.93 = [0()] 244.40/124.93 244.40/124.93 [terms^#(N)] = [0] 244.40/124.93 >= [0] 244.40/124.93 = [c_1(sqr^#(N))] 244.40/124.93 244.40/124.93 [sqr^#(s(X))] = [0] 244.40/124.93 >= [0] 244.40/124.93 = [c_3(add^#(sqr(X), dbl(X)), sqr^#(X), dbl^#(X))] 244.40/124.93 244.40/124.93 [add^#(s(X), Y)] = [0] 244.40/124.93 >= [0] 244.40/124.93 = [c_5(add^#(X, Y))] 244.40/124.93 244.40/124.93 [dbl^#(s(X))] = [0] 244.40/124.93 >= [0] 244.40/124.93 = [c_7(dbl^#(X))] 244.40/124.93 244.40/124.93 [first^#(s(X), cons(Y, Z))] = [0] 244.40/124.93 >= [0] 244.40/124.93 = [c_10(activate^#(Z))] 244.40/124.93 244.40/124.93 [activate^#(n__terms(X))] = [0] 244.40/124.93 >= [0] 244.40/124.93 = [c_13(terms^#(X))] 244.40/124.93 244.40/124.93 [activate^#(n__first(X1, X2))] = [0] 244.40/124.93 >= [0] 244.40/124.93 = [c_14(first^#(X1, X2))] 244.40/124.93 244.40/124.93 [half^#(s(s(X)))] = [1] X + [8] 244.40/124.93 > [1] X + [5] 244.40/124.93 = [c_15(half^#(X))] 244.40/124.93 244.40/124.93 244.40/124.93 The strictly oriented rules are moved into the weak component. 244.40/124.93 244.40/124.93 We are left with following problem, upon which TcT provides the 244.40/124.93 certificate YES(O(1),O(n^3)). 244.40/124.93 244.40/124.93 Strict DPs: 244.40/124.93 { terms^#(N) -> c_1(sqr^#(N)) 244.40/124.93 , sqr^#(s(X)) -> c_3(add^#(sqr(X), dbl(X)), sqr^#(X), dbl^#(X)) 244.40/124.93 , add^#(s(X), Y) -> c_5(add^#(X, Y)) 244.40/124.93 , dbl^#(s(X)) -> c_7(dbl^#(X)) 244.40/124.93 , first^#(s(X), cons(Y, Z)) -> c_10(activate^#(Z)) 244.40/124.93 , activate^#(n__terms(X)) -> c_13(terms^#(X)) 244.40/124.93 , activate^#(n__first(X1, X2)) -> c_14(first^#(X1, X2)) } 244.40/124.93 Weak DPs: { half^#(s(s(X))) -> c_15(half^#(X)) } 244.40/124.93 Weak Trs: 244.40/124.93 { sqr(s(X)) -> s(add(sqr(X), dbl(X))) 244.40/124.93 , sqr(0()) -> 0() 244.40/124.93 , add(s(X), Y) -> s(add(X, Y)) 244.40/124.93 , add(0(), X) -> X 244.40/124.93 , dbl(s(X)) -> s(s(dbl(X))) 244.40/124.93 , dbl(0()) -> 0() } 244.40/124.93 Obligation: 244.40/124.93 innermost runtime complexity 244.40/124.93 Answer: 244.40/124.93 YES(O(1),O(n^3)) 244.40/124.93 244.40/124.93 The following weak DPs constitute a sub-graph of the DG that is 244.40/124.93 closed under successors. The DPs are removed. 244.40/124.93 244.40/124.93 { half^#(s(s(X))) -> c_15(half^#(X)) } 244.40/124.93 244.40/124.93 We are left with following problem, upon which TcT provides the 244.40/124.93 certificate YES(O(1),O(n^3)). 244.40/124.93 244.40/124.93 Strict DPs: 244.40/124.93 { terms^#(N) -> c_1(sqr^#(N)) 244.40/124.93 , sqr^#(s(X)) -> c_3(add^#(sqr(X), dbl(X)), sqr^#(X), dbl^#(X)) 244.40/124.93 , add^#(s(X), Y) -> c_5(add^#(X, Y)) 244.40/124.93 , dbl^#(s(X)) -> c_7(dbl^#(X)) 244.40/124.93 , first^#(s(X), cons(Y, Z)) -> c_10(activate^#(Z)) 244.40/124.93 , activate^#(n__terms(X)) -> c_13(terms^#(X)) 244.40/124.93 , activate^#(n__first(X1, X2)) -> c_14(first^#(X1, X2)) } 244.40/124.93 Weak Trs: 244.40/124.93 { sqr(s(X)) -> s(add(sqr(X), dbl(X))) 244.40/124.93 , sqr(0()) -> 0() 244.40/124.93 , add(s(X), Y) -> s(add(X, Y)) 244.40/124.93 , add(0(), X) -> X 244.40/124.93 , dbl(s(X)) -> s(s(dbl(X))) 244.40/124.93 , dbl(0()) -> 0() } 244.40/124.93 Obligation: 244.40/124.93 innermost runtime complexity 244.40/124.93 Answer: 244.40/124.93 YES(O(1),O(n^3)) 244.40/124.93 244.40/124.93 We use the processor 'matrix interpretation of dimension 2' to 244.40/124.93 orient following rules strictly. 244.40/124.93 244.40/124.93 DPs: 244.40/124.93 { 4: dbl^#(s(X)) -> c_7(dbl^#(X)) } 244.40/124.93 244.40/124.93 Sub-proof: 244.40/124.93 ---------- 244.40/124.93 The following argument positions are usable: 244.40/124.93 Uargs(c_1) = {1}, Uargs(c_3) = {1, 2, 3}, Uargs(c_5) = {1}, 244.40/124.93 Uargs(c_7) = {1}, Uargs(c_10) = {1}, Uargs(c_13) = {1}, 244.40/124.93 Uargs(c_14) = {1} 244.40/124.93 244.40/124.93 TcT has computed the following constructor-based matrix 244.40/124.93 interpretation satisfying not(EDA). 244.40/124.93 244.40/124.93 [cons](x1, x2) = [1 0] x2 + [0] 244.40/124.93 [0 0] [0] 244.40/124.93 244.40/124.93 [sqr](x1) = [0] 244.40/124.93 [0] 244.40/124.93 244.40/124.93 [n__terms](x1) = [1 0] x1 + [0] 244.40/124.93 [0 0] [0] 244.40/124.93 244.40/124.93 [s](x1) = [1 3] x1 + [0] 244.40/124.93 [0 1] [1] 244.40/124.93 244.40/124.93 [0] = [0] 244.40/124.93 [0] 244.40/124.93 244.40/124.93 [add](x1, x2) = [0] 244.40/124.93 [0] 244.40/124.93 244.40/124.93 [dbl](x1) = [0] 244.40/124.93 [0] 244.40/124.93 244.40/124.93 [n__first](x1, x2) = [1 2] x2 + [0] 244.40/124.93 [0 1] [0] 244.40/124.93 244.40/124.93 [terms^#](x1) = [5 0] x1 + [0] 244.40/124.93 [0 4] [0] 244.40/124.93 244.40/124.93 [c_1](x1) = [1 1] x1 + [0] 244.40/124.93 [0 0] [0] 244.40/124.93 244.40/124.93 [sqr^#](x1) = [3 0] x1 + [0] 244.40/124.93 [2 0] [0] 244.40/124.93 244.40/124.93 [c_3](x1, x2, x3) = [1 0] x1 + [1 0] x2 + [1 1] x3 + [0] 244.40/124.93 [0 0] [0 0] [0 0] [0] 244.40/124.93 244.40/124.93 [add^#](x1, x2) = [0] 244.40/124.93 [4] 244.40/124.93 244.40/124.93 [dbl^#](x1) = [0 1] x1 + [0] 244.40/124.93 [0 1] [0] 244.40/124.93 244.40/124.93 [c_5](x1) = [2 0] x1 + [0] 244.40/124.93 [0 0] [3] 244.40/124.93 244.40/124.93 [c_7](x1) = [1 0] x1 + [0] 244.40/124.93 [0 0] [1] 244.40/124.93 244.40/124.93 [first^#](x1, x2) = [5 0] x2 + [0] 244.40/124.93 [0 0] [0] 244.40/124.93 244.40/124.93 [c_10](x1) = [1 0] x1 + [0] 244.40/124.93 [0 0] [0] 244.40/124.93 244.40/124.93 [activate^#](x1) = [5 0] x1 + [0] 244.40/124.93 [4 0] [0] 244.40/124.93 244.40/124.93 [c_13](x1) = [1 0] x1 + [0] 244.40/124.93 [0 0] [0] 244.40/124.93 244.40/124.93 [c_14](x1) = [1 0] x1 + [0] 244.40/124.93 [0 0] [0] 244.40/124.93 244.40/124.93 [half^#](x1) = [7 7] x1 + [0] 244.40/124.93 [0 0] [0] 244.40/124.93 244.40/124.93 [c_15](x1) = [7 7] x1 + [0] 244.40/124.93 [0 0] [0] 244.40/124.93 244.40/124.93 The order satisfies the following ordering constraints: 244.40/124.93 244.40/124.93 [sqr(s(X))] = [0] 244.40/124.93 [0] 244.40/124.93 ? [0] 244.40/124.93 [1] 244.40/124.93 = [s(add(sqr(X), dbl(X)))] 244.40/124.93 244.40/124.93 [sqr(0())] = [0] 244.40/124.93 [0] 244.40/124.93 >= [0] 244.40/124.93 [0] 244.40/124.93 = [0()] 244.40/124.93 244.40/124.93 [add(s(X), Y)] = [0] 244.40/124.93 [0] 244.40/124.93 ? [0] 244.40/124.93 [1] 244.40/124.93 = [s(add(X, Y))] 244.40/124.93 244.40/124.93 [add(0(), X)] = [0] 244.40/124.93 [0] 244.40/124.93 ? [1 0] X + [0] 244.40/124.93 [0 1] [0] 244.40/124.93 = [X] 244.40/124.93 244.40/124.93 [dbl(s(X))] = [0] 244.40/124.93 [0] 244.40/124.93 ? [3] 244.40/124.93 [2] 244.40/124.93 = [s(s(dbl(X)))] 244.40/124.93 244.40/124.93 [dbl(0())] = [0] 244.40/124.93 [0] 244.40/124.93 >= [0] 244.40/124.93 [0] 244.40/124.93 = [0()] 244.40/124.93 244.40/124.93 [terms^#(N)] = [5 0] N + [0] 244.40/124.93 [0 4] [0] 244.40/124.93 >= [5 0] N + [0] 244.40/124.93 [0 0] [0] 244.40/124.93 = [c_1(sqr^#(N))] 244.40/124.93 244.40/124.93 [sqr^#(s(X))] = [3 9] X + [0] 244.40/124.93 [2 6] [0] 244.40/124.93 >= [3 2] X + [0] 244.40/124.93 [0 0] [0] 244.40/124.93 = [c_3(add^#(sqr(X), dbl(X)), sqr^#(X), dbl^#(X))] 244.40/124.93 244.40/124.93 [add^#(s(X), Y)] = [0] 244.40/124.93 [4] 244.40/124.93 >= [0] 244.40/124.93 [3] 244.40/124.93 = [c_5(add^#(X, Y))] 244.40/124.93 244.40/124.93 [dbl^#(s(X))] = [0 1] X + [1] 244.40/124.93 [0 1] [1] 244.40/124.93 > [0 1] X + [0] 244.40/124.93 [0 0] [1] 244.40/124.93 = [c_7(dbl^#(X))] 244.40/124.93 244.40/124.93 [first^#(s(X), cons(Y, Z))] = [5 0] Z + [0] 244.40/124.93 [0 0] [0] 244.40/124.93 >= [5 0] Z + [0] 244.40/124.93 [0 0] [0] 244.40/124.93 = [c_10(activate^#(Z))] 244.40/124.93 244.40/124.93 [activate^#(n__terms(X))] = [5 0] X + [0] 244.40/124.93 [4 0] [0] 244.40/124.93 >= [5 0] X + [0] 244.40/124.93 [0 0] [0] 244.40/124.93 = [c_13(terms^#(X))] 244.40/124.93 244.40/124.93 [activate^#(n__first(X1, X2))] = [5 10] X2 + [0] 244.40/124.93 [4 8] [0] 244.40/124.93 >= [5 0] X2 + [0] 244.40/124.93 [0 0] [0] 244.40/124.93 = [c_14(first^#(X1, X2))] 244.40/124.93 244.40/124.93 244.40/124.93 The strictly oriented rules are moved into the weak component. 244.40/124.93 244.40/124.93 We are left with following problem, upon which TcT provides the 244.40/124.93 certificate YES(O(1),O(n^3)). 244.40/124.93 244.40/124.93 Strict DPs: 244.40/124.93 { terms^#(N) -> c_1(sqr^#(N)) 244.40/124.93 , sqr^#(s(X)) -> c_3(add^#(sqr(X), dbl(X)), sqr^#(X), dbl^#(X)) 244.40/124.93 , add^#(s(X), Y) -> c_5(add^#(X, Y)) 244.40/124.93 , first^#(s(X), cons(Y, Z)) -> c_10(activate^#(Z)) 244.40/124.93 , activate^#(n__terms(X)) -> c_13(terms^#(X)) 244.40/124.93 , activate^#(n__first(X1, X2)) -> c_14(first^#(X1, X2)) } 244.40/124.93 Weak DPs: { dbl^#(s(X)) -> c_7(dbl^#(X)) } 244.40/124.93 Weak Trs: 244.40/124.93 { sqr(s(X)) -> s(add(sqr(X), dbl(X))) 244.40/124.93 , sqr(0()) -> 0() 244.40/124.93 , add(s(X), Y) -> s(add(X, Y)) 244.40/124.93 , add(0(), X) -> X 244.40/124.93 , dbl(s(X)) -> s(s(dbl(X))) 244.40/124.93 , dbl(0()) -> 0() } 244.40/124.93 Obligation: 244.40/124.93 innermost runtime complexity 244.40/124.93 Answer: 244.40/124.93 YES(O(1),O(n^3)) 244.40/124.93 244.40/124.93 The following weak DPs constitute a sub-graph of the DG that is 244.40/124.93 closed under successors. The DPs are removed. 244.40/124.93 244.40/124.93 { dbl^#(s(X)) -> c_7(dbl^#(X)) } 244.40/124.93 244.40/124.93 We are left with following problem, upon which TcT provides the 244.40/124.93 certificate YES(O(1),O(n^3)). 244.40/124.93 244.40/124.93 Strict DPs: 244.40/124.93 { terms^#(N) -> c_1(sqr^#(N)) 244.40/124.93 , sqr^#(s(X)) -> c_3(add^#(sqr(X), dbl(X)), sqr^#(X), dbl^#(X)) 244.40/124.93 , add^#(s(X), Y) -> c_5(add^#(X, Y)) 244.40/124.93 , first^#(s(X), cons(Y, Z)) -> c_10(activate^#(Z)) 244.40/124.93 , activate^#(n__terms(X)) -> c_13(terms^#(X)) 244.40/124.93 , activate^#(n__first(X1, X2)) -> c_14(first^#(X1, X2)) } 244.40/124.93 Weak Trs: 244.40/124.93 { sqr(s(X)) -> s(add(sqr(X), dbl(X))) 244.40/124.93 , sqr(0()) -> 0() 244.40/124.93 , add(s(X), Y) -> s(add(X, Y)) 244.40/124.93 , add(0(), X) -> X 244.40/124.93 , dbl(s(X)) -> s(s(dbl(X))) 244.40/124.93 , dbl(0()) -> 0() } 244.40/124.93 Obligation: 244.40/124.93 innermost runtime complexity 244.40/124.93 Answer: 244.40/124.93 YES(O(1),O(n^3)) 244.40/124.93 244.40/124.93 Due to missing edges in the dependency-graph, the right-hand sides 244.40/124.93 of following rules could be simplified: 244.40/124.93 244.40/124.93 { sqr^#(s(X)) -> c_3(add^#(sqr(X), dbl(X)), sqr^#(X), dbl^#(X)) } 244.40/124.93 244.40/124.93 We are left with following problem, upon which TcT provides the 244.40/124.93 certificate YES(O(1),O(n^3)). 244.40/124.93 244.40/124.93 Strict DPs: 244.40/124.93 { terms^#(N) -> c_1(sqr^#(N)) 244.40/124.93 , sqr^#(s(X)) -> c_2(add^#(sqr(X), dbl(X)), sqr^#(X)) 244.40/124.93 , add^#(s(X), Y) -> c_3(add^#(X, Y)) 244.40/124.93 , first^#(s(X), cons(Y, Z)) -> c_4(activate^#(Z)) 244.40/124.93 , activate^#(n__terms(X)) -> c_5(terms^#(X)) 244.40/124.93 , activate^#(n__first(X1, X2)) -> c_6(first^#(X1, X2)) } 244.40/124.93 Weak Trs: 244.40/124.93 { sqr(s(X)) -> s(add(sqr(X), dbl(X))) 244.40/124.93 , sqr(0()) -> 0() 244.40/124.93 , add(s(X), Y) -> s(add(X, Y)) 244.40/124.93 , add(0(), X) -> X 244.40/124.93 , dbl(s(X)) -> s(s(dbl(X))) 244.40/124.93 , dbl(0()) -> 0() } 244.40/124.93 Obligation: 244.40/124.93 innermost runtime complexity 244.40/124.93 Answer: 244.40/124.93 YES(O(1),O(n^3)) 244.40/124.93 244.40/124.93 We decompose the input problem according to the dependency graph 244.40/124.93 into the upper component 244.40/124.93 244.40/124.93 { terms^#(N) -> c_1(sqr^#(N)) 244.40/124.93 , sqr^#(s(X)) -> c_2(add^#(sqr(X), dbl(X)), sqr^#(X)) 244.40/124.93 , first^#(s(X), cons(Y, Z)) -> c_4(activate^#(Z)) 244.40/124.93 , activate^#(n__terms(X)) -> c_5(terms^#(X)) 244.40/124.93 , activate^#(n__first(X1, X2)) -> c_6(first^#(X1, X2)) } 244.40/124.93 244.40/124.93 and lower component 244.40/124.93 244.40/124.93 { add^#(s(X), Y) -> c_3(add^#(X, Y)) } 244.40/124.93 244.40/124.93 Further, following extension rules are added to the lower 244.40/124.93 component. 244.40/124.93 244.40/124.93 { terms^#(N) -> sqr^#(N) 244.40/124.93 , sqr^#(s(X)) -> sqr^#(X) 244.40/124.93 , sqr^#(s(X)) -> add^#(sqr(X), dbl(X)) 244.40/124.93 , first^#(s(X), cons(Y, Z)) -> activate^#(Z) 244.40/124.93 , activate^#(n__terms(X)) -> terms^#(X) 244.40/124.93 , activate^#(n__first(X1, X2)) -> first^#(X1, X2) } 244.40/124.93 244.40/124.93 TcT solves the upper component with certificate YES(O(1),O(n^1)). 244.40/124.93 244.40/124.93 Sub-proof: 244.40/124.93 ---------- 244.40/124.93 We are left with following problem, upon which TcT provides the 244.40/124.93 certificate YES(O(1),O(n^1)). 244.40/124.93 244.40/124.93 Strict DPs: 244.40/124.93 { terms^#(N) -> c_1(sqr^#(N)) 244.40/124.93 , sqr^#(s(X)) -> c_2(add^#(sqr(X), dbl(X)), sqr^#(X)) 244.40/124.93 , first^#(s(X), cons(Y, Z)) -> c_4(activate^#(Z)) 244.40/124.93 , activate^#(n__terms(X)) -> c_5(terms^#(X)) 244.40/124.93 , activate^#(n__first(X1, X2)) -> c_6(first^#(X1, X2)) } 244.40/124.93 Weak Trs: 244.40/124.93 { sqr(s(X)) -> s(add(sqr(X), dbl(X))) 244.40/124.93 , sqr(0()) -> 0() 244.40/124.93 , add(s(X), Y) -> s(add(X, Y)) 244.40/124.93 , add(0(), X) -> X 244.40/124.93 , dbl(s(X)) -> s(s(dbl(X))) 244.40/124.93 , dbl(0()) -> 0() } 244.40/124.93 Obligation: 244.40/124.93 innermost runtime complexity 244.40/124.93 Answer: 244.40/124.93 YES(O(1),O(n^1)) 244.40/124.93 244.40/124.93 We use the processor 'matrix interpretation of dimension 1' to 244.40/124.93 orient following rules strictly. 244.40/124.93 244.40/124.93 DPs: 244.40/124.93 { 2: sqr^#(s(X)) -> c_2(add^#(sqr(X), dbl(X)), sqr^#(X)) 244.40/124.93 , 4: activate^#(n__terms(X)) -> c_5(terms^#(X)) } 244.40/124.93 Trs: { dbl(0()) -> 0() } 244.40/124.93 244.40/124.93 Sub-proof: 244.40/124.93 ---------- 244.40/124.93 The following argument positions are usable: 244.40/124.93 Uargs(c_1) = {1}, Uargs(c_2) = {1, 2}, Uargs(c_4) = {1}, 244.40/124.93 Uargs(c_5) = {1}, Uargs(c_6) = {1} 244.40/124.93 244.40/124.93 TcT has computed the following constructor-based matrix 244.40/124.93 interpretation satisfying not(EDA). 244.40/124.93 244.40/124.93 [cons](x1, x2) = [1] x1 + [1] x2 + [0] 244.40/124.93 244.40/124.93 [sqr](x1) = [0] 244.40/124.93 244.40/124.93 [n__terms](x1) = [1] x1 + [2] 244.40/124.93 244.40/124.93 [s](x1) = [1] x1 + [1] 244.40/124.93 244.40/124.93 [0] = [0] 244.40/124.93 244.40/124.93 [add](x1, x2) = [0] 244.40/124.93 244.40/124.93 [dbl](x1) = [1] 244.40/124.93 244.40/124.93 [n__first](x1, x2) = [1] x1 + [1] x2 + [0] 244.40/124.93 244.40/124.93 [terms^#](x1) = [1] x1 + [0] 244.40/124.93 244.40/124.93 [sqr^#](x1) = [1] x1 + [0] 244.40/124.93 244.40/124.93 [add^#](x1, x2) = [0] 244.40/124.93 244.40/124.93 [first^#](x1, x2) = [2] x2 + [4] 244.40/124.93 244.40/124.93 [activate^#](x1) = [2] x1 + [4] 244.40/124.93 244.40/124.93 [c_1](x1) = [1] x1 + [0] 244.40/124.93 244.40/124.93 [c_2](x1, x2) = [2] x1 + [1] x2 + [0] 244.40/124.93 244.40/124.93 [c_4](x1) = [1] x1 + [0] 244.40/124.93 244.40/124.93 [c_5](x1) = [2] x1 + [5] 244.40/124.93 244.40/124.93 [c_6](x1) = [1] x1 + [0] 244.40/124.93 244.40/124.93 The order satisfies the following ordering constraints: 244.40/124.93 244.40/124.93 [sqr(s(X))] = [0] 244.40/124.93 ? [1] 244.40/124.93 = [s(add(sqr(X), dbl(X)))] 244.40/124.93 244.40/124.93 [sqr(0())] = [0] 244.40/124.93 >= [0] 244.40/124.93 = [0()] 244.40/124.93 244.40/124.93 [add(s(X), Y)] = [0] 244.40/124.93 ? [1] 244.40/124.93 = [s(add(X, Y))] 244.40/124.93 244.40/124.93 [add(0(), X)] = [0] 244.40/124.93 ? [1] X + [0] 244.40/124.93 = [X] 244.40/124.93 244.40/124.93 [dbl(s(X))] = [1] 244.40/124.93 ? [3] 244.40/124.93 = [s(s(dbl(X)))] 244.40/124.93 244.40/124.93 [dbl(0())] = [1] 244.40/124.93 > [0] 244.40/124.93 = [0()] 244.40/124.93 244.40/124.93 [terms^#(N)] = [1] N + [0] 244.40/124.93 >= [1] N + [0] 244.40/124.93 = [c_1(sqr^#(N))] 244.40/124.93 244.40/124.93 [sqr^#(s(X))] = [1] X + [1] 244.40/124.93 > [1] X + [0] 244.40/124.93 = [c_2(add^#(sqr(X), dbl(X)), sqr^#(X))] 244.40/124.93 244.40/124.93 [first^#(s(X), cons(Y, Z))] = [2] Y + [2] Z + [4] 244.40/124.93 >= [2] Z + [4] 244.40/124.93 = [c_4(activate^#(Z))] 244.40/124.93 244.40/124.93 [activate^#(n__terms(X))] = [2] X + [8] 244.40/124.93 > [2] X + [5] 244.40/124.93 = [c_5(terms^#(X))] 244.40/124.93 244.40/124.93 [activate^#(n__first(X1, X2))] = [2] X1 + [2] X2 + [4] 244.40/124.93 >= [2] X2 + [4] 244.40/124.93 = [c_6(first^#(X1, X2))] 244.40/124.93 244.40/124.93 244.40/124.93 We return to the main proof. Consider the set of all dependency 244.40/124.93 pairs 244.40/124.93 244.40/124.93 : 244.40/124.93 { 1: terms^#(N) -> c_1(sqr^#(N)) 244.40/124.93 , 2: sqr^#(s(X)) -> c_2(add^#(sqr(X), dbl(X)), sqr^#(X)) 244.40/124.93 , 3: first^#(s(X), cons(Y, Z)) -> c_4(activate^#(Z)) 244.40/124.93 , 4: activate^#(n__terms(X)) -> c_5(terms^#(X)) 244.40/124.93 , 5: activate^#(n__first(X1, X2)) -> c_6(first^#(X1, X2)) } 244.40/124.93 244.40/124.93 Processor 'matrix interpretation of dimension 1' induces the 244.40/124.93 complexity certificate YES(?,O(n^1)) on application of dependency 244.40/124.93 pairs {2,4}. These cover all (indirect) predecessors of dependency 244.40/124.93 pairs {1,2,4}, their number of application is equally bounded. The 244.40/124.93 dependency pairs are shifted into the weak component. 244.40/124.93 244.40/124.93 We are left with following problem, upon which TcT provides the 244.40/124.93 certificate YES(O(1),O(n^1)). 244.40/124.93 244.40/124.93 Strict DPs: 244.40/124.93 { first^#(s(X), cons(Y, Z)) -> c_4(activate^#(Z)) 244.40/124.93 , activate^#(n__first(X1, X2)) -> c_6(first^#(X1, X2)) } 244.40/124.93 Weak DPs: 244.40/124.93 { terms^#(N) -> c_1(sqr^#(N)) 244.40/124.93 , sqr^#(s(X)) -> c_2(add^#(sqr(X), dbl(X)), sqr^#(X)) 244.40/124.93 , activate^#(n__terms(X)) -> c_5(terms^#(X)) } 244.40/124.93 Weak Trs: 244.40/124.93 { sqr(s(X)) -> s(add(sqr(X), dbl(X))) 244.40/124.93 , sqr(0()) -> 0() 244.40/124.93 , add(s(X), Y) -> s(add(X, Y)) 244.40/124.93 , add(0(), X) -> X 244.40/124.93 , dbl(s(X)) -> s(s(dbl(X))) 244.40/124.93 , dbl(0()) -> 0() } 244.40/124.93 Obligation: 244.40/124.93 innermost runtime complexity 244.40/124.93 Answer: 244.40/124.93 YES(O(1),O(n^1)) 244.40/124.93 244.40/124.93 The following weak DPs constitute a sub-graph of the DG that is 244.40/124.93 closed under successors. The DPs are removed. 244.40/124.93 244.40/124.93 { terms^#(N) -> c_1(sqr^#(N)) 244.40/124.93 , sqr^#(s(X)) -> c_2(add^#(sqr(X), dbl(X)), sqr^#(X)) 244.40/124.93 , activate^#(n__terms(X)) -> c_5(terms^#(X)) } 244.40/124.93 244.40/124.93 We are left with following problem, upon which TcT provides the 244.40/124.93 certificate YES(O(1),O(n^1)). 244.40/124.93 244.40/124.93 Strict DPs: 244.40/124.93 { first^#(s(X), cons(Y, Z)) -> c_4(activate^#(Z)) 244.40/124.93 , activate^#(n__first(X1, X2)) -> c_6(first^#(X1, X2)) } 244.40/124.93 Weak Trs: 244.40/124.93 { sqr(s(X)) -> s(add(sqr(X), dbl(X))) 244.40/124.93 , sqr(0()) -> 0() 244.40/124.93 , add(s(X), Y) -> s(add(X, Y)) 244.40/124.93 , add(0(), X) -> X 244.40/124.93 , dbl(s(X)) -> s(s(dbl(X))) 244.40/124.93 , dbl(0()) -> 0() } 244.40/124.93 Obligation: 244.40/124.93 innermost runtime complexity 244.40/124.93 Answer: 244.40/124.93 YES(O(1),O(n^1)) 244.40/124.93 244.40/124.93 No rule is usable, rules are removed from the input problem. 244.40/124.93 244.40/124.93 We are left with following problem, upon which TcT provides the 244.40/124.93 certificate YES(O(1),O(n^1)). 244.40/124.93 244.40/124.93 Strict DPs: 244.40/124.93 { first^#(s(X), cons(Y, Z)) -> c_4(activate^#(Z)) 244.40/124.93 , activate^#(n__first(X1, X2)) -> c_6(first^#(X1, X2)) } 244.40/124.93 Obligation: 244.40/124.93 innermost runtime complexity 244.40/124.93 Answer: 244.40/124.93 YES(O(1),O(n^1)) 244.40/124.93 244.40/124.93 We use the processor 'Small Polynomial Path Order (PS,1-bounded)' 244.40/124.93 to orient following rules strictly. 244.40/124.93 244.40/124.93 DPs: 244.40/124.93 { 1: first^#(s(X), cons(Y, Z)) -> c_4(activate^#(Z)) 244.40/124.93 , 2: activate^#(n__first(X1, X2)) -> c_6(first^#(X1, X2)) } 244.40/124.93 244.40/124.93 Sub-proof: 244.40/124.93 ---------- 244.40/124.93 The input was oriented with the instance of 'Small Polynomial Path 244.40/124.93 Order (PS,1-bounded)' as induced by the safe mapping 244.40/124.93 244.40/124.93 safe(cons) = {1, 2}, safe(sqr) = {}, safe(n__terms) = {1}, 244.40/124.93 safe(s) = {1}, safe(0) = {}, safe(add) = {}, safe(dbl) = {}, 244.40/124.93 safe(n__first) = {1, 2}, safe(terms^#) = {}, safe(sqr^#) = {}, 244.40/124.93 safe(add^#) = {}, safe(first^#) = {1}, safe(activate^#) = {}, 244.40/124.93 safe(c_1) = {}, safe(c_2) = {}, safe(c_4) = {}, safe(c_5) = {}, 244.40/124.93 safe(c_6) = {} 244.40/124.93 244.40/124.93 and precedence 244.40/124.93 244.40/124.93 first^# ~ activate^# . 244.40/124.93 244.40/124.93 Following symbols are considered recursive: 244.40/124.93 244.40/124.93 {first^#, activate^#} 244.40/124.93 244.40/124.93 The recursion depth is 1. 244.40/124.93 244.40/124.93 Further, following argument filtering is employed: 244.40/124.93 244.40/124.93 pi(cons) = [2], pi(sqr) = [], pi(n__terms) = [], pi(s) = 1, 244.40/124.93 pi(0) = [], pi(add) = [], pi(dbl) = [], pi(n__first) = [2], 244.40/124.93 pi(terms^#) = [], pi(sqr^#) = [], pi(add^#) = [], 244.40/124.93 pi(first^#) = [2], pi(activate^#) = [1], pi(c_1) = [], 244.40/124.93 pi(c_2) = [], pi(c_4) = [1], pi(c_5) = [], pi(c_6) = [1] 244.40/124.93 244.40/124.93 Usable defined function symbols are a subset of: 244.40/124.93 244.40/124.93 {terms^#, sqr^#, add^#, first^#, activate^#} 244.40/124.93 244.40/124.93 For your convenience, here are the satisfied ordering constraints: 244.40/124.93 244.40/124.93 pi(first^#(s(X), cons(Y, Z))) = first^#(cons(; Z);) 244.40/124.93 > c_4(activate^#(Z;);) 244.40/124.93 = pi(c_4(activate^#(Z))) 244.40/124.93 244.40/124.93 pi(activate^#(n__first(X1, X2))) = activate^#(n__first(; X2);) 244.40/124.93 > c_6(first^#(X2;);) 244.40/124.93 = pi(c_6(first^#(X1, X2))) 244.40/124.93 244.40/124.93 244.40/124.93 The strictly oriented rules are moved into the weak component. 244.40/124.93 244.40/124.93 We are left with following problem, upon which TcT provides the 244.40/124.93 certificate YES(O(1),O(1)). 244.40/124.93 244.40/124.93 Weak DPs: 244.40/124.93 { first^#(s(X), cons(Y, Z)) -> c_4(activate^#(Z)) 244.40/124.93 , activate^#(n__first(X1, X2)) -> c_6(first^#(X1, X2)) } 244.40/124.93 Obligation: 244.40/124.93 innermost runtime complexity 244.40/124.93 Answer: 244.40/124.93 YES(O(1),O(1)) 244.40/124.93 244.40/124.93 The following weak DPs constitute a sub-graph of the DG that is 244.40/124.93 closed under successors. The DPs are removed. 244.40/124.93 244.40/124.93 { first^#(s(X), cons(Y, Z)) -> c_4(activate^#(Z)) 244.40/124.93 , activate^#(n__first(X1, X2)) -> c_6(first^#(X1, X2)) } 244.40/124.93 244.40/124.93 We are left with following problem, upon which TcT provides the 244.40/124.93 certificate YES(O(1),O(1)). 244.40/124.93 244.40/124.93 Rules: Empty 244.40/124.93 Obligation: 244.40/124.93 innermost runtime complexity 244.40/124.93 Answer: 244.40/124.93 YES(O(1),O(1)) 244.40/124.93 244.40/124.93 Empty rules are trivially bounded 244.40/124.93 244.40/124.93 We return to the main proof. 244.40/124.93 244.40/124.93 We are left with following problem, upon which TcT provides the 244.40/124.93 certificate YES(O(1),O(n^2)). 244.40/124.93 244.40/124.93 Strict DPs: { add^#(s(X), Y) -> c_3(add^#(X, Y)) } 244.40/124.93 Weak DPs: 244.40/124.93 { terms^#(N) -> sqr^#(N) 244.40/124.93 , sqr^#(s(X)) -> sqr^#(X) 244.40/124.93 , sqr^#(s(X)) -> add^#(sqr(X), dbl(X)) 244.40/124.93 , first^#(s(X), cons(Y, Z)) -> activate^#(Z) 244.40/124.93 , activate^#(n__terms(X)) -> terms^#(X) 244.40/124.93 , activate^#(n__first(X1, X2)) -> first^#(X1, X2) } 244.40/124.93 Weak Trs: 244.40/124.93 { sqr(s(X)) -> s(add(sqr(X), dbl(X))) 244.40/124.93 , sqr(0()) -> 0() 244.40/124.93 , add(s(X), Y) -> s(add(X, Y)) 244.40/124.93 , add(0(), X) -> X 244.40/124.93 , dbl(s(X)) -> s(s(dbl(X))) 244.40/124.93 , dbl(0()) -> 0() } 244.40/124.93 Obligation: 244.40/124.93 innermost runtime complexity 244.40/124.93 Answer: 244.40/124.93 YES(O(1),O(n^2)) 244.40/124.93 244.40/124.93 We use the processor 'polynomial interpretation' to orient 244.40/124.93 following rules strictly. 244.40/124.93 244.40/124.93 DPs: 244.40/124.93 { 1: add^#(s(X), Y) -> c_3(add^#(X, Y)) 244.40/124.93 , 3: sqr^#(s(X)) -> sqr^#(X) 244.40/124.93 , 4: sqr^#(s(X)) -> add^#(sqr(X), dbl(X)) } 244.40/124.93 Trs: { sqr(s(X)) -> s(add(sqr(X), dbl(X))) } 244.40/124.93 244.40/124.93 Sub-proof: 244.40/124.93 ---------- 244.40/124.93 We consider the following typing: 244.40/124.93 244.40/124.93 cons :: (a,d) -> c 244.40/124.93 sqr :: b -> b 244.40/124.93 n__terms :: b -> d 244.40/124.93 s :: b -> b 244.40/124.93 0 :: b 244.40/124.93 add :: (b,b) -> b 244.40/124.93 dbl :: b -> b 244.40/124.93 n__first :: (b,c) -> d 244.40/124.93 terms^# :: b -> e 244.40/124.93 sqr^# :: b -> e 244.40/124.93 add^# :: (b,b) -> e 244.40/124.93 first^# :: (b,c) -> e 244.40/124.93 activate^# :: d -> e 244.40/124.93 c_3 :: e -> e 244.40/124.93 244.40/124.93 The following argument positions are considered usable: 244.40/124.93 244.40/124.93 Uargs(c_3) = {1} 244.40/124.93 244.40/124.93 TcT has computed the following constructor-restricted 244.40/124.93 typedpolynomial interpretation. 244.40/124.93 244.40/124.93 [cons](x1, x2) = 3*x1 + x2 244.40/124.93 244.40/124.93 [sqr](x1) = x1^2 244.40/124.93 244.40/124.93 [n__terms](x1) = x1 244.40/124.93 244.40/124.93 [s](x1) = 2 + x1 244.40/124.93 244.40/124.93 [0]() = 0 244.40/124.93 244.40/124.93 [add](x1, x2) = x1 + 2*x2 244.40/124.93 244.40/124.93 [dbl](x1) = 2*x1 244.40/124.93 244.40/124.93 [n__first](x1, x2) = x2 244.40/124.93 244.40/124.93 [terms^#](x1) = x1^2 244.40/124.93 244.40/124.93 [sqr^#](x1) = x1^2 244.40/124.93 244.40/124.93 [add^#](x1, x2) = x1 244.40/124.93 244.40/124.93 [first^#](x1, x2) = x2^2 244.40/124.93 244.40/124.93 [activate^#](x1) = x1^2 244.40/124.93 244.40/124.93 [c_3](x1) = x1 244.40/124.93 244.40/124.93 244.40/124.93 This order satisfies the following ordering constraints. 244.40/124.93 244.40/124.93 [sqr(s(X))] = 4 + 4*X + X^2 244.40/124.93 > 2 + X^2 + 4*X 244.40/124.93 = [s(add(sqr(X), dbl(X)))] 244.40/124.93 244.40/124.93 [sqr(0())] = 244.40/124.93 >= 244.40/124.93 = [0()] 244.40/124.93 244.40/124.93 [add(s(X), Y)] = 2 + X + 2*Y 244.40/124.93 >= 2 + X + 2*Y 244.40/124.93 = [s(add(X, Y))] 244.40/124.93 244.40/124.93 [add(0(), X)] = 2*X 244.40/124.93 >= X 244.40/124.93 = [X] 244.40/124.93 244.40/124.93 [dbl(s(X))] = 4 + 2*X 244.40/124.93 >= 4 + 2*X 244.40/124.93 = [s(s(dbl(X)))] 244.40/124.93 244.40/124.93 [dbl(0())] = 244.40/124.93 >= 244.40/124.93 = [0()] 244.40/124.93 244.40/124.93 [terms^#(N)] = N^2 244.40/124.93 >= N^2 244.40/124.93 = [sqr^#(N)] 244.40/124.93 244.40/124.93 [sqr^#(s(X))] = 4 + 4*X + X^2 244.40/124.93 > X^2 244.40/124.93 = [sqr^#(X)] 244.40/124.93 244.40/124.93 [sqr^#(s(X))] = 4 + 4*X + X^2 244.40/124.93 > X^2 244.40/124.93 = [add^#(sqr(X), dbl(X))] 244.40/124.93 244.40/124.93 [add^#(s(X), Y)] = 2 + X 244.40/124.93 > X 244.40/124.93 = [c_3(add^#(X, Y))] 244.40/124.93 244.40/124.93 [first^#(s(X), cons(Y, Z))] = 9*Y^2 + 3*Y*Z + 3*Z*Y + Z^2 244.40/124.93 >= Z^2 244.40/124.93 = [activate^#(Z)] 244.40/124.93 244.40/124.93 [activate^#(n__terms(X))] = X^2 244.40/124.93 >= X^2 244.40/124.93 = [terms^#(X)] 244.40/124.93 244.40/124.93 [activate^#(n__first(X1, X2))] = X2^2 244.40/124.93 >= X2^2 244.40/124.93 = [first^#(X1, X2)] 244.40/124.93 244.40/124.93 244.40/124.93 The strictly oriented rules are moved into the weak component. 244.40/124.93 244.40/124.93 We are left with following problem, upon which TcT provides the 244.40/124.93 certificate YES(O(1),O(1)). 244.40/124.93 244.40/124.93 Weak DPs: 244.40/124.93 { terms^#(N) -> sqr^#(N) 244.40/124.93 , sqr^#(s(X)) -> sqr^#(X) 244.40/124.93 , sqr^#(s(X)) -> add^#(sqr(X), dbl(X)) 244.40/124.93 , add^#(s(X), Y) -> c_3(add^#(X, Y)) 244.40/124.93 , first^#(s(X), cons(Y, Z)) -> activate^#(Z) 244.40/124.93 , activate^#(n__terms(X)) -> terms^#(X) 244.40/124.93 , activate^#(n__first(X1, X2)) -> first^#(X1, X2) } 244.40/124.93 Weak Trs: 244.40/124.93 { sqr(s(X)) -> s(add(sqr(X), dbl(X))) 244.40/124.93 , sqr(0()) -> 0() 244.40/124.93 , add(s(X), Y) -> s(add(X, Y)) 244.40/124.93 , add(0(), X) -> X 244.40/124.93 , dbl(s(X)) -> s(s(dbl(X))) 244.40/124.93 , dbl(0()) -> 0() } 244.40/124.93 Obligation: 244.40/124.93 innermost runtime complexity 244.40/124.93 Answer: 244.40/124.93 YES(O(1),O(1)) 244.40/124.93 244.40/124.93 The following weak DPs constitute a sub-graph of the DG that is 244.40/124.93 closed under successors. The DPs are removed. 244.40/124.93 244.40/124.93 { terms^#(N) -> sqr^#(N) 244.40/124.93 , sqr^#(s(X)) -> sqr^#(X) 244.40/124.93 , sqr^#(s(X)) -> add^#(sqr(X), dbl(X)) 244.40/124.93 , add^#(s(X), Y) -> c_3(add^#(X, Y)) 244.40/124.93 , first^#(s(X), cons(Y, Z)) -> activate^#(Z) 244.40/124.93 , activate^#(n__terms(X)) -> terms^#(X) 244.40/124.93 , activate^#(n__first(X1, X2)) -> first^#(X1, X2) } 244.40/124.93 244.40/124.93 We are left with following problem, upon which TcT provides the 244.40/124.93 certificate YES(O(1),O(1)). 244.40/124.93 244.40/124.93 Weak Trs: 244.40/124.93 { sqr(s(X)) -> s(add(sqr(X), dbl(X))) 244.40/124.93 , sqr(0()) -> 0() 244.40/124.93 , add(s(X), Y) -> s(add(X, Y)) 244.40/124.93 , add(0(), X) -> X 244.40/124.93 , dbl(s(X)) -> s(s(dbl(X))) 244.40/124.93 , dbl(0()) -> 0() } 244.40/124.93 Obligation: 244.40/124.93 innermost runtime complexity 244.40/124.93 Answer: 244.40/124.93 YES(O(1),O(1)) 244.40/124.93 244.40/124.93 No rule is usable, rules are removed from the input problem. 244.40/124.93 244.40/124.93 We are left with following problem, upon which TcT provides the 244.40/124.93 certificate YES(O(1),O(1)). 244.40/124.93 244.40/124.93 Rules: Empty 244.40/124.93 Obligation: 244.40/124.93 innermost runtime complexity 244.40/124.93 Answer: 244.40/124.93 YES(O(1),O(1)) 244.40/124.93 244.40/124.93 Empty rules are trivially bounded 244.40/124.93 244.40/124.93 Hurray, we answered YES(O(1),O(n^3)) 244.40/124.94 EOF