[IF] = [ if R >= Y then Q := Q+1 ; R := R-Y endif ] = ( R >= Y --> Q,R := Q+1,R-Y ) | ( R < Y --> ident )
The second clause is important... don't leave it out... AND, don't get confused. An alternate to write the function [IF] is
( R >= Y --> Q,R := Q+1,R-Y ) | ( )If you choose this notation, don't forget that the second clause is not the identity function. It is the identity function restricted to domain elements where ( R < Y ). If you forget, and treat it as identity, your trace tables will get fouled up.