Trace Table

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

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

Rewriting the conditions:

   R < Y and R >= Y ==> false

so we get

( false --> Q,R := Q+R/Y, R mod Y )