MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { nats() -> cons(0(), n__incr(nats())) , pairs() -> cons(0(), n__incr(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(X) , 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^#()) , pairs^#() -> c_2(odds^#()) , odds^#() -> c_3(incr^#(pairs()), pairs^#()) , incr^#(X) -> c_4() , incr^#(cons(X, XS)) -> c_5(activate^#(XS)) , activate^#(X) -> c_6() , activate^#(n__incr(X)) -> c_7(incr^#(X)) , head^#(cons(X, XS)) -> c_8() , tail^#(cons(X, XS)) -> c_9(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^#()) , pairs^#() -> c_2(odds^#()) , odds^#() -> c_3(incr^#(pairs()), pairs^#()) , incr^#(X) -> c_4() , incr^#(cons(X, XS)) -> c_5(activate^#(XS)) , activate^#(X) -> c_6() , activate^#(n__incr(X)) -> c_7(incr^#(X)) , head^#(cons(X, XS)) -> c_8() , tail^#(cons(X, XS)) -> c_9(activate^#(XS)) } Weak Trs: { nats() -> cons(0(), n__incr(nats())) , pairs() -> cons(0(), n__incr(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(X) , 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,6,8} by applications of Pre({4,6,8}) = {3,5,7,9}. Here rules are labeled as follows: DPs: { 1: nats^#() -> c_1(nats^#()) , 2: pairs^#() -> c_2(odds^#()) , 3: odds^#() -> c_3(incr^#(pairs()), pairs^#()) , 4: incr^#(X) -> c_4() , 5: incr^#(cons(X, XS)) -> c_5(activate^#(XS)) , 6: activate^#(X) -> c_6() , 7: activate^#(n__incr(X)) -> c_7(incr^#(X)) , 8: head^#(cons(X, XS)) -> c_8() , 9: tail^#(cons(X, XS)) -> c_9(activate^#(XS)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { nats^#() -> c_1(nats^#()) , pairs^#() -> c_2(odds^#()) , odds^#() -> c_3(incr^#(pairs()), pairs^#()) , incr^#(cons(X, XS)) -> c_5(activate^#(XS)) , activate^#(n__incr(X)) -> c_7(incr^#(X)) , tail^#(cons(X, XS)) -> c_9(activate^#(XS)) } Weak DPs: { incr^#(X) -> c_4() , activate^#(X) -> c_6() , head^#(cons(X, XS)) -> c_8() } Weak Trs: { nats() -> cons(0(), n__incr(nats())) , pairs() -> cons(0(), n__incr(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(X) , 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. { incr^#(X) -> c_4() , activate^#(X) -> c_6() , head^#(cons(X, XS)) -> c_8() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { nats^#() -> c_1(nats^#()) , pairs^#() -> c_2(odds^#()) , odds^#() -> c_3(incr^#(pairs()), pairs^#()) , incr^#(cons(X, XS)) -> c_5(activate^#(XS)) , activate^#(n__incr(X)) -> c_7(incr^#(X)) , tail^#(cons(X, XS)) -> c_9(activate^#(XS)) } Weak Trs: { nats() -> cons(0(), n__incr(nats())) , pairs() -> cons(0(), n__incr(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(X) , head(cons(X, XS)) -> X , tail(cons(X, XS)) -> activate(XS) } Obligation: innermost runtime complexity Answer: MAYBE Consider the dependency graph 1: nats^#() -> c_1(nats^#()) -->_1 nats^#() -> c_1(nats^#()) :1 2: pairs^#() -> c_2(odds^#()) -->_1 odds^#() -> c_3(incr^#(pairs()), pairs^#()) :3 3: odds^#() -> c_3(incr^#(pairs()), pairs^#()) -->_1 incr^#(cons(X, XS)) -> c_5(activate^#(XS)) :4 -->_2 pairs^#() -> c_2(odds^#()) :2 4: incr^#(cons(X, XS)) -> c_5(activate^#(XS)) -->_1 activate^#(n__incr(X)) -> c_7(incr^#(X)) :5 5: activate^#(n__incr(X)) -> c_7(incr^#(X)) -->_1 incr^#(cons(X, XS)) -> c_5(activate^#(XS)) :4 6: tail^#(cons(X, XS)) -> c_9(activate^#(XS)) -->_1 activate^#(n__incr(X)) -> c_7(incr^#(X)) :5 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_9(activate^#(XS)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { nats^#() -> c_1(nats^#()) , pairs^#() -> c_2(odds^#()) , odds^#() -> c_3(incr^#(pairs()), pairs^#()) , incr^#(cons(X, XS)) -> c_5(activate^#(XS)) , activate^#(n__incr(X)) -> c_7(incr^#(X)) } Weak Trs: { nats() -> cons(0(), n__incr(nats())) , pairs() -> cons(0(), n__incr(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(X) , 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: { pairs() -> cons(0(), n__incr(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(X) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { nats^#() -> c_1(nats^#()) , pairs^#() -> c_2(odds^#()) , odds^#() -> c_3(incr^#(pairs()), pairs^#()) , incr^#(cons(X, XS)) -> c_5(activate^#(XS)) , activate^#(n__incr(X)) -> c_7(incr^#(X)) } Weak Trs: { pairs() -> cons(0(), n__incr(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(X) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..