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 --> 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 )After symbolic execution (click each clause to see its trace table):
( 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 ) | ( false --> Q,R := Q+R/Y, R mod Y )