MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { terms(N) -> cons(recip(sqr(N)), terms(s(N))) , sqr(s(X)) -> s(add(sqr(X), dbl(X))) , sqr(0()) -> 0() , add(s(X), Y) -> s(add(X, Y)) , add(0(), X) -> X , dbl(s(X)) -> s(s(dbl(X))) , dbl(0()) -> 0() , first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)) , first(0(), X) -> nil() } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { terms^#(N) -> c_1(sqr^#(N), terms^#(s(N))) , sqr^#(s(X)) -> c_2(add^#(sqr(X), dbl(X)), sqr^#(X), dbl^#(X)) , sqr^#(0()) -> c_3() , add^#(s(X), Y) -> c_4(add^#(X, Y)) , add^#(0(), X) -> c_5() , dbl^#(s(X)) -> c_6(dbl^#(X)) , dbl^#(0()) -> c_7() , first^#(s(X), cons(Y, Z)) -> c_8(first^#(X, Z)) , first^#(0(), X) -> c_9() } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { terms^#(N) -> c_1(sqr^#(N), terms^#(s(N))) , sqr^#(s(X)) -> c_2(add^#(sqr(X), dbl(X)), sqr^#(X), dbl^#(X)) , sqr^#(0()) -> c_3() , add^#(s(X), Y) -> c_4(add^#(X, Y)) , add^#(0(), X) -> c_5() , dbl^#(s(X)) -> c_6(dbl^#(X)) , dbl^#(0()) -> c_7() , first^#(s(X), cons(Y, Z)) -> c_8(first^#(X, Z)) , first^#(0(), X) -> c_9() } Weak Trs: { terms(N) -> cons(recip(sqr(N)), terms(s(N))) , sqr(s(X)) -> s(add(sqr(X), dbl(X))) , sqr(0()) -> 0() , add(s(X), Y) -> s(add(X, Y)) , add(0(), X) -> X , dbl(s(X)) -> s(s(dbl(X))) , dbl(0()) -> 0() , first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)) , first(0(), X) -> nil() } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {3,5,7,9} by applications of Pre({3,5,7,9}) = {1,2,4,6,8}. Here rules are labeled as follows: DPs: { 1: terms^#(N) -> c_1(sqr^#(N), terms^#(s(N))) , 2: sqr^#(s(X)) -> c_2(add^#(sqr(X), dbl(X)), sqr^#(X), dbl^#(X)) , 3: sqr^#(0()) -> c_3() , 4: add^#(s(X), Y) -> c_4(add^#(X, Y)) , 5: add^#(0(), X) -> c_5() , 6: dbl^#(s(X)) -> c_6(dbl^#(X)) , 7: dbl^#(0()) -> c_7() , 8: first^#(s(X), cons(Y, Z)) -> c_8(first^#(X, Z)) , 9: first^#(0(), X) -> c_9() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { terms^#(N) -> c_1(sqr^#(N), terms^#(s(N))) , sqr^#(s(X)) -> c_2(add^#(sqr(X), dbl(X)), sqr^#(X), dbl^#(X)) , add^#(s(X), Y) -> c_4(add^#(X, Y)) , dbl^#(s(X)) -> c_6(dbl^#(X)) , first^#(s(X), cons(Y, Z)) -> c_8(first^#(X, Z)) } Weak DPs: { sqr^#(0()) -> c_3() , add^#(0(), X) -> c_5() , dbl^#(0()) -> c_7() , first^#(0(), X) -> c_9() } Weak Trs: { terms(N) -> cons(recip(sqr(N)), terms(s(N))) , sqr(s(X)) -> s(add(sqr(X), dbl(X))) , sqr(0()) -> 0() , add(s(X), Y) -> s(add(X, Y)) , add(0(), X) -> X , dbl(s(X)) -> s(s(dbl(X))) , dbl(0()) -> 0() , first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)) , first(0(), X) -> nil() } Obligation: innermost runtime complexity Answer: MAYBE The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { sqr^#(0()) -> c_3() , add^#(0(), X) -> c_5() , dbl^#(0()) -> c_7() , first^#(0(), X) -> c_9() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { terms^#(N) -> c_1(sqr^#(N), terms^#(s(N))) , sqr^#(s(X)) -> c_2(add^#(sqr(X), dbl(X)), sqr^#(X), dbl^#(X)) , add^#(s(X), Y) -> c_4(add^#(X, Y)) , dbl^#(s(X)) -> c_6(dbl^#(X)) , first^#(s(X), cons(Y, Z)) -> c_8(first^#(X, Z)) } Weak Trs: { terms(N) -> cons(recip(sqr(N)), terms(s(N))) , sqr(s(X)) -> s(add(sqr(X), dbl(X))) , sqr(0()) -> 0() , add(s(X), Y) -> s(add(X, Y)) , add(0(), X) -> X , dbl(s(X)) -> s(s(dbl(X))) , dbl(0()) -> 0() , first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)) , first(0(), X) -> nil() } Obligation: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Weak Usable Rules: { sqr(s(X)) -> s(add(sqr(X), dbl(X))) , sqr(0()) -> 0() , add(s(X), Y) -> s(add(X, Y)) , add(0(), X) -> X , dbl(s(X)) -> s(s(dbl(X))) , dbl(0()) -> 0() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { terms^#(N) -> c_1(sqr^#(N), terms^#(s(N))) , sqr^#(s(X)) -> c_2(add^#(sqr(X), dbl(X)), sqr^#(X), dbl^#(X)) , add^#(s(X), Y) -> c_4(add^#(X, Y)) , dbl^#(s(X)) -> c_6(dbl^#(X)) , first^#(s(X), cons(Y, Z)) -> c_8(first^#(X, Z)) } Weak Trs: { sqr(s(X)) -> s(add(sqr(X), dbl(X))) , sqr(0()) -> 0() , add(s(X), Y) -> s(add(X, Y)) , add(0(), X) -> X , dbl(s(X)) -> s(s(dbl(X))) , dbl(0()) -> 0() } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..