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 )Rewriting the conditions:
R-Y >= Y ==> R >= 2Y R >= Y and R >= 2Y ==> R >= 2Yso we get