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 None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 60 seconds)' failed due to the following reason: We add the 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 analyse the complexity of following sub-problems (R) and (S). Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component: Problem (R): ------------ Strict DPs: { 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())) } Weak DPs: { from^#(X) -> c_1(from^#(s(X))) , 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) } StartTerms: basic terms Defined Symbols: from^# 2ndspos^# 2ndsneg^# pi^# plus^# times^# square^# Constructors: cons s 0 rnil cons2 rcons posrecip negrecip Strategy: innermost Problem (S): ------------ Strict DPs: { from^#(X) -> c_1(from^#(s(X))) , plus^#(s(X), Y) -> c_9(plus^#(X, Y)) , times^#(s(X), Y) -> c_11(plus^#(Y, times(X, Y)), times^#(X, Y)) } Weak DPs: { 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())) } 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) } StartTerms: basic terms Defined Symbols: from^# 2ndspos^# 2ndsneg^# pi^# plus^# times^# square^# Constructors: cons s 0 rnil cons2 rcons posrecip negrecip Strategy: innermost Overall, the transformation results in the following sub-problem(s): Generated new problems: ----------------------- R) Strict DPs: { 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())) } Weak DPs: { from^#(X) -> c_1(from^#(s(X))) , 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) } StartTerms: basic terms Defined Symbols: from^# 2ndspos^# 2ndsneg^# pi^# plus^# times^# square^# Constructors: cons s 0 rnil cons2 rcons posrecip negrecip Strategy: innermost This problem was proven YES(O(1),O(n^1)). S) Strict DPs: { from^#(X) -> c_1(from^#(s(X))) , plus^#(s(X), Y) -> c_9(plus^#(X, Y)) , times^#(s(X), Y) -> c_11(plus^#(Y, times(X, Y)), times^#(X, Y)) } Weak DPs: { 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())) } 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) } StartTerms: basic terms Defined Symbols: from^# 2ndspos^# 2ndsneg^# pi^# plus^# times^# square^# Constructors: cons s 0 rnil cons2 rcons posrecip negrecip Strategy: innermost This problem remains open. Proofs for generated problems: ------------------------------ R) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { 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())) } Weak DPs: { from^#(X) -> c_1(from^#(s(X))) , 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: YES(O(1),O(n^1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { from^#(X) -> c_1(from^#(s(X))) , plus^#(s(X), Y) -> c_9(plus^#(X, Y)) , times^#(s(X), Y) -> c_11(plus^#(Y, times(X, Y)), times^#(X, Y)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { 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())) } 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: YES(O(1),O(n^1)) Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { pi^#(X) -> c_8(2ndspos^#(X, from(0())), from^#(0())) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { 2ndspos^#(s(N), cons(X, Z)) -> c_1(2ndspos^#(s(N), cons2(X, Z))) , 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> c_2(2ndsneg^#(N, Z)) , 2ndsneg^#(s(N), cons(X, Z)) -> c_3(2ndsneg^#(s(N), cons2(X, Z))) , 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> c_4(2ndspos^#(N, Z)) , pi^#(X) -> c_5(2ndspos^#(X, from(0()))) } 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: YES(O(1),O(n^1)) We replace rewrite rules by usable rules: Weak Usable Rules: { from(X) -> cons(X, from(s(X))) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { 2ndspos^#(s(N), cons(X, Z)) -> c_1(2ndspos^#(s(N), cons2(X, Z))) , 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> c_2(2ndsneg^#(N, Z)) , 2ndsneg^#(s(N), cons(X, Z)) -> c_3(2ndsneg^#(s(N), cons2(X, Z))) , 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> c_4(2ndspos^#(N, Z)) , pi^#(X) -> c_5(2ndspos^#(X, from(0()))) } Weak Trs: { from(X) -> cons(X, from(s(X))) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 2: 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> c_2(2ndsneg^#(N, Z)) , 4: 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> c_4(2ndspos^#(N, Z)) } Sub-proof: ---------- The following argument positions are usable: Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1}, Uargs(c_4) = {1}, Uargs(c_5) = {1} TcT has computed the following constructor-based matrix interpretation satisfying not(EDA). [from](x1) = [0] [cons](x1, x2) = [0] [s](x1) = [1] x1 + [4] [2ndspos](x1, x2) = [7] x1 + [7] x2 + [0] [0] = [6] [rnil] = [0] [cons2](x1, x2) = [1] x1 + [0] [rcons](x1, x2) = [1] x1 + [1] x2 + [0] [posrecip](x1) = [1] x1 + [0] [2ndsneg](x1, x2) = [7] x1 + [7] x2 + [0] [negrecip](x1) = [1] x1 + [0] [pi](x1) = [7] x1 + [0] [plus](x1, x2) = [7] x1 + [7] x2 + [0] [times](x1, x2) = [7] x1 + [7] x2 + [0] [square](x1) = [7] x1 + [0] [from^#](x1) = [7] x1 + [0] [c_1](x1) = [7] x1 + [0] [2ndspos^#](x1, x2) = [2] x1 + [0] [c_2](x1) = [7] x1 + [0] [c_3](x1) = [7] x1 + [0] [2ndsneg^#](x1, x2) = [2] x1 + [0] [c_4] = [0] [c_5](x1) = [7] x1 + [0] [c_6](x1) = [7] x1 + [0] [c_7] = [0] [pi^#](x1) = [7] x1 + [7] [c_8](x1, x2) = [7] x1 + [7] x2 + [0] [plus^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_9](x1) = [7] x1 + [0] [c_10] = [0] [times^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_11](x1, x2) = [7] x1 + [7] x2 + [0] [c_12] = [0] [square^#](x1) = [7] x1 + [0] [c_13](x1) = [7] x1 + [0] [c] = [0] [c_1](x1) = [1] x1 + [0] [c_2](x1) = [1] x1 + [7] [c_3](x1) = [1] x1 + [0] [c_4](x1) = [1] x1 + [5] [c_5](x1) = [2] x1 + [7] The following symbols are considered usable {from, 2ndspos^#, 2ndsneg^#, pi^#} The order satisfies the following ordering constraints: [from(X)] = [0] >= [0] = [cons(X, from(s(X)))] [2ndspos^#(s(N), cons(X, Z))] = [2] N + [8] >= [2] N + [8] = [c_1(2ndspos^#(s(N), cons2(X, Z)))] [2ndspos^#(s(N), cons2(X, cons(Y, Z)))] = [2] N + [8] > [2] N + [7] = [c_2(2ndsneg^#(N, Z))] [2ndsneg^#(s(N), cons(X, Z))] = [2] N + [8] >= [2] N + [8] = [c_3(2ndsneg^#(s(N), cons2(X, Z)))] [2ndsneg^#(s(N), cons2(X, cons(Y, Z)))] = [2] N + [8] > [2] N + [5] = [c_4(2ndspos^#(N, Z))] [pi^#(X)] = [7] X + [7] >= [4] X + [7] = [c_5(2ndspos^#(X, from(0())))] We return to the main proof. Consider the set of all dependency pairs : { 1: 2ndspos^#(s(N), cons(X, Z)) -> c_1(2ndspos^#(s(N), cons2(X, Z))) , 2: 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> c_2(2ndsneg^#(N, Z)) , 3: 2ndsneg^#(s(N), cons(X, Z)) -> c_3(2ndsneg^#(s(N), cons2(X, Z))) , 4: 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> c_4(2ndspos^#(N, Z)) , 5: pi^#(X) -> c_5(2ndspos^#(X, from(0()))) } Processor 'matrix interpretation of dimension 1' induces the complexity certificate YES(?,O(n^1)) on application of dependency pairs {2,4}. These cover all (indirect) predecessors of dependency pairs {1,2,3,4,5}, their number of application is equally bounded. The dependency pairs are shifted into the weak component. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak DPs: { 2ndspos^#(s(N), cons(X, Z)) -> c_1(2ndspos^#(s(N), cons2(X, Z))) , 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> c_2(2ndsneg^#(N, Z)) , 2ndsneg^#(s(N), cons(X, Z)) -> c_3(2ndsneg^#(s(N), cons2(X, Z))) , 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> c_4(2ndspos^#(N, Z)) , pi^#(X) -> c_5(2ndspos^#(X, from(0()))) } Weak Trs: { from(X) -> cons(X, from(s(X))) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { 2ndspos^#(s(N), cons(X, Z)) -> c_1(2ndspos^#(s(N), cons2(X, Z))) , 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> c_2(2ndsneg^#(N, Z)) , 2ndsneg^#(s(N), cons(X, Z)) -> c_3(2ndsneg^#(s(N), cons2(X, Z))) , 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> c_4(2ndspos^#(N, Z)) , pi^#(X) -> c_5(2ndspos^#(X, from(0()))) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak Trs: { from(X) -> cons(X, from(s(X))) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded S) We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { from^#(X) -> c_1(from^#(s(X))) , plus^#(s(X), Y) -> c_9(plus^#(X, Y)) , times^#(s(X), Y) -> c_11(plus^#(Y, times(X, Y)), times^#(X, Y)) } Weak DPs: { 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())) } 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^#(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)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { from^#(X) -> c_1(from^#(s(X))) , plus^#(s(X), Y) -> c_9(plus^#(X, Y)) , times^#(s(X), Y) -> c_11(plus^#(Y, times(X, Y)), times^#(X, Y)) } Weak DPs: { pi^#(X) -> c_8(2ndspos^#(X, from(0())), from^#(0())) } 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 Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { pi^#(X) -> c_8(2ndspos^#(X, from(0())), from^#(0())) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { from^#(X) -> c_1(from^#(s(X))) , plus^#(s(X), Y) -> c_2(plus^#(X, Y)) , times^#(s(X), Y) -> c_3(plus^#(Y, times(X, Y)), times^#(X, Y)) } Weak DPs: { pi^#(X) -> c_4(from^#(0())) } 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: { 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))) , plus^#(s(X), Y) -> c_2(plus^#(X, Y)) , times^#(s(X), Y) -> c_3(plus^#(Y, times(X, Y)), times^#(X, Y)) } Weak DPs: { pi^#(X) -> c_4(from^#(0())) } Weak Trs: { 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 We analyse the complexity of following sub-problems (R) and (S). Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component: Problem (R): ------------ Strict DPs: { from^#(X) -> c_1(from^#(s(X))) } Weak DPs: { pi^#(X) -> c_4(from^#(0())) , plus^#(s(X), Y) -> c_2(plus^#(X, Y)) , times^#(s(X), Y) -> c_3(plus^#(Y, times(X, Y)), times^#(X, Y)) } Weak Trs: { 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() } StartTerms: basic terms Defined Symbols: from^# 2ndspos^# 2ndsneg^# pi^# plus^# times^# square^# Constructors: cons s 0 rnil cons2 rcons posrecip negrecip Strategy: innermost Problem (S): ------------ Strict DPs: { plus^#(s(X), Y) -> c_2(plus^#(X, Y)) , times^#(s(X), Y) -> c_3(plus^#(Y, times(X, Y)), times^#(X, Y)) } Weak DPs: { from^#(X) -> c_1(from^#(s(X))) , pi^#(X) -> c_4(from^#(0())) } Weak Trs: { 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() } StartTerms: basic terms Defined Symbols: from^# 2ndspos^# 2ndsneg^# pi^# plus^# times^# square^# Constructors: cons s 0 rnil cons2 rcons posrecip negrecip Strategy: innermost Overall, the transformation results in the following sub-problem(s): Generated new problems: ----------------------- R) Strict DPs: { from^#(X) -> c_1(from^#(s(X))) } Weak DPs: { pi^#(X) -> c_4(from^#(0())) , plus^#(s(X), Y) -> c_2(plus^#(X, Y)) , times^#(s(X), Y) -> c_3(plus^#(Y, times(X, Y)), times^#(X, Y)) } Weak Trs: { 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() } StartTerms: basic terms Defined Symbols: from^# 2ndspos^# 2ndsneg^# pi^# plus^# times^# square^# Constructors: cons s 0 rnil cons2 rcons posrecip negrecip Strategy: innermost This problem remains open. S) Strict DPs: { plus^#(s(X), Y) -> c_2(plus^#(X, Y)) , times^#(s(X), Y) -> c_3(plus^#(Y, times(X, Y)), times^#(X, Y)) } Weak DPs: { from^#(X) -> c_1(from^#(s(X))) , pi^#(X) -> c_4(from^#(0())) } Weak Trs: { 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() } StartTerms: basic terms Defined Symbols: from^# 2ndspos^# 2ndsneg^# pi^# plus^# times^# square^# Constructors: cons s 0 rnil cons2 rcons posrecip negrecip Strategy: innermost This problem was proven YES(O(1),O(n^2)). Proofs for generated problems: ------------------------------ R) We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { from^#(X) -> c_1(from^#(s(X))) } Weak DPs: { pi^#(X) -> c_4(from^#(0())) , plus^#(s(X), Y) -> c_2(plus^#(X, Y)) , times^#(s(X), Y) -> c_3(plus^#(Y, times(X, Y)), times^#(X, Y)) } Weak Trs: { 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 following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { plus^#(s(X), Y) -> c_2(plus^#(X, Y)) , times^#(s(X), Y) -> c_3(plus^#(Y, times(X, Y)), times^#(X, Y)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { from^#(X) -> c_1(from^#(s(X))) } Weak DPs: { pi^#(X) -> c_4(from^#(0())) } Weak Trs: { 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 No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { from^#(X) -> c_1(from^#(s(X))) } Weak DPs: { pi^#(X) -> c_4(from^#(0())) } Obligation: innermost runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'WithProblem' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Fastest' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Polynomial Path Order (PS)' failed due to the following reason: The input cannot be shown compatible 2) 'Fastest (timeout of 5 seconds)' failed due to the following reason: Computation stopped due to timeout after 5.0 seconds. 3) 'Polynomial Path Order (PS)' failed due to the following reason: The input cannot be shown compatible S) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { plus^#(s(X), Y) -> c_2(plus^#(X, Y)) , times^#(s(X), Y) -> c_3(plus^#(Y, times(X, Y)), times^#(X, Y)) } Weak DPs: { from^#(X) -> c_1(from^#(s(X))) , pi^#(X) -> c_4(from^#(0())) } Weak Trs: { 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: YES(O(1),O(n^2)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { from^#(X) -> c_1(from^#(s(X))) , pi^#(X) -> c_4(from^#(0())) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { plus^#(s(X), Y) -> c_2(plus^#(X, Y)) , times^#(s(X), Y) -> c_3(plus^#(Y, times(X, Y)), times^#(X, Y)) } Weak Trs: { 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: YES(O(1),O(n^2)) We use the processor 'Small Polynomial Path Order (PS,2-bounded)' to orient following rules strictly. DPs: { 1: plus^#(s(X), Y) -> c_2(plus^#(X, Y)) , 2: times^#(s(X), Y) -> c_3(plus^#(Y, times(X, Y)), times^#(X, Y)) } Trs: { times(0(), Y) -> 0() } Sub-proof: ---------- The input was oriented with the instance of 'Small Polynomial Path Order (PS,2-bounded)' as induced by the safe mapping safe(from) = {}, safe(cons) = {1, 2}, safe(s) = {1}, safe(2ndspos) = {}, safe(0) = {}, safe(rnil) = {}, safe(cons2) = {1, 2}, safe(rcons) = {1, 2}, safe(posrecip) = {1}, safe(2ndsneg) = {}, safe(negrecip) = {1}, safe(pi) = {}, safe(plus) = {}, safe(times) = {}, safe(square) = {}, safe(from^#) = {}, safe(c_1) = {}, safe(2ndspos^#) = {}, safe(c_2) = {}, safe(c_3) = {}, safe(2ndsneg^#) = {}, safe(c_4) = {}, safe(c_5) = {}, safe(c_6) = {}, safe(c_7) = {}, safe(pi^#) = {}, safe(c_8) = {}, safe(plus^#) = {2}, safe(c_9) = {}, safe(c_10) = {}, safe(times^#) = {}, safe(c_11) = {}, safe(c_12) = {}, safe(square^#) = {}, safe(c_13) = {}, safe(c) = {}, safe(c_1) = {}, safe(c_2) = {}, safe(c_3) = {}, safe(c_4) = {} and precedence times > plus, times > plus^#, times^# > plus, times^# > plus^#, plus ~ plus^#, times ~ times^# . Following symbols are considered recursive: {plus, times, plus^#, times^#} The recursion depth is 2. Further, following argument filtering is employed: pi(from) = [], pi(cons) = [], pi(s) = [1], pi(2ndspos) = [], pi(0) = [], pi(rnil) = [], pi(cons2) = [], pi(rcons) = [], pi(posrecip) = [], pi(2ndsneg) = [], pi(negrecip) = [], pi(pi) = [], pi(plus) = [1], pi(times) = [1], pi(square) = [], pi(from^#) = [], pi(c_1) = [], pi(2ndspos^#) = [], pi(c_2) = [], pi(c_3) = [], pi(2ndsneg^#) = [], pi(c_4) = [], pi(c_5) = [], pi(c_6) = [], pi(c_7) = [], pi(pi^#) = [], pi(c_8) = [], pi(plus^#) = [1], pi(c_9) = [], pi(c_10) = [], pi(times^#) = [1, 2], pi(c_11) = [], pi(c_12) = [], pi(square^#) = [], pi(c_13) = [], pi(c) = [], pi(c_1) = [], pi(c_2) = [1], pi(c_3) = [1, 2], pi(c_4) = [] Usable defined function symbols are a subset of: {from^#, 2ndspos^#, 2ndsneg^#, pi^#, plus^#, times^#, square^#} For your convenience, here are the satisfied ordering constraints: pi(plus^#(s(X), Y)) = plus^#(s(; X);) > c_2(plus^#(X;);) = pi(c_2(plus^#(X, Y))) pi(times^#(s(X), Y)) = times^#(s(; X), Y;) > c_3(plus^#(Y;), times^#(X, Y;);) = pi(c_3(plus^#(Y, times(X, Y)), times^#(X, Y))) The strictly oriented rules are moved into the weak component. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak DPs: { plus^#(s(X), Y) -> c_2(plus^#(X, Y)) , times^#(s(X), Y) -> c_3(plus^#(Y, times(X, Y)), times^#(X, Y)) } Weak Trs: { 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: YES(O(1),O(1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { plus^#(s(X), Y) -> c_2(plus^#(X, Y)) , times^#(s(X), Y) -> c_3(plus^#(Y, times(X, Y)), times^#(X, Y)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak Trs: { 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: YES(O(1),O(1)) No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 30.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'bsearch-popstar (timeout of 60 seconds)' failed due to the following reason: The input cannot be shown compatible 2) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due to the following reason: The input cannot be shown compatible 3) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. Arrrr..