(COMMENT 
 fibiter has bound, counter, fib(counter), fib(counter+1) as arguments
)
(VAR x y c a b)
(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))
)