var dx: real, dy:real;
begin

assume not (dx == 0 and dy == 0);

/* fabs(dy) > fabs(dx) */
if ((dy > 0 and -dy < dx and dx < dy) or (-dy > 0 and dy < dx and dx < -dy)) then
 assume not dy == 0;
else 
 assume not dx == 0;
endif;

end