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, cons(Y, Z))) -> rcons(posrecip(Y), 2ndsneg(N, Z)) , 2ndspos(0(), Z) -> rnil() , 2ndsneg(s(N), cons(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) '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. 2) '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, cons(Y, Z))) -> c_2(2ndsneg^#(N, Z)) , 2ndspos^#(0(), Z) -> c_3() , 2ndsneg^#(s(N), cons(X, cons(Y, Z))) -> c_4(2ndspos^#(N, Z)) , 2ndsneg^#(0(), Z) -> c_5() , pi^#(X) -> c_6(2ndspos^#(X, from(0())), from^#(0())) , plus^#(s(X), Y) -> c_7(plus^#(X, Y)) , plus^#(0(), Y) -> c_8() , times^#(s(X), Y) -> c_9(plus^#(Y, times(X, Y)), times^#(X, Y)) , times^#(0(), Y) -> c_10() , square^#(X) -> c_11(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, cons(Y, Z))) -> c_2(2ndsneg^#(N, Z)) , 2ndspos^#(0(), Z) -> c_3() , 2ndsneg^#(s(N), cons(X, cons(Y, Z))) -> c_4(2ndspos^#(N, Z)) , 2ndsneg^#(0(), Z) -> c_5() , pi^#(X) -> c_6(2ndspos^#(X, from(0())), from^#(0())) , plus^#(s(X), Y) -> c_7(plus^#(X, Y)) , plus^#(0(), Y) -> c_8() , times^#(s(X), Y) -> c_9(plus^#(Y, times(X, Y)), times^#(X, Y)) , times^#(0(), Y) -> c_10() , square^#(X) -> c_11(times^#(X, X)) } Weak Trs: { from(X) -> cons(X, from(s(X))) , 2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(Y), 2ndsneg(N, Z)) , 2ndspos(0(), Z) -> rnil() , 2ndsneg(s(N), cons(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 {3,5,8,10} by applications of Pre({3,5,8,10}) = {2,4,6,7,9,11}. Here rules are labeled as follows: DPs: { 1: from^#(X) -> c_1(from^#(s(X))) , 2: 2ndspos^#(s(N), cons(X, cons(Y, Z))) -> c_2(2ndsneg^#(N, Z)) , 3: 2ndspos^#(0(), Z) -> c_3() , 4: 2ndsneg^#(s(N), cons(X, cons(Y, Z))) -> c_4(2ndspos^#(N, Z)) , 5: 2ndsneg^#(0(), Z) -> c_5() , 6: pi^#(X) -> c_6(2ndspos^#(X, from(0())), from^#(0())) , 7: plus^#(s(X), Y) -> c_7(plus^#(X, Y)) , 8: plus^#(0(), Y) -> c_8() , 9: times^#(s(X), Y) -> c_9(plus^#(Y, times(X, Y)), times^#(X, Y)) , 10: times^#(0(), Y) -> c_10() , 11: square^#(X) -> c_11(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, cons(Y, Z))) -> c_2(2ndsneg^#(N, Z)) , 2ndsneg^#(s(N), cons(X, cons(Y, Z))) -> c_4(2ndspos^#(N, Z)) , pi^#(X) -> c_6(2ndspos^#(X, from(0())), from^#(0())) , plus^#(s(X), Y) -> c_7(plus^#(X, Y)) , times^#(s(X), Y) -> c_9(plus^#(Y, times(X, Y)), times^#(X, Y)) , square^#(X) -> c_11(times^#(X, X)) } Weak DPs: { 2ndspos^#(0(), Z) -> c_3() , 2ndsneg^#(0(), Z) -> c_5() , plus^#(0(), Y) -> c_8() , times^#(0(), Y) -> c_10() } Weak Trs: { from(X) -> cons(X, from(s(X))) , 2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(Y), 2ndsneg(N, Z)) , 2ndspos(0(), Z) -> rnil() , 2ndsneg(s(N), cons(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_3() , 2ndsneg^#(0(), Z) -> c_5() , plus^#(0(), Y) -> c_8() , times^#(0(), Y) -> c_10() } 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, cons(Y, Z))) -> c_2(2ndsneg^#(N, Z)) , 2ndsneg^#(s(N), cons(X, cons(Y, Z))) -> c_4(2ndspos^#(N, Z)) , pi^#(X) -> c_6(2ndspos^#(X, from(0())), from^#(0())) , plus^#(s(X), Y) -> c_7(plus^#(X, Y)) , times^#(s(X), Y) -> c_9(plus^#(Y, times(X, Y)), times^#(X, Y)) , square^#(X) -> c_11(times^#(X, X)) } Weak Trs: { from(X) -> cons(X, from(s(X))) , 2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(Y), 2ndsneg(N, Z)) , 2ndspos(0(), Z) -> rnil() , 2ndsneg(s(N), cons(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, cons(Y, Z))) -> c_2(2ndsneg^#(N, Z)) -->_1 2ndsneg^#(s(N), cons(X, cons(Y, Z))) -> c_4(2ndspos^#(N, Z)) :3 3: 2ndsneg^#(s(N), cons(X, cons(Y, Z))) -> c_4(2ndspos^#(N, Z)) -->_1 2ndspos^#(s(N), cons(X, cons(Y, Z))) -> c_2(2ndsneg^#(N, Z)) :2 4: pi^#(X) -> c_6(2ndspos^#(X, from(0())), from^#(0())) -->_1 2ndspos^#(s(N), cons(X, cons(Y, Z))) -> c_2(2ndsneg^#(N, Z)) :2 -->_2 from^#(X) -> c_1(from^#(s(X))) :1 5: plus^#(s(X), Y) -> c_7(plus^#(X, Y)) -->_1 plus^#(s(X), Y) -> c_7(plus^#(X, Y)) :5 6: times^#(s(X), Y) -> c_9(plus^#(Y, times(X, Y)), times^#(X, Y)) -->_2 times^#(s(X), Y) -> c_9(plus^#(Y, times(X, Y)), times^#(X, Y)) :6 -->_1 plus^#(s(X), Y) -> c_7(plus^#(X, Y)) :5 7: square^#(X) -> c_11(times^#(X, X)) -->_1 times^#(s(X), Y) -> c_9(plus^#(Y, times(X, Y)), times^#(X, Y)) :6 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_11(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, cons(Y, Z))) -> c_2(2ndsneg^#(N, Z)) , 2ndsneg^#(s(N), cons(X, cons(Y, Z))) -> c_4(2ndspos^#(N, Z)) , pi^#(X) -> c_6(2ndspos^#(X, from(0())), from^#(0())) , plus^#(s(X), Y) -> c_7(plus^#(X, Y)) , times^#(s(X), Y) -> c_9(plus^#(Y, times(X, Y)), times^#(X, Y)) } Weak Trs: { from(X) -> cons(X, from(s(X))) , 2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(Y), 2ndsneg(N, Z)) , 2ndspos(0(), Z) -> rnil() , 2ndsneg(s(N), cons(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, cons(Y, Z))) -> c_2(2ndsneg^#(N, Z)) , 2ndsneg^#(s(N), cons(X, cons(Y, Z))) -> c_4(2ndspos^#(N, Z)) , pi^#(X) -> c_6(2ndspos^#(X, from(0())), from^#(0())) } Weak DPs: { from^#(X) -> c_1(from^#(s(X))) , plus^#(s(X), Y) -> c_7(plus^#(X, Y)) , times^#(s(X), Y) -> c_9(plus^#(Y, times(X, Y)), times^#(X, Y)) } Weak Trs: { from(X) -> cons(X, from(s(X))) , 2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(Y), 2ndsneg(N, Z)) , 2ndspos(0(), Z) -> rnil() , 2ndsneg(s(N), cons(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 rcons posrecip negrecip Strategy: innermost Problem (S): ------------ Strict DPs: { from^#(X) -> c_1(from^#(s(X))) , plus^#(s(X), Y) -> c_7(plus^#(X, Y)) , times^#(s(X), Y) -> c_9(plus^#(Y, times(X, Y)), times^#(X, Y)) } Weak DPs: { 2ndspos^#(s(N), cons(X, cons(Y, Z))) -> c_2(2ndsneg^#(N, Z)) , 2ndsneg^#(s(N), cons(X, cons(Y, Z))) -> c_4(2ndspos^#(N, Z)) , pi^#(X) -> c_6(2ndspos^#(X, from(0())), from^#(0())) } Weak Trs: { from(X) -> cons(X, from(s(X))) , 2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(Y), 2ndsneg(N, Z)) , 2ndspos(0(), Z) -> rnil() , 2ndsneg(s(N), cons(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 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, cons(Y, Z))) -> c_2(2ndsneg^#(N, Z)) , 2ndsneg^#(s(N), cons(X, cons(Y, Z))) -> c_4(2ndspos^#(N, Z)) , pi^#(X) -> c_6(2ndspos^#(X, from(0())), from^#(0())) } Weak DPs: { from^#(X) -> c_1(from^#(s(X))) , plus^#(s(X), Y) -> c_7(plus^#(X, Y)) , times^#(s(X), Y) -> c_9(plus^#(Y, times(X, Y)), times^#(X, Y)) } Weak Trs: { from(X) -> cons(X, from(s(X))) , 2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(Y), 2ndsneg(N, Z)) , 2ndspos(0(), Z) -> rnil() , 2ndsneg(s(N), cons(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 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_7(plus^#(X, Y)) , times^#(s(X), Y) -> c_9(plus^#(Y, times(X, Y)), times^#(X, Y)) } Weak DPs: { 2ndspos^#(s(N), cons(X, cons(Y, Z))) -> c_2(2ndsneg^#(N, Z)) , 2ndsneg^#(s(N), cons(X, cons(Y, Z))) -> c_4(2ndspos^#(N, Z)) , pi^#(X) -> c_6(2ndspos^#(X, from(0())), from^#(0())) } Weak Trs: { from(X) -> cons(X, from(s(X))) , 2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(Y), 2ndsneg(N, Z)) , 2ndspos(0(), Z) -> rnil() , 2ndsneg(s(N), cons(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 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, cons(Y, Z))) -> c_2(2ndsneg^#(N, Z)) , 2ndsneg^#(s(N), cons(X, cons(Y, Z))) -> c_4(2ndspos^#(N, Z)) , pi^#(X) -> c_6(2ndspos^#(X, from(0())), from^#(0())) } Weak DPs: { from^#(X) -> c_1(from^#(s(X))) , plus^#(s(X), Y) -> c_7(plus^#(X, Y)) , times^#(s(X), Y) -> c_9(plus^#(Y, times(X, Y)), times^#(X, Y)) } Weak Trs: { from(X) -> cons(X, from(s(X))) , 2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(Y), 2ndsneg(N, Z)) , 2ndspos(0(), Z) -> rnil() , 2ndsneg(s(N), cons(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_7(plus^#(X, Y)) , times^#(s(X), Y) -> c_9(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, cons(Y, Z))) -> c_2(2ndsneg^#(N, Z)) , 2ndsneg^#(s(N), cons(X, cons(Y, Z))) -> c_4(2ndspos^#(N, Z)) , pi^#(X) -> c_6(2ndspos^#(X, from(0())), from^#(0())) } Weak Trs: { from(X) -> cons(X, from(s(X))) , 2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(Y), 2ndsneg(N, Z)) , 2ndspos(0(), Z) -> rnil() , 2ndsneg(s(N), cons(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_6(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, cons(Y, Z))) -> c_1(2ndsneg^#(N, Z)) , 2ndsneg^#(s(N), cons(X, cons(Y, Z))) -> c_2(2ndspos^#(N, Z)) , pi^#(X) -> c_3(2ndspos^#(X, from(0()))) } Weak Trs: { from(X) -> cons(X, from(s(X))) , 2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(Y), 2ndsneg(N, Z)) , 2ndspos(0(), Z) -> rnil() , 2ndsneg(s(N), cons(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, cons(Y, Z))) -> c_1(2ndsneg^#(N, Z)) , 2ndsneg^#(s(N), cons(X, cons(Y, Z))) -> c_2(2ndspos^#(N, Z)) , pi^#(X) -> c_3(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 'Small Polynomial Path Order (PS,1-bounded)' to orient following rules strictly. DPs: { 1: 2ndspos^#(s(N), cons(X, cons(Y, Z))) -> c_1(2ndsneg^#(N, Z)) , 2: 2ndsneg^#(s(N), cons(X, cons(Y, Z))) -> c_2(2ndspos^#(N, Z)) , 3: pi^#(X) -> c_3(2ndspos^#(X, from(0()))) } Trs: { from(X) -> cons(X, from(s(X))) } Sub-proof: ---------- The input was oriented with the instance of 'Small Polynomial Path Order (PS,1-bounded)' as induced by the safe mapping safe(from) = {1}, safe(cons) = {1, 2}, safe(s) = {1}, safe(2ndspos) = {}, safe(0) = {}, safe(rnil) = {}, 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^#) = {2}, safe(c_2) = {}, safe(2ndsneg^#) = {2}, safe(c_3) = {}, safe(c_4) = {}, safe(c_5) = {}, safe(pi^#) = {}, safe(c_6) = {}, safe(plus^#) = {}, safe(c_7) = {}, safe(c_8) = {}, safe(times^#) = {}, safe(c_9) = {}, safe(c_10) = {}, safe(square^#) = {}, safe(c_11) = {}, safe(c) = {}, safe(c_1) = {}, safe(c_2) = {}, safe(c_3) = {} and precedence pi^# > from, pi^# > 2ndspos^#, pi^# > 2ndsneg^#, 2ndspos^# ~ 2ndsneg^# . Following symbols are considered recursive: {from, 2ndspos^#, 2ndsneg^#} The recursion depth is 1. Further, following argument filtering is employed: pi(from) = [1], pi(cons) = [], pi(s) = [1], pi(2ndspos) = [], pi(0) = [], pi(rnil) = [], pi(rcons) = [], pi(posrecip) = [], pi(2ndsneg) = [], pi(negrecip) = [], pi(pi) = [], pi(plus) = [], pi(times) = [], pi(square) = [], pi(from^#) = [], pi(c_1) = [], pi(2ndspos^#) = [1], pi(c_2) = [], pi(2ndsneg^#) = [1], pi(c_3) = [], pi(c_4) = [], pi(c_5) = [], pi(pi^#) = [1], pi(c_6) = [], pi(plus^#) = [], pi(c_7) = [], pi(c_8) = [], pi(times^#) = [], pi(c_9) = [], pi(c_10) = [], pi(square^#) = [], pi(c_11) = [], pi(c) = [], pi(c_1) = [1], pi(c_2) = [1], pi(c_3) = [1] Usable defined function symbols are a subset of: {from, from^#, 2ndspos^#, 2ndsneg^#, pi^#, plus^#, times^#, square^#} For your convenience, here are the satisfied ordering constraints: pi(2ndspos^#(s(N), cons(X, cons(Y, Z)))) = 2ndspos^#(s(; N);) > c_1(2ndsneg^#(N;);) = pi(c_1(2ndsneg^#(N, Z))) pi(2ndsneg^#(s(N), cons(X, cons(Y, Z)))) = 2ndsneg^#(s(; N);) > c_2(2ndspos^#(N;);) = pi(c_2(2ndspos^#(N, Z))) pi(pi^#(X)) = pi^#(X;) > c_3(2ndspos^#(X;);) = pi(c_3(2ndspos^#(X, from(0())))) pi(from(X)) = from(; X) > cons() = pi(cons(X, from(s(X)))) 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: { 2ndspos^#(s(N), cons(X, cons(Y, Z))) -> c_1(2ndsneg^#(N, Z)) , 2ndsneg^#(s(N), cons(X, cons(Y, Z))) -> c_2(2ndspos^#(N, Z)) , pi^#(X) -> c_3(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, cons(Y, Z))) -> c_1(2ndsneg^#(N, Z)) , 2ndsneg^#(s(N), cons(X, cons(Y, Z))) -> c_2(2ndspos^#(N, Z)) , pi^#(X) -> c_3(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_7(plus^#(X, Y)) , times^#(s(X), Y) -> c_9(plus^#(Y, times(X, Y)), times^#(X, Y)) } Weak DPs: { 2ndspos^#(s(N), cons(X, cons(Y, Z))) -> c_2(2ndsneg^#(N, Z)) , 2ndsneg^#(s(N), cons(X, cons(Y, Z))) -> c_4(2ndspos^#(N, Z)) , pi^#(X) -> c_6(2ndspos^#(X, from(0())), from^#(0())) } Weak Trs: { from(X) -> cons(X, from(s(X))) , 2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(Y), 2ndsneg(N, Z)) , 2ndspos(0(), Z) -> rnil() , 2ndsneg(s(N), cons(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, cons(Y, Z))) -> c_2(2ndsneg^#(N, Z)) , 2ndsneg^#(s(N), cons(X, cons(Y, Z))) -> c_4(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_7(plus^#(X, Y)) , times^#(s(X), Y) -> c_9(plus^#(Y, times(X, Y)), times^#(X, Y)) } Weak DPs: { pi^#(X) -> c_6(2ndspos^#(X, from(0())), from^#(0())) } Weak Trs: { from(X) -> cons(X, from(s(X))) , 2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(Y), 2ndsneg(N, Z)) , 2ndspos(0(), Z) -> rnil() , 2ndsneg(s(N), cons(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_6(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, cons(Y, Z))) -> rcons(posrecip(Y), 2ndsneg(N, Z)) , 2ndspos(0(), Z) -> rnil() , 2ndsneg(s(N), cons(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 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 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 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 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(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(2ndsneg^#) = {}, safe(c_3) = {}, safe(c_4) = {}, safe(c_5) = {}, safe(pi^#) = {}, safe(c_6) = {}, safe(plus^#) = {2}, safe(c_7) = {}, safe(c_8) = {}, safe(times^#) = {}, safe(c_9) = {}, safe(c_10) = {}, safe(square^#) = {}, safe(c_11) = {}, 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(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(2ndsneg^#) = [], pi(c_3) = [], pi(c_4) = [], pi(c_5) = [], pi(pi^#) = [], pi(c_6) = [], pi(plus^#) = [1], pi(c_7) = [], pi(c_8) = [], pi(times^#) = [1, 2], pi(c_9) = [], pi(c_10) = [], pi(square^#) = [], pi(c_11) = [], 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 Arrrr..