(VAR b c x y )
(RULES 
        plus(0, y) -> y
        plus(s(x), y) -> s(plus(x, y))
        lt(0, s(y)) -> true
        lt(x, 0) -> false
        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(false, b, c, x, y) -> x
        if(true, b, c, x, y) -> fibiter(b, s(c), y, plus(x, y))
        
)