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
- show dom(f) = dom([WHILE])
- show f = [IF] o f where IF is made of the loop components
[IF] = ( R >= Y --> Q,R := Q+1,R-Y ) | ( R < Y --> ident )
<<< watch out here
so compute the composition [IF] o f =
( ( R >= Y --> Q,R := Q+1,R-Y ) | ( R < Y --> ident ) )
o ( ( R < Y --> ident ) | ( R >= Y and Y > 0 --> Q,R := Q+R/Y, R mod Y ) )