compute symbolically
( R >= Y --> Q,R := Q+1,R-Y )
o ( R >= Y and Y > 0 --> Q,R := Q+R/Y, R mod Y )
We do this with a table for recording the effects of symbolically
executing each statement of the function we are computing.
The table has one column or each variable involved in the
computation. It also has one column for noting the
current symbolic form of conditions when they are encountered.
condition Q R Y _____________________________________________________________ R >= Y Q+1 R-Y R-Y >= Y and Y > 0
The condition "R >= Y and Y > 0" is recorded in the table, but the current symbolic table entries are substituted in for the variable names in the condition expression. Here, this means "R" is replaced with "R-Y".