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 )
( R >= Y and R < 2Y --> Q,R := Q+1, R-Y ) | ( R >= 2Y and Y > 0 --> Q,R := Q+R/Y, R mod Y ) | ( R < Y --> identity )Rewrite the condition on the first clause:
= ( Y <= R < 2Y --> Q,R := Q+1, R-Y ) | ( R >= 2Y and Y > 0 --> Q,R := Q+R/Y, R mod Y ) | ( R < Y --> identity )Note that when Y <= R < 2Y we have these:
Y < 2Y which implies Y > 0 R/Y = 1 R-Y = R mod Y