The conversion WORD_MOD_BITS_CONV replaces instances of word_mod by a power
of two with applications of word_bits.
EXAMPLE
> wordsLib.WORD_MOD_BITS_CONV ``word_mod w 8w : word16``;
val it = |- word_mod w 8w = (2 -- 0) w: thm
wordsLib.WORD_MOD_BITS_CONV ``word_mod w 1w : word16``;
val it = |- word_mod w 1w = 0w: thm
COMMENTS
This conversion requires the word length to be known.