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 )