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, activate(XS)) , sel(0(), cons(X, XS)) -> X , fib1(X, Y) -> cons(X, n__fib1(Y, n__add(X, Y))) , fib1(X1, X2) -> n__fib1(X1, X2) , add(X1, X2) -> n__add(X1, X2) , add(s(X), Y) -> s(add(X, Y)) , add(0(), X) -> X , activate(X) -> X , activate(n__fib1(X1, X2)) -> fib1(activate(X1), activate(X2)) , activate(n__add(X1, X2)) -> add(activate(X1), activate(X2)) } 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, activate(XS)), activate^#(XS)) , sel^#(0(), cons(X, XS)) -> c_3() , fib1^#(X, Y) -> c_4() , fib1^#(X1, X2) -> c_5() , activate^#(X) -> c_9() , activate^#(n__fib1(X1, X2)) -> c_10(fib1^#(activate(X1), activate(X2)), activate^#(X1), activate^#(X2)) , activate^#(n__add(X1, X2)) -> c_11(add^#(activate(X1), activate(X2)), activate^#(X1), activate^#(X2)) , add^#(X1, X2) -> c_6() , add^#(s(X), Y) -> c_7(add^#(X, Y)) , add^#(0(), X) -> c_8() } 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, activate(XS)), activate^#(XS)) , sel^#(0(), cons(X, XS)) -> c_3() , fib1^#(X, Y) -> c_4() , fib1^#(X1, X2) -> c_5() , activate^#(X) -> c_9() , activate^#(n__fib1(X1, X2)) -> c_10(fib1^#(activate(X1), activate(X2)), activate^#(X1), activate^#(X2)) , activate^#(n__add(X1, X2)) -> c_11(add^#(activate(X1), activate(X2)), activate^#(X1), activate^#(X2)) , add^#(X1, X2) -> c_6() , add^#(s(X), Y) -> c_7(add^#(X, Y)) , add^#(0(), X) -> c_8() } Weak Trs: { fib(N) -> sel(N, fib1(s(0()), s(0()))) , sel(s(N), cons(X, XS)) -> sel(N, activate(XS)) , sel(0(), cons(X, XS)) -> X , fib1(X, Y) -> cons(X, n__fib1(Y, n__add(X, Y))) , fib1(X1, X2) -> n__fib1(X1, X2) , add(X1, X2) -> n__add(X1, X2) , add(s(X), Y) -> s(add(X, Y)) , add(0(), X) -> X , activate(X) -> X , activate(n__fib1(X1, X2)) -> fib1(activate(X1), activate(X2)) , activate(n__add(X1, X2)) -> add(activate(X1), activate(X2)) } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {3,4,5,6,9,11} by applications of Pre({3,4,5,6,9,11}) = {1,2,7,8,10}. 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, activate(XS)), activate^#(XS)) , 3: sel^#(0(), cons(X, XS)) -> c_3() , 4: fib1^#(X, Y) -> c_4() , 5: fib1^#(X1, X2) -> c_5() , 6: activate^#(X) -> c_9() , 7: activate^#(n__fib1(X1, X2)) -> c_10(fib1^#(activate(X1), activate(X2)), activate^#(X1), activate^#(X2)) , 8: activate^#(n__add(X1, X2)) -> c_11(add^#(activate(X1), activate(X2)), activate^#(X1), activate^#(X2)) , 9: add^#(X1, X2) -> c_6() , 10: add^#(s(X), Y) -> c_7(add^#(X, Y)) , 11: add^#(0(), X) -> c_8() } 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, activate(XS)), activate^#(XS)) , activate^#(n__fib1(X1, X2)) -> c_10(fib1^#(activate(X1), activate(X2)), activate^#(X1), activate^#(X2)) , activate^#(n__add(X1, X2)) -> c_11(add^#(activate(X1), activate(X2)), activate^#(X1), activate^#(X2)) , add^#(s(X), Y) -> c_7(add^#(X, Y)) } Weak DPs: { sel^#(0(), cons(X, XS)) -> c_3() , fib1^#(X, Y) -> c_4() , fib1^#(X1, X2) -> c_5() , activate^#(X) -> c_9() , add^#(X1, X2) -> c_6() , add^#(0(), X) -> c_8() } Weak Trs: { fib(N) -> sel(N, fib1(s(0()), s(0()))) , sel(s(N), cons(X, XS)) -> sel(N, activate(XS)) , sel(0(), cons(X, XS)) -> X , fib1(X, Y) -> cons(X, n__fib1(Y, n__add(X, Y))) , fib1(X1, X2) -> n__fib1(X1, X2) , add(X1, X2) -> n__add(X1, X2) , add(s(X), Y) -> s(add(X, Y)) , add(0(), X) -> X , activate(X) -> X , activate(n__fib1(X1, X2)) -> fib1(activate(X1), activate(X2)) , activate(n__add(X1, X2)) -> add(activate(X1), activate(X2)) } 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() , fib1^#(X, Y) -> c_4() , fib1^#(X1, X2) -> c_5() , activate^#(X) -> c_9() , add^#(X1, X2) -> c_6() , add^#(0(), X) -> c_8() } 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, activate(XS)), activate^#(XS)) , activate^#(n__fib1(X1, X2)) -> c_10(fib1^#(activate(X1), activate(X2)), activate^#(X1), activate^#(X2)) , activate^#(n__add(X1, X2)) -> c_11(add^#(activate(X1), activate(X2)), activate^#(X1), activate^#(X2)) , add^#(s(X), Y) -> c_7(add^#(X, Y)) } Weak Trs: { fib(N) -> sel(N, fib1(s(0()), s(0()))) , sel(s(N), cons(X, XS)) -> sel(N, activate(XS)) , sel(0(), cons(X, XS)) -> X , fib1(X, Y) -> cons(X, n__fib1(Y, n__add(X, Y))) , fib1(X1, X2) -> n__fib1(X1, X2) , add(X1, X2) -> n__add(X1, X2) , add(s(X), Y) -> s(add(X, Y)) , add(0(), X) -> X , activate(X) -> X , activate(n__fib1(X1, X2)) -> fib1(activate(X1), activate(X2)) , activate(n__add(X1, X2)) -> add(activate(X1), activate(X2)) } Obligation: innermost runtime complexity Answer: MAYBE Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { fib^#(N) -> c_1(sel^#(N, fib1(s(0()), s(0()))), fib1^#(s(0()), s(0()))) , activate^#(n__fib1(X1, X2)) -> c_10(fib1^#(activate(X1), activate(X2)), activate^#(X1), activate^#(X2)) } 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())))) , sel^#(s(N), cons(X, XS)) -> c_2(sel^#(N, activate(XS)), activate^#(XS)) , activate^#(n__fib1(X1, X2)) -> c_3(activate^#(X1), activate^#(X2)) , activate^#(n__add(X1, X2)) -> c_4(add^#(activate(X1), activate(X2)), activate^#(X1), activate^#(X2)) , 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, activate(XS)) , sel(0(), cons(X, XS)) -> X , fib1(X, Y) -> cons(X, n__fib1(Y, n__add(X, Y))) , fib1(X1, X2) -> n__fib1(X1, X2) , add(X1, X2) -> n__add(X1, X2) , add(s(X), Y) -> s(add(X, Y)) , add(0(), X) -> X , activate(X) -> X , activate(n__fib1(X1, X2)) -> fib1(activate(X1), activate(X2)) , activate(n__add(X1, X2)) -> add(activate(X1), activate(X2)) } Obligation: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Weak Usable Rules: { fib1(X, Y) -> cons(X, n__fib1(Y, n__add(X, Y))) , fib1(X1, X2) -> n__fib1(X1, X2) , add(X1, X2) -> n__add(X1, X2) , add(s(X), Y) -> s(add(X, Y)) , add(0(), X) -> X , activate(X) -> X , activate(n__fib1(X1, X2)) -> fib1(activate(X1), activate(X2)) , activate(n__add(X1, X2)) -> add(activate(X1), activate(X2)) } 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())))) , sel^#(s(N), cons(X, XS)) -> c_2(sel^#(N, activate(XS)), activate^#(XS)) , activate^#(n__fib1(X1, X2)) -> c_3(activate^#(X1), activate^#(X2)) , activate^#(n__add(X1, X2)) -> c_4(add^#(activate(X1), activate(X2)), activate^#(X1), activate^#(X2)) , add^#(s(X), Y) -> c_5(add^#(X, Y)) } Weak Trs: { fib1(X, Y) -> cons(X, n__fib1(Y, n__add(X, Y))) , fib1(X1, X2) -> n__fib1(X1, X2) , add(X1, X2) -> n__add(X1, X2) , add(s(X), Y) -> s(add(X, Y)) , add(0(), X) -> X , activate(X) -> X , activate(n__fib1(X1, X2)) -> fib1(activate(X1), activate(X2)) , activate(n__add(X1, X2)) -> add(activate(X1), activate(X2)) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..