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