MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { nats() -> cons(0(), n__incr(n__nats())) , nats() -> n__nats() , pairs() -> cons(0(), n__incr(n__odds())) , odds() -> n__odds() , odds() -> incr(pairs()) , incr(X) -> n__incr(X) , incr(cons(X, XS)) -> cons(s(X), n__incr(activate(XS))) , activate(X) -> X , activate(n__incr(X)) -> incr(activate(X)) , activate(n__nats()) -> nats() , activate(n__odds()) -> odds() , head(cons(X, XS)) -> X , tail(cons(X, XS)) -> activate(XS) } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { nats^#() -> c_1() , nats^#() -> c_2() , pairs^#() -> c_3() , odds^#() -> c_4() , odds^#() -> c_5(incr^#(pairs()), pairs^#()) , incr^#(X) -> c_6() , incr^#(cons(X, XS)) -> c_7(activate^#(XS)) , activate^#(X) -> c_8() , activate^#(n__incr(X)) -> c_9(incr^#(activate(X)), activate^#(X)) , activate^#(n__nats()) -> c_10(nats^#()) , activate^#(n__odds()) -> c_11(odds^#()) , head^#(cons(X, XS)) -> c_12() , tail^#(cons(X, XS)) -> c_13(activate^#(XS)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { nats^#() -> c_1() , nats^#() -> c_2() , pairs^#() -> c_3() , odds^#() -> c_4() , odds^#() -> c_5(incr^#(pairs()), pairs^#()) , incr^#(X) -> c_6() , incr^#(cons(X, XS)) -> c_7(activate^#(XS)) , activate^#(X) -> c_8() , activate^#(n__incr(X)) -> c_9(incr^#(activate(X)), activate^#(X)) , activate^#(n__nats()) -> c_10(nats^#()) , activate^#(n__odds()) -> c_11(odds^#()) , head^#(cons(X, XS)) -> c_12() , tail^#(cons(X, XS)) -> c_13(activate^#(XS)) } Weak Trs: { nats() -> cons(0(), n__incr(n__nats())) , nats() -> n__nats() , pairs() -> cons(0(), n__incr(n__odds())) , odds() -> n__odds() , odds() -> incr(pairs()) , incr(X) -> n__incr(X) , incr(cons(X, XS)) -> cons(s(X), n__incr(activate(XS))) , activate(X) -> X , activate(n__incr(X)) -> incr(activate(X)) , activate(n__nats()) -> nats() , activate(n__odds()) -> odds() , head(cons(X, XS)) -> X , tail(cons(X, XS)) -> activate(XS) } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {1,2,3,4,6,8,12} by applications of Pre({1,2,3,4,6,8,12}) = {5,7,9,10,11,13}. Here rules are labeled as follows: DPs: { 1: nats^#() -> c_1() , 2: nats^#() -> c_2() , 3: pairs^#() -> c_3() , 4: odds^#() -> c_4() , 5: odds^#() -> c_5(incr^#(pairs()), pairs^#()) , 6: incr^#(X) -> c_6() , 7: incr^#(cons(X, XS)) -> c_7(activate^#(XS)) , 8: activate^#(X) -> c_8() , 9: activate^#(n__incr(X)) -> c_9(incr^#(activate(X)), activate^#(X)) , 10: activate^#(n__nats()) -> c_10(nats^#()) , 11: activate^#(n__odds()) -> c_11(odds^#()) , 12: head^#(cons(X, XS)) -> c_12() , 13: tail^#(cons(X, XS)) -> c_13(activate^#(XS)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { odds^#() -> c_5(incr^#(pairs()), pairs^#()) , incr^#(cons(X, XS)) -> c_7(activate^#(XS)) , activate^#(n__incr(X)) -> c_9(incr^#(activate(X)), activate^#(X)) , activate^#(n__nats()) -> c_10(nats^#()) , activate^#(n__odds()) -> c_11(odds^#()) , tail^#(cons(X, XS)) -> c_13(activate^#(XS)) } Weak DPs: { nats^#() -> c_1() , nats^#() -> c_2() , pairs^#() -> c_3() , odds^#() -> c_4() , incr^#(X) -> c_6() , activate^#(X) -> c_8() , head^#(cons(X, XS)) -> c_12() } Weak Trs: { nats() -> cons(0(), n__incr(n__nats())) , nats() -> n__nats() , pairs() -> cons(0(), n__incr(n__odds())) , odds() -> n__odds() , odds() -> incr(pairs()) , incr(X) -> n__incr(X) , incr(cons(X, XS)) -> cons(s(X), n__incr(activate(XS))) , activate(X) -> X , activate(n__incr(X)) -> incr(activate(X)) , activate(n__nats()) -> nats() , activate(n__odds()) -> odds() , head(cons(X, XS)) -> X , tail(cons(X, XS)) -> activate(XS) } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {4} by applications of Pre({4}) = {2,3,6}. Here rules are labeled as follows: DPs: { 1: odds^#() -> c_5(incr^#(pairs()), pairs^#()) , 2: incr^#(cons(X, XS)) -> c_7(activate^#(XS)) , 3: activate^#(n__incr(X)) -> c_9(incr^#(activate(X)), activate^#(X)) , 4: activate^#(n__nats()) -> c_10(nats^#()) , 5: activate^#(n__odds()) -> c_11(odds^#()) , 6: tail^#(cons(X, XS)) -> c_13(activate^#(XS)) , 7: nats^#() -> c_1() , 8: nats^#() -> c_2() , 9: pairs^#() -> c_3() , 10: odds^#() -> c_4() , 11: incr^#(X) -> c_6() , 12: activate^#(X) -> c_8() , 13: head^#(cons(X, XS)) -> c_12() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { odds^#() -> c_5(incr^#(pairs()), pairs^#()) , incr^#(cons(X, XS)) -> c_7(activate^#(XS)) , activate^#(n__incr(X)) -> c_9(incr^#(activate(X)), activate^#(X)) , activate^#(n__odds()) -> c_11(odds^#()) , tail^#(cons(X, XS)) -> c_13(activate^#(XS)) } Weak DPs: { nats^#() -> c_1() , nats^#() -> c_2() , pairs^#() -> c_3() , odds^#() -> c_4() , incr^#(X) -> c_6() , activate^#(X) -> c_8() , activate^#(n__nats()) -> c_10(nats^#()) , head^#(cons(X, XS)) -> c_12() } Weak Trs: { nats() -> cons(0(), n__incr(n__nats())) , nats() -> n__nats() , pairs() -> cons(0(), n__incr(n__odds())) , odds() -> n__odds() , odds() -> incr(pairs()) , incr(X) -> n__incr(X) , incr(cons(X, XS)) -> cons(s(X), n__incr(activate(XS))) , activate(X) -> X , activate(n__incr(X)) -> incr(activate(X)) , activate(n__nats()) -> nats() , activate(n__odds()) -> odds() , head(cons(X, XS)) -> X , tail(cons(X, XS)) -> activate(XS) } 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. { nats^#() -> c_1() , nats^#() -> c_2() , pairs^#() -> c_3() , odds^#() -> c_4() , incr^#(X) -> c_6() , activate^#(X) -> c_8() , activate^#(n__nats()) -> c_10(nats^#()) , head^#(cons(X, XS)) -> c_12() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { odds^#() -> c_5(incr^#(pairs()), pairs^#()) , incr^#(cons(X, XS)) -> c_7(activate^#(XS)) , activate^#(n__incr(X)) -> c_9(incr^#(activate(X)), activate^#(X)) , activate^#(n__odds()) -> c_11(odds^#()) , tail^#(cons(X, XS)) -> c_13(activate^#(XS)) } Weak Trs: { nats() -> cons(0(), n__incr(n__nats())) , nats() -> n__nats() , pairs() -> cons(0(), n__incr(n__odds())) , odds() -> n__odds() , odds() -> incr(pairs()) , incr(X) -> n__incr(X) , incr(cons(X, XS)) -> cons(s(X), n__incr(activate(XS))) , activate(X) -> X , activate(n__incr(X)) -> incr(activate(X)) , activate(n__nats()) -> nats() , activate(n__odds()) -> odds() , head(cons(X, XS)) -> X , tail(cons(X, XS)) -> activate(XS) } Obligation: innermost runtime complexity Answer: MAYBE Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { odds^#() -> c_5(incr^#(pairs()), pairs^#()) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { odds^#() -> c_1(incr^#(pairs())) , incr^#(cons(X, XS)) -> c_2(activate^#(XS)) , activate^#(n__incr(X)) -> c_3(incr^#(activate(X)), activate^#(X)) , activate^#(n__odds()) -> c_4(odds^#()) , tail^#(cons(X, XS)) -> c_5(activate^#(XS)) } Weak Trs: { nats() -> cons(0(), n__incr(n__nats())) , nats() -> n__nats() , pairs() -> cons(0(), n__incr(n__odds())) , odds() -> n__odds() , odds() -> incr(pairs()) , incr(X) -> n__incr(X) , incr(cons(X, XS)) -> cons(s(X), n__incr(activate(XS))) , activate(X) -> X , activate(n__incr(X)) -> incr(activate(X)) , activate(n__nats()) -> nats() , activate(n__odds()) -> odds() , head(cons(X, XS)) -> X , tail(cons(X, XS)) -> activate(XS) } Obligation: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Weak Usable Rules: { nats() -> cons(0(), n__incr(n__nats())) , nats() -> n__nats() , pairs() -> cons(0(), n__incr(n__odds())) , odds() -> n__odds() , odds() -> incr(pairs()) , incr(X) -> n__incr(X) , incr(cons(X, XS)) -> cons(s(X), n__incr(activate(XS))) , activate(X) -> X , activate(n__incr(X)) -> incr(activate(X)) , activate(n__nats()) -> nats() , activate(n__odds()) -> odds() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { odds^#() -> c_1(incr^#(pairs())) , incr^#(cons(X, XS)) -> c_2(activate^#(XS)) , activate^#(n__incr(X)) -> c_3(incr^#(activate(X)), activate^#(X)) , activate^#(n__odds()) -> c_4(odds^#()) , tail^#(cons(X, XS)) -> c_5(activate^#(XS)) } Weak Trs: { nats() -> cons(0(), n__incr(n__nats())) , nats() -> n__nats() , pairs() -> cons(0(), n__incr(n__odds())) , odds() -> n__odds() , odds() -> incr(pairs()) , incr(X) -> n__incr(X) , incr(cons(X, XS)) -> cons(s(X), n__incr(activate(XS))) , activate(X) -> X , activate(n__incr(X)) -> incr(activate(X)) , activate(n__nats()) -> nats() , activate(n__odds()) -> odds() } Obligation: innermost runtime complexity Answer: MAYBE Consider the dependency graph 1: odds^#() -> c_1(incr^#(pairs())) -->_1 incr^#(cons(X, XS)) -> c_2(activate^#(XS)) :2 2: incr^#(cons(X, XS)) -> c_2(activate^#(XS)) -->_1 activate^#(n__odds()) -> c_4(odds^#()) :4 -->_1 activate^#(n__incr(X)) -> c_3(incr^#(activate(X)), activate^#(X)) :3 3: activate^#(n__incr(X)) -> c_3(incr^#(activate(X)), activate^#(X)) -->_2 activate^#(n__odds()) -> c_4(odds^#()) :4 -->_2 activate^#(n__incr(X)) -> c_3(incr^#(activate(X)), activate^#(X)) :3 -->_1 incr^#(cons(X, XS)) -> c_2(activate^#(XS)) :2 4: activate^#(n__odds()) -> c_4(odds^#()) -->_1 odds^#() -> c_1(incr^#(pairs())) :1 5: tail^#(cons(X, XS)) -> c_5(activate^#(XS)) -->_1 activate^#(n__odds()) -> c_4(odds^#()) :4 -->_1 activate^#(n__incr(X)) -> c_3(incr^#(activate(X)), activate^#(X)) :3 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). { tail^#(cons(X, XS)) -> c_5(activate^#(XS)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { odds^#() -> c_1(incr^#(pairs())) , incr^#(cons(X, XS)) -> c_2(activate^#(XS)) , activate^#(n__incr(X)) -> c_3(incr^#(activate(X)), activate^#(X)) , activate^#(n__odds()) -> c_4(odds^#()) } Weak Trs: { nats() -> cons(0(), n__incr(n__nats())) , nats() -> n__nats() , pairs() -> cons(0(), n__incr(n__odds())) , odds() -> n__odds() , odds() -> incr(pairs()) , incr(X) -> n__incr(X) , incr(cons(X, XS)) -> cons(s(X), n__incr(activate(XS))) , activate(X) -> X , activate(n__incr(X)) -> incr(activate(X)) , activate(n__nats()) -> nats() , activate(n__odds()) -> odds() } Obligation: innermost runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'matrices' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'matrix interpretation of dimension 4' failed due to the following reason: The input cannot be shown compatible 2) 'matrix interpretation of dimension 3' failed due to the following reason: The input cannot be shown compatible 3) 'matrix interpretation of dimension 3' failed due to the following reason: The input cannot be shown compatible 4) 'matrix interpretation of dimension 2' failed due to the following reason: The input cannot be shown compatible 5) 'matrix interpretation of dimension 2' failed due to the following reason: The input cannot be shown compatible 6) 'matrix interpretation of dimension 1' failed due to the following reason: The input cannot be shown compatible 2) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. Arrrr..