MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { from_2(x) -> cons_0(x, from_3(s_0(x))) , from_3(x) -> cons_1(x, from_3(s_0(x))) , cons_1(s_0(x), xs) -> overflow_0() , from_1(x) -> cons_0(x, from_3(s_0(x))) } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { from_2^#(x) -> c_1(from_3^#(s_0(x))) , from_3^#(x) -> c_2(cons_1^#(x, from_3(s_0(x))), from_3^#(s_0(x))) , cons_1^#(s_0(x), xs) -> c_3() , from_1^#(x) -> c_4(from_3^#(s_0(x))) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { from_2^#(x) -> c_1(from_3^#(s_0(x))) , from_3^#(x) -> c_2(cons_1^#(x, from_3(s_0(x))), from_3^#(s_0(x))) , cons_1^#(s_0(x), xs) -> c_3() , from_1^#(x) -> c_4(from_3^#(s_0(x))) } Weak Trs: { from_2(x) -> cons_0(x, from_3(s_0(x))) , from_3(x) -> cons_1(x, from_3(s_0(x))) , cons_1(s_0(x), xs) -> overflow_0() , from_1(x) -> cons_0(x, from_3(s_0(x))) } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {3} by applications of Pre({3}) = {2}. Here rules are labeled as follows: DPs: { 1: from_2^#(x) -> c_1(from_3^#(s_0(x))) , 2: from_3^#(x) -> c_2(cons_1^#(x, from_3(s_0(x))), from_3^#(s_0(x))) , 3: cons_1^#(s_0(x), xs) -> c_3() , 4: from_1^#(x) -> c_4(from_3^#(s_0(x))) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { from_2^#(x) -> c_1(from_3^#(s_0(x))) , from_3^#(x) -> c_2(cons_1^#(x, from_3(s_0(x))), from_3^#(s_0(x))) , from_1^#(x) -> c_4(from_3^#(s_0(x))) } Weak DPs: { cons_1^#(s_0(x), xs) -> c_3() } Weak Trs: { from_2(x) -> cons_0(x, from_3(s_0(x))) , from_3(x) -> cons_1(x, from_3(s_0(x))) , cons_1(s_0(x), xs) -> overflow_0() , from_1(x) -> cons_0(x, from_3(s_0(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. { cons_1^#(s_0(x), xs) -> c_3() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { from_2^#(x) -> c_1(from_3^#(s_0(x))) , from_3^#(x) -> c_2(cons_1^#(x, from_3(s_0(x))), from_3^#(s_0(x))) , from_1^#(x) -> c_4(from_3^#(s_0(x))) } Weak Trs: { from_2(x) -> cons_0(x, from_3(s_0(x))) , from_3(x) -> cons_1(x, from_3(s_0(x))) , cons_1(s_0(x), xs) -> overflow_0() , from_1(x) -> cons_0(x, from_3(s_0(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: { from_3^#(x) -> c_2(cons_1^#(x, from_3(s_0(x))), from_3^#(s_0(x))) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { from_2^#(x) -> c_1(from_3^#(s_0(x))) , from_3^#(x) -> c_2(from_3^#(s_0(x))) , from_1^#(x) -> c_3(from_3^#(s_0(x))) } Weak Trs: { from_2(x) -> cons_0(x, from_3(s_0(x))) , from_3(x) -> cons_1(x, from_3(s_0(x))) , cons_1(s_0(x), xs) -> overflow_0() , from_1(x) -> cons_0(x, from_3(s_0(x))) } 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_2^#(x) -> c_1(from_3^#(s_0(x))) , from_3^#(x) -> c_2(from_3^#(s_0(x))) , from_1^#(x) -> c_3(from_3^#(s_0(x))) } Obligation: innermost runtime complexity Answer: MAYBE Consider the dependency graph 1: from_2^#(x) -> c_1(from_3^#(s_0(x))) -->_1 from_3^#(x) -> c_2(from_3^#(s_0(x))) :2 2: from_3^#(x) -> c_2(from_3^#(s_0(x))) -->_1 from_3^#(x) -> c_2(from_3^#(s_0(x))) :2 3: from_1^#(x) -> c_3(from_3^#(s_0(x))) -->_1 from_3^#(x) -> c_2(from_3^#(s_0(x))) :2 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). { from_2^#(x) -> c_1(from_3^#(s_0(x))) , from_1^#(x) -> c_3(from_3^#(s_0(x))) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { from_3^#(x) -> c_2(from_3^#(s_0(x))) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..