Trace Table (simulate in detail)

compute symbolically
( R >= Y --> Q,R := Q+1,R-Y ) o ( R >= Y and Y > 0 --> Q,R := Q+R/Y, R mod Y )

  condition            Q               R             Y
  _____________________________________________________________
  R >= Y               Q+1             R-Y
  R-Y >= Y and Y > 0   (Q+1)+(R-Y)/Y   (R-Y) mod Y  
  _____________________________________________________________
    ( R >=Y and R-Y >= Y and Y > 0 --> Q,R := Q+R/Y, R mod Y )

   R-Y >= Y ==> R >= 2Y 
   R >= Y and R >= 2Y ==> R >= 2Y