Trace Table

compute symbolically ( R >= Y --> Q,R := Q+1,R-Y ) o ( R < Y --> ident )

  condition     Q             R           Y
  _______________________________________________
  R >= Y        Q+1           R-Y
  R-Y < Y     
  _______________________________________________
 
    ( R >= Y and R-Y < Y --> Q,R := Q+1, R-Y )

Rewriting the conditions.

   R-Y < Y ==> R < 2Y

so we get

( R >= Y and R < 2Y --> Q,R := Q+1, R-Y )