(VAR b c x y )
(STRATEGY INNERMOST)
(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))
        
)