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, add(X, Y))) , fib1(X1, X2) -> n__fib1(X1, X2) , add(s(X), Y) -> s(add(X, Y)) , add(0(), X) -> X , activate(X) -> X , activate(n__fib1(X1, X2)) -> fib1(X1, 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(add^#(X, Y)) , fib1^#(X1, X2) -> c_5() , activate^#(X) -> c_8() , activate^#(n__fib1(X1, X2)) -> c_9(fib1^#(X1, X2)) , add^#(s(X), Y) -> c_6(add^#(X, Y)) , add^#(0(), X) -> c_7() } 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(add^#(X, Y)) , fib1^#(X1, X2) -> c_5() , activate^#(X) -> c_8() , activate^#(n__fib1(X1, X2)) -> c_9(fib1^#(X1, X2)) , add^#(s(X), Y) -> c_6(add^#(X, Y)) , add^#(0(), X) -> c_7() } 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, add(X, Y))) , fib1(X1, X2) -> n__fib1(X1, X2) , add(s(X), Y) -> s(add(X, Y)) , add(0(), X) -> X , activate(X) -> X , activate(n__fib1(X1, X2)) -> fib1(X1, X2) } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {3,5,6,9} by applications of Pre({3,5,6,9}) = {1,2,4,7,8}. 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(add^#(X, Y)) , 5: fib1^#(X1, X2) -> c_5() , 6: activate^#(X) -> c_8() , 7: activate^#(n__fib1(X1, X2)) -> c_9(fib1^#(X1, X2)) , 8: add^#(s(X), Y) -> c_6(add^#(X, Y)) , 9: add^#(0(), X) -> c_7() } 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)) , fib1^#(X, Y) -> c_4(add^#(X, Y)) , activate^#(n__fib1(X1, X2)) -> c_9(fib1^#(X1, X2)) , add^#(s(X), Y) -> c_6(add^#(X, Y)) } Weak DPs: { sel^#(0(), cons(X, XS)) -> c_3() , fib1^#(X1, X2) -> c_5() , activate^#(X) -> c_8() , add^#(0(), X) -> c_7() } 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, add(X, Y))) , fib1(X1, X2) -> n__fib1(X1, X2) , add(s(X), Y) -> s(add(X, Y)) , add(0(), X) -> X , activate(X) -> X , activate(n__fib1(X1, X2)) -> fib1(X1, 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^#(X1, X2) -> c_5() , activate^#(X) -> c_8() , add^#(0(), X) -> c_7() } 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)) , fib1^#(X, Y) -> c_4(add^#(X, Y)) , activate^#(n__fib1(X1, X2)) -> c_9(fib1^#(X1, X2)) , add^#(s(X), Y) -> c_6(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, add(X, Y))) , fib1(X1, X2) -> n__fib1(X1, X2) , add(s(X), Y) -> s(add(X, Y)) , add(0(), X) -> X , activate(X) -> X , activate(n__fib1(X1, X2)) -> fib1(X1, 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, add(X, Y))) , fib1(X1, X2) -> n__fib1(X1, X2) , add(s(X), Y) -> s(add(X, Y)) , add(0(), X) -> X , activate(X) -> X , activate(n__fib1(X1, X2)) -> fib1(X1, 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()))), fib1^#(s(0()), s(0()))) , sel^#(s(N), cons(X, XS)) -> c_2(sel^#(N, activate(XS)), activate^#(XS)) , fib1^#(X, Y) -> c_4(add^#(X, Y)) , activate^#(n__fib1(X1, X2)) -> c_9(fib1^#(X1, X2)) , add^#(s(X), Y) -> c_6(add^#(X, Y)) } Weak Trs: { fib1(X, Y) -> cons(X, n__fib1(Y, add(X, Y))) , fib1(X1, X2) -> n__fib1(X1, X2) , add(s(X), Y) -> s(add(X, Y)) , add(0(), X) -> X , activate(X) -> X , activate(n__fib1(X1, X2)) -> fib1(X1, X2) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..