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 --> 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 ) ) = ( R >= Y --> Q,R := Q+1,R-Y ) o ( R < Y --> ident ) | ( R >= Y --> Q,R := Q+1,R-Y ) o ( R >= Y and Y > 0 --> Q,R := Q+R/Y, R mod Y ) | ( R < Y --> ident ) o ( R < Y --> ident ) | ( R < Y --> ident ) o ( R >= Y and Y > 0 --> Q,R := Q+R/Y, R mod Y )