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