compute symbolically ( R < Y --> ident ) o ( R < Y --> ident )
condition Q R Y _______________________________________________ R < Y R < Y _______________________________________________ ( R < Y --> Q,R := Q, R )