MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { plus(0(), y) -> y , plus(s(x), y) -> s(plus(x, y)) , lt(x, 0()) -> false() , lt(0(), s(y)) -> true() , lt(s(x), s(y)) -> lt(x, y) , fib(x) -> fibiter(x, 0(), 0(), s(0())) , fibiter(b, c, x, y) -> if(lt(c, b), b, c, x, y) , if(true(), b, c, x, y) -> fibiter(b, s(c), y, plus(x, y)) , if(false(), b, c, x, y) -> x } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { plus^#(0(), y) -> c_1() , plus^#(s(x), y) -> c_2(plus^#(x, y)) , lt^#(x, 0()) -> c_3() , lt^#(0(), s(y)) -> c_4() , lt^#(s(x), s(y)) -> c_5(lt^#(x, y)) , fib^#(x) -> c_6(fibiter^#(x, 0(), 0(), s(0()))) , fibiter^#(b, c, x, y) -> c_7(if^#(lt(c, b), b, c, x, y), lt^#(c, b)) , if^#(true(), b, c, x, y) -> c_8(fibiter^#(b, s(c), y, plus(x, y)), plus^#(x, y)) , if^#(false(), b, c, x, y) -> c_9() } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { plus^#(0(), y) -> c_1() , plus^#(s(x), y) -> c_2(plus^#(x, y)) , lt^#(x, 0()) -> c_3() , lt^#(0(), s(y)) -> c_4() , lt^#(s(x), s(y)) -> c_5(lt^#(x, y)) , fib^#(x) -> c_6(fibiter^#(x, 0(), 0(), s(0()))) , fibiter^#(b, c, x, y) -> c_7(if^#(lt(c, b), b, c, x, y), lt^#(c, b)) , if^#(true(), b, c, x, y) -> c_8(fibiter^#(b, s(c), y, plus(x, y)), plus^#(x, y)) , if^#(false(), b, c, x, y) -> c_9() } Weak Trs: { plus(0(), y) -> y , plus(s(x), y) -> s(plus(x, y)) , lt(x, 0()) -> false() , lt(0(), s(y)) -> true() , lt(s(x), s(y)) -> lt(x, y) , fib(x) -> fibiter(x, 0(), 0(), s(0())) , fibiter(b, c, x, y) -> if(lt(c, b), b, c, x, y) , if(true(), b, c, x, y) -> fibiter(b, s(c), y, plus(x, y)) , if(false(), b, c, x, y) -> x } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {1,3,4,9} by applications of Pre({1,3,4,9}) = {2,5,7,8}. Here rules are labeled as follows: DPs: { 1: plus^#(0(), y) -> c_1() , 2: plus^#(s(x), y) -> c_2(plus^#(x, y)) , 3: lt^#(x, 0()) -> c_3() , 4: lt^#(0(), s(y)) -> c_4() , 5: lt^#(s(x), s(y)) -> c_5(lt^#(x, y)) , 6: fib^#(x) -> c_6(fibiter^#(x, 0(), 0(), s(0()))) , 7: fibiter^#(b, c, x, y) -> c_7(if^#(lt(c, b), b, c, x, y), lt^#(c, b)) , 8: if^#(true(), b, c, x, y) -> c_8(fibiter^#(b, s(c), y, plus(x, y)), plus^#(x, y)) , 9: if^#(false(), b, c, x, y) -> c_9() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { plus^#(s(x), y) -> c_2(plus^#(x, y)) , lt^#(s(x), s(y)) -> c_5(lt^#(x, y)) , fib^#(x) -> c_6(fibiter^#(x, 0(), 0(), s(0()))) , fibiter^#(b, c, x, y) -> c_7(if^#(lt(c, b), b, c, x, y), lt^#(c, b)) , if^#(true(), b, c, x, y) -> c_8(fibiter^#(b, s(c), y, plus(x, y)), plus^#(x, y)) } Weak DPs: { plus^#(0(), y) -> c_1() , lt^#(x, 0()) -> c_3() , lt^#(0(), s(y)) -> c_4() , if^#(false(), b, c, x, y) -> c_9() } Weak Trs: { plus(0(), y) -> y , plus(s(x), y) -> s(plus(x, y)) , lt(x, 0()) -> false() , lt(0(), s(y)) -> true() , lt(s(x), s(y)) -> lt(x, y) , fib(x) -> fibiter(x, 0(), 0(), s(0())) , fibiter(b, c, x, y) -> if(lt(c, b), b, c, x, y) , if(true(), b, c, x, y) -> fibiter(b, s(c), y, plus(x, y)) , if(false(), b, c, x, y) -> 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. { plus^#(0(), y) -> c_1() , lt^#(x, 0()) -> c_3() , lt^#(0(), s(y)) -> c_4() , if^#(false(), b, c, x, y) -> c_9() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { plus^#(s(x), y) -> c_2(plus^#(x, y)) , lt^#(s(x), s(y)) -> c_5(lt^#(x, y)) , fib^#(x) -> c_6(fibiter^#(x, 0(), 0(), s(0()))) , fibiter^#(b, c, x, y) -> c_7(if^#(lt(c, b), b, c, x, y), lt^#(c, b)) , if^#(true(), b, c, x, y) -> c_8(fibiter^#(b, s(c), y, plus(x, y)), plus^#(x, y)) } Weak Trs: { plus(0(), y) -> y , plus(s(x), y) -> s(plus(x, y)) , lt(x, 0()) -> false() , lt(0(), s(y)) -> true() , lt(s(x), s(y)) -> lt(x, y) , fib(x) -> fibiter(x, 0(), 0(), s(0())) , fibiter(b, c, x, y) -> if(lt(c, b), b, c, x, y) , if(true(), b, c, x, y) -> fibiter(b, s(c), y, plus(x, y)) , if(false(), b, c, x, y) -> x } Obligation: innermost runtime complexity Answer: MAYBE Consider the dependency graph 1: plus^#(s(x), y) -> c_2(plus^#(x, y)) -->_1 plus^#(s(x), y) -> c_2(plus^#(x, y)) :1 2: lt^#(s(x), s(y)) -> c_5(lt^#(x, y)) -->_1 lt^#(s(x), s(y)) -> c_5(lt^#(x, y)) :2 3: fib^#(x) -> c_6(fibiter^#(x, 0(), 0(), s(0()))) -->_1 fibiter^#(b, c, x, y) -> c_7(if^#(lt(c, b), b, c, x, y), lt^#(c, b)) :4 4: fibiter^#(b, c, x, y) -> c_7(if^#(lt(c, b), b, c, x, y), lt^#(c, b)) -->_1 if^#(true(), b, c, x, y) -> c_8(fibiter^#(b, s(c), y, plus(x, y)), plus^#(x, y)) :5 -->_2 lt^#(s(x), s(y)) -> c_5(lt^#(x, y)) :2 5: if^#(true(), b, c, x, y) -> c_8(fibiter^#(b, s(c), y, plus(x, y)), plus^#(x, y)) -->_1 fibiter^#(b, c, x, y) -> c_7(if^#(lt(c, b), b, c, x, y), lt^#(c, b)) :4 -->_2 plus^#(s(x), y) -> c_2(plus^#(x, y)) :1 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). { fib^#(x) -> c_6(fibiter^#(x, 0(), 0(), s(0()))) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { plus^#(s(x), y) -> c_2(plus^#(x, y)) , lt^#(s(x), s(y)) -> c_5(lt^#(x, y)) , fibiter^#(b, c, x, y) -> c_7(if^#(lt(c, b), b, c, x, y), lt^#(c, b)) , if^#(true(), b, c, x, y) -> c_8(fibiter^#(b, s(c), y, plus(x, y)), plus^#(x, y)) } Weak Trs: { plus(0(), y) -> y , plus(s(x), y) -> s(plus(x, y)) , lt(x, 0()) -> false() , lt(0(), s(y)) -> true() , lt(s(x), s(y)) -> lt(x, y) , fib(x) -> fibiter(x, 0(), 0(), s(0())) , fibiter(b, c, x, y) -> if(lt(c, b), b, c, x, y) , if(true(), b, c, x, y) -> fibiter(b, s(c), y, plus(x, y)) , if(false(), b, c, x, y) -> x } Obligation: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Weak Usable Rules: { plus(0(), y) -> y , plus(s(x), y) -> s(plus(x, y)) , lt(x, 0()) -> false() , lt(0(), s(y)) -> true() , lt(s(x), s(y)) -> lt(x, y) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { plus^#(s(x), y) -> c_2(plus^#(x, y)) , lt^#(s(x), s(y)) -> c_5(lt^#(x, y)) , fibiter^#(b, c, x, y) -> c_7(if^#(lt(c, b), b, c, x, y), lt^#(c, b)) , if^#(true(), b, c, x, y) -> c_8(fibiter^#(b, s(c), y, plus(x, y)), plus^#(x, y)) } Weak Trs: { plus(0(), y) -> y , plus(s(x), y) -> s(plus(x, y)) , lt(x, 0()) -> false() , lt(0(), s(y)) -> true() , lt(s(x), s(y)) -> lt(x, y) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..