MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { fib(N) -> sel(N, fib1(s(0()), s(0()))) , sel(s(N), cons(X, XS)) -> sel(N, XS) , sel(0(), cons(X, XS)) -> X , fib1(X, Y) -> cons(X, fib1(Y, add(X, Y))) , add(s(X), Y) -> s(add(X, Y)) , add(0(), X) -> X } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { fib^#(N) -> c_1(sel^#(N, fib1(s(0()), s(0()))), fib1^#(s(0()), s(0()))) , sel^#(s(N), cons(X, XS)) -> c_2(sel^#(N, XS)) , sel^#(0(), cons(X, XS)) -> c_3() , fib1^#(X, Y) -> c_4(fib1^#(Y, add(X, Y)), add^#(X, Y)) , add^#(s(X), Y) -> c_5(add^#(X, Y)) , add^#(0(), X) -> c_6() } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { fib^#(N) -> c_1(sel^#(N, fib1(s(0()), s(0()))), fib1^#(s(0()), s(0()))) , sel^#(s(N), cons(X, XS)) -> c_2(sel^#(N, XS)) , sel^#(0(), cons(X, XS)) -> c_3() , fib1^#(X, Y) -> c_4(fib1^#(Y, add(X, Y)), add^#(X, Y)) , add^#(s(X), Y) -> c_5(add^#(X, Y)) , add^#(0(), X) -> c_6() } Weak Trs: { fib(N) -> sel(N, fib1(s(0()), s(0()))) , sel(s(N), cons(X, XS)) -> sel(N, XS) , sel(0(), cons(X, XS)) -> X , fib1(X, Y) -> cons(X, fib1(Y, add(X, Y))) , add(s(X), Y) -> s(add(X, Y)) , add(0(), X) -> X } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {3,6} by applications of Pre({3,6}) = {1,2,4,5}. Here rules are labeled as follows: DPs: { 1: fib^#(N) -> c_1(sel^#(N, fib1(s(0()), s(0()))), fib1^#(s(0()), s(0()))) , 2: sel^#(s(N), cons(X, XS)) -> c_2(sel^#(N, XS)) , 3: sel^#(0(), cons(X, XS)) -> c_3() , 4: fib1^#(X, Y) -> c_4(fib1^#(Y, add(X, Y)), add^#(X, Y)) , 5: add^#(s(X), Y) -> c_5(add^#(X, Y)) , 6: add^#(0(), X) -> c_6() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { fib^#(N) -> c_1(sel^#(N, fib1(s(0()), s(0()))), fib1^#(s(0()), s(0()))) , sel^#(s(N), cons(X, XS)) -> c_2(sel^#(N, XS)) , fib1^#(X, Y) -> c_4(fib1^#(Y, add(X, Y)), add^#(X, Y)) , add^#(s(X), Y) -> c_5(add^#(X, Y)) } Weak DPs: { sel^#(0(), cons(X, XS)) -> c_3() , add^#(0(), X) -> c_6() } Weak Trs: { fib(N) -> sel(N, fib1(s(0()), s(0()))) , sel(s(N), cons(X, XS)) -> sel(N, XS) , sel(0(), cons(X, XS)) -> X , fib1(X, Y) -> cons(X, fib1(Y, add(X, Y))) , add(s(X), Y) -> s(add(X, Y)) , add(0(), 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. { sel^#(0(), cons(X, XS)) -> c_3() , add^#(0(), X) -> c_6() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { fib^#(N) -> c_1(sel^#(N, fib1(s(0()), s(0()))), fib1^#(s(0()), s(0()))) , sel^#(s(N), cons(X, XS)) -> c_2(sel^#(N, XS)) , fib1^#(X, Y) -> c_4(fib1^#(Y, add(X, Y)), add^#(X, Y)) , add^#(s(X), Y) -> c_5(add^#(X, Y)) } Weak Trs: { fib(N) -> sel(N, fib1(s(0()), s(0()))) , sel(s(N), cons(X, XS)) -> sel(N, XS) , sel(0(), cons(X, XS)) -> X , fib1(X, Y) -> cons(X, fib1(Y, add(X, Y))) , add(s(X), Y) -> s(add(X, Y)) , add(0(), X) -> X } Obligation: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Weak Usable Rules: { fib1(X, Y) -> cons(X, fib1(Y, add(X, Y))) , add(s(X), Y) -> s(add(X, Y)) , add(0(), X) -> X } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { fib^#(N) -> c_1(sel^#(N, fib1(s(0()), s(0()))), fib1^#(s(0()), s(0()))) , sel^#(s(N), cons(X, XS)) -> c_2(sel^#(N, XS)) , fib1^#(X, Y) -> c_4(fib1^#(Y, add(X, Y)), add^#(X, Y)) , add^#(s(X), Y) -> c_5(add^#(X, Y)) } Weak Trs: { fib1(X, Y) -> cons(X, fib1(Y, add(X, Y))) , add(s(X), Y) -> s(add(X, Y)) , add(0(), X) -> X } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..