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 The input cannot be shown compatible Arrrr..