MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { from(x) -> cons(x, cons(nil(), from(s(x)))) , cons(s(x), xs) -> nil() } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { from^#(x) -> c_1(cons^#(x, cons(nil(), from(s(x)))), cons^#(nil(), from(s(x))), from^#(s(x))) , cons^#(s(x), xs) -> c_2() } 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(cons^#(x, cons(nil(), from(s(x)))), cons^#(nil(), from(s(x))), from^#(s(x))) , cons^#(s(x), xs) -> c_2() } Weak Trs: { from(x) -> cons(x, cons(nil(), from(s(x)))) , cons(s(x), xs) -> nil() } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {2} by applications of Pre({2}) = {1}. Here rules are labeled as follows: DPs: { 1: from^#(x) -> c_1(cons^#(x, cons(nil(), from(s(x)))), cons^#(nil(), from(s(x))), from^#(s(x))) , 2: cons^#(s(x), xs) -> c_2() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { from^#(x) -> c_1(cons^#(x, cons(nil(), from(s(x)))), cons^#(nil(), from(s(x))), from^#(s(x))) } Weak DPs: { cons^#(s(x), xs) -> c_2() } Weak Trs: { from(x) -> cons(x, cons(nil(), from(s(x)))) , cons(s(x), xs) -> nil() } 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^#(s(x), xs) -> c_2() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { from^#(x) -> c_1(cons^#(x, cons(nil(), from(s(x)))), cons^#(nil(), from(s(x))), from^#(s(x))) } Weak Trs: { from(x) -> cons(x, cons(nil(), from(s(x)))) , cons(s(x), xs) -> nil() } 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^#(x) -> c_1(cons^#(x, cons(nil(), from(s(x)))), cons^#(nil(), from(s(x))), from^#(s(x))) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { from^#(x) -> c_1(from^#(s(x))) } Weak Trs: { from(x) -> cons(x, cons(nil(), from(s(x)))) , cons(s(x), xs) -> nil() } 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))) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..