MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { from(X) -> cons(X, from(s(X))) , 2ndspos(s(N), cons(X, Z)) -> 2ndspos(s(N), cons2(X, Z)) , 2ndspos(s(N), cons2(X, cons(Y, Z))) -> rcons(posrecip(Y), 2ndsneg(N, Z)) , 2ndspos(0(), Z) -> rnil() , 2ndsneg(s(N), cons(X, Z)) -> 2ndsneg(s(N), cons2(X, Z)) , 2ndsneg(s(N), cons2(X, cons(Y, Z))) -> rcons(negrecip(Y), 2ndspos(N, Z)) , 2ndsneg(0(), Z) -> rnil() , pi(X) -> 2ndspos(X, from(0())) , plus(s(X), Y) -> s(plus(X, Y)) , plus(0(), Y) -> Y , times(s(X), Y) -> plus(Y, times(X, Y)) , times(0(), Y) -> 0() , square(X) -> times(X, X) } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { from^#(X) -> c_1(from^#(s(X))) , 2ndspos^#(s(N), cons(X, Z)) -> c_2(2ndspos^#(s(N), cons2(X, Z))) , 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> c_3(2ndsneg^#(N, Z)) , 2ndspos^#(0(), Z) -> c_4() , 2ndsneg^#(s(N), cons(X, Z)) -> c_5(2ndsneg^#(s(N), cons2(X, Z))) , 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> c_6(2ndspos^#(N, Z)) , 2ndsneg^#(0(), Z) -> c_7() , pi^#(X) -> c_8(2ndspos^#(X, from(0())), from^#(0())) , plus^#(s(X), Y) -> c_9(plus^#(X, Y)) , plus^#(0(), Y) -> c_10() , times^#(s(X), Y) -> c_11(plus^#(Y, times(X, Y)), times^#(X, Y)) , times^#(0(), Y) -> c_12() , square^#(X) -> c_13(times^#(X, X)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { from^#(X) -> c_1(from^#(s(X))) , 2ndspos^#(s(N), cons(X, Z)) -> c_2(2ndspos^#(s(N), cons2(X, Z))) , 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> c_3(2ndsneg^#(N, Z)) , 2ndspos^#(0(), Z) -> c_4() , 2ndsneg^#(s(N), cons(X, Z)) -> c_5(2ndsneg^#(s(N), cons2(X, Z))) , 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> c_6(2ndspos^#(N, Z)) , 2ndsneg^#(0(), Z) -> c_7() , pi^#(X) -> c_8(2ndspos^#(X, from(0())), from^#(0())) , plus^#(s(X), Y) -> c_9(plus^#(X, Y)) , plus^#(0(), Y) -> c_10() , times^#(s(X), Y) -> c_11(plus^#(Y, times(X, Y)), times^#(X, Y)) , times^#(0(), Y) -> c_12() , square^#(X) -> c_13(times^#(X, X)) } Weak Trs: { from(X) -> cons(X, from(s(X))) , 2ndspos(s(N), cons(X, Z)) -> 2ndspos(s(N), cons2(X, Z)) , 2ndspos(s(N), cons2(X, cons(Y, Z))) -> rcons(posrecip(Y), 2ndsneg(N, Z)) , 2ndspos(0(), Z) -> rnil() , 2ndsneg(s(N), cons(X, Z)) -> 2ndsneg(s(N), cons2(X, Z)) , 2ndsneg(s(N), cons2(X, cons(Y, Z))) -> rcons(negrecip(Y), 2ndspos(N, Z)) , 2ndsneg(0(), Z) -> rnil() , pi(X) -> 2ndspos(X, from(0())) , plus(s(X), Y) -> s(plus(X, Y)) , plus(0(), Y) -> Y , times(s(X), Y) -> plus(Y, times(X, Y)) , times(0(), Y) -> 0() , square(X) -> times(X, X) } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {4,7,10,12} by applications of Pre({4,7,10,12}) = {3,6,8,9,11,13}. Here rules are labeled as follows: DPs: { 1: from^#(X) -> c_1(from^#(s(X))) , 2: 2ndspos^#(s(N), cons(X, Z)) -> c_2(2ndspos^#(s(N), cons2(X, Z))) , 3: 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> c_3(2ndsneg^#(N, Z)) , 4: 2ndspos^#(0(), Z) -> c_4() , 5: 2ndsneg^#(s(N), cons(X, Z)) -> c_5(2ndsneg^#(s(N), cons2(X, Z))) , 6: 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> c_6(2ndspos^#(N, Z)) , 7: 2ndsneg^#(0(), Z) -> c_7() , 8: pi^#(X) -> c_8(2ndspos^#(X, from(0())), from^#(0())) , 9: plus^#(s(X), Y) -> c_9(plus^#(X, Y)) , 10: plus^#(0(), Y) -> c_10() , 11: times^#(s(X), Y) -> c_11(plus^#(Y, times(X, Y)), times^#(X, Y)) , 12: times^#(0(), Y) -> c_12() , 13: square^#(X) -> c_13(times^#(X, X)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { from^#(X) -> c_1(from^#(s(X))) , 2ndspos^#(s(N), cons(X, Z)) -> c_2(2ndspos^#(s(N), cons2(X, Z))) , 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> c_3(2ndsneg^#(N, Z)) , 2ndsneg^#(s(N), cons(X, Z)) -> c_5(2ndsneg^#(s(N), cons2(X, Z))) , 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> c_6(2ndspos^#(N, Z)) , pi^#(X) -> c_8(2ndspos^#(X, from(0())), from^#(0())) , plus^#(s(X), Y) -> c_9(plus^#(X, Y)) , times^#(s(X), Y) -> c_11(plus^#(Y, times(X, Y)), times^#(X, Y)) , square^#(X) -> c_13(times^#(X, X)) } Weak DPs: { 2ndspos^#(0(), Z) -> c_4() , 2ndsneg^#(0(), Z) -> c_7() , plus^#(0(), Y) -> c_10() , times^#(0(), Y) -> c_12() } Weak Trs: { from(X) -> cons(X, from(s(X))) , 2ndspos(s(N), cons(X, Z)) -> 2ndspos(s(N), cons2(X, Z)) , 2ndspos(s(N), cons2(X, cons(Y, Z))) -> rcons(posrecip(Y), 2ndsneg(N, Z)) , 2ndspos(0(), Z) -> rnil() , 2ndsneg(s(N), cons(X, Z)) -> 2ndsneg(s(N), cons2(X, Z)) , 2ndsneg(s(N), cons2(X, cons(Y, Z))) -> rcons(negrecip(Y), 2ndspos(N, Z)) , 2ndsneg(0(), Z) -> rnil() , pi(X) -> 2ndspos(X, from(0())) , plus(s(X), Y) -> s(plus(X, Y)) , plus(0(), Y) -> Y , times(s(X), Y) -> plus(Y, times(X, Y)) , times(0(), Y) -> 0() , square(X) -> times(X, X) } 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. { 2ndspos^#(0(), Z) -> c_4() , 2ndsneg^#(0(), Z) -> c_7() , plus^#(0(), Y) -> c_10() , times^#(0(), Y) -> c_12() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { from^#(X) -> c_1(from^#(s(X))) , 2ndspos^#(s(N), cons(X, Z)) -> c_2(2ndspos^#(s(N), cons2(X, Z))) , 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> c_3(2ndsneg^#(N, Z)) , 2ndsneg^#(s(N), cons(X, Z)) -> c_5(2ndsneg^#(s(N), cons2(X, Z))) , 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> c_6(2ndspos^#(N, Z)) , pi^#(X) -> c_8(2ndspos^#(X, from(0())), from^#(0())) , plus^#(s(X), Y) -> c_9(plus^#(X, Y)) , times^#(s(X), Y) -> c_11(plus^#(Y, times(X, Y)), times^#(X, Y)) , square^#(X) -> c_13(times^#(X, X)) } Weak Trs: { from(X) -> cons(X, from(s(X))) , 2ndspos(s(N), cons(X, Z)) -> 2ndspos(s(N), cons2(X, Z)) , 2ndspos(s(N), cons2(X, cons(Y, Z))) -> rcons(posrecip(Y), 2ndsneg(N, Z)) , 2ndspos(0(), Z) -> rnil() , 2ndsneg(s(N), cons(X, Z)) -> 2ndsneg(s(N), cons2(X, Z)) , 2ndsneg(s(N), cons2(X, cons(Y, Z))) -> rcons(negrecip(Y), 2ndspos(N, Z)) , 2ndsneg(0(), Z) -> rnil() , pi(X) -> 2ndspos(X, from(0())) , plus(s(X), Y) -> s(plus(X, Y)) , plus(0(), Y) -> Y , times(s(X), Y) -> plus(Y, times(X, Y)) , times(0(), Y) -> 0() , square(X) -> times(X, X) } Obligation: innermost runtime complexity Answer: MAYBE Consider the dependency graph 1: from^#(X) -> c_1(from^#(s(X))) -->_1 from^#(X) -> c_1(from^#(s(X))) :1 2: 2ndspos^#(s(N), cons(X, Z)) -> c_2(2ndspos^#(s(N), cons2(X, Z))) -->_1 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> c_3(2ndsneg^#(N, Z)) :3 3: 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> c_3(2ndsneg^#(N, Z)) -->_1 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> c_6(2ndspos^#(N, Z)) :5 -->_1 2ndsneg^#(s(N), cons(X, Z)) -> c_5(2ndsneg^#(s(N), cons2(X, Z))) :4 4: 2ndsneg^#(s(N), cons(X, Z)) -> c_5(2ndsneg^#(s(N), cons2(X, Z))) -->_1 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> c_6(2ndspos^#(N, Z)) :5 5: 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> c_6(2ndspos^#(N, Z)) -->_1 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> c_3(2ndsneg^#(N, Z)) :3 -->_1 2ndspos^#(s(N), cons(X, Z)) -> c_2(2ndspos^#(s(N), cons2(X, Z))) :2 6: pi^#(X) -> c_8(2ndspos^#(X, from(0())), from^#(0())) -->_1 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> c_3(2ndsneg^#(N, Z)) :3 -->_1 2ndspos^#(s(N), cons(X, Z)) -> c_2(2ndspos^#(s(N), cons2(X, Z))) :2 -->_2 from^#(X) -> c_1(from^#(s(X))) :1 7: plus^#(s(X), Y) -> c_9(plus^#(X, Y)) -->_1 plus^#(s(X), Y) -> c_9(plus^#(X, Y)) :7 8: times^#(s(X), Y) -> c_11(plus^#(Y, times(X, Y)), times^#(X, Y)) -->_2 times^#(s(X), Y) -> c_11(plus^#(Y, times(X, Y)), times^#(X, Y)) :8 -->_1 plus^#(s(X), Y) -> c_9(plus^#(X, Y)) :7 9: square^#(X) -> c_13(times^#(X, X)) -->_1 times^#(s(X), Y) -> c_11(plus^#(Y, times(X, Y)), times^#(X, Y)) :8 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). { square^#(X) -> c_13(times^#(X, X)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { from^#(X) -> c_1(from^#(s(X))) , 2ndspos^#(s(N), cons(X, Z)) -> c_2(2ndspos^#(s(N), cons2(X, Z))) , 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> c_3(2ndsneg^#(N, Z)) , 2ndsneg^#(s(N), cons(X, Z)) -> c_5(2ndsneg^#(s(N), cons2(X, Z))) , 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> c_6(2ndspos^#(N, Z)) , pi^#(X) -> c_8(2ndspos^#(X, from(0())), from^#(0())) , plus^#(s(X), Y) -> c_9(plus^#(X, Y)) , times^#(s(X), Y) -> c_11(plus^#(Y, times(X, Y)), times^#(X, Y)) } Weak Trs: { from(X) -> cons(X, from(s(X))) , 2ndspos(s(N), cons(X, Z)) -> 2ndspos(s(N), cons2(X, Z)) , 2ndspos(s(N), cons2(X, cons(Y, Z))) -> rcons(posrecip(Y), 2ndsneg(N, Z)) , 2ndspos(0(), Z) -> rnil() , 2ndsneg(s(N), cons(X, Z)) -> 2ndsneg(s(N), cons2(X, Z)) , 2ndsneg(s(N), cons2(X, cons(Y, Z))) -> rcons(negrecip(Y), 2ndspos(N, Z)) , 2ndsneg(0(), Z) -> rnil() , pi(X) -> 2ndspos(X, from(0())) , plus(s(X), Y) -> s(plus(X, Y)) , plus(0(), Y) -> Y , times(s(X), Y) -> plus(Y, times(X, Y)) , times(0(), Y) -> 0() , square(X) -> times(X, X) } Obligation: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Weak Usable Rules: { from(X) -> cons(X, from(s(X))) , plus(s(X), Y) -> s(plus(X, Y)) , plus(0(), Y) -> Y , times(s(X), Y) -> plus(Y, times(X, Y)) , times(0(), Y) -> 0() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { from^#(X) -> c_1(from^#(s(X))) , 2ndspos^#(s(N), cons(X, Z)) -> c_2(2ndspos^#(s(N), cons2(X, Z))) , 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> c_3(2ndsneg^#(N, Z)) , 2ndsneg^#(s(N), cons(X, Z)) -> c_5(2ndsneg^#(s(N), cons2(X, Z))) , 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> c_6(2ndspos^#(N, Z)) , pi^#(X) -> c_8(2ndspos^#(X, from(0())), from^#(0())) , plus^#(s(X), Y) -> c_9(plus^#(X, Y)) , times^#(s(X), Y) -> c_11(plus^#(Y, times(X, Y)), times^#(X, Y)) } Weak Trs: { from(X) -> cons(X, from(s(X))) , plus(s(X), Y) -> s(plus(X, Y)) , plus(0(), Y) -> Y , times(s(X), Y) -> plus(Y, times(X, Y)) , times(0(), Y) -> 0() } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..