Proving the LOOP function
We must demonstrate that our guess is good, i.e.
f = [WHILE]
= ( R < Y --> ident ) | ( R >= Y and Y > 0 --> Q,R := Q+R/Y, R mod Y )
- show f behaves like identity when the loop boolean is false
In this case, we constructed f exactly so this will happen
( ~( R >= Y ) --> ident ) is identity function restricted to the loop boolean false
rewrite as ( R < Y --> ident ), this is exactly one clause of f