> > The simplification bit_lsh(x, - 3) => x/2^(- 3) is wrong! bit_lsh(x,i) == floor(x/2^i) for integer x,i. Not clear whether that is a useful simplification.