# Need mathematical help with loop invariant

I was wondering about following. I have condition in my program that I want to prove its correctness (I won't write the whole problem, just the part I'm curious about):

• if $$w \leq r$$ then $$r:=r-w$$;

What I'm trying to do is form loop invariant and I have the following problem (might sound silly but I'm clueless as of what to write).

$$r_{j+1}= r_{j} + w_j \times {condition}$$

I want to find a condition that holds following stuff: if $$w\leq r$$ return $$1$$ else return $$0$$ so I could just put it mathematically in $$r_{j+1}$$ above so it holds. I have no clue which expression should I form that gives $$1$$ if $$w \leq r$$ else $$0$$. I would be grateful if someone could help me.

$$f(x,y) = \begin{cases} 1, \quad x \leq y\\ 0, \quad otherwise\\\end{cases}$$