Trace Table: Symbolic Execution

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