----------------------------------------------------------------------
WORD_SUB_CONV                                               (wordsLib)
----------------------------------------------------------------------
WORD_SUB_CONV : conv

DESCRIBE
The conversion {WORD_SUB_CONV} is designed to eliminate occurrences of
multiplication by a negative coefficient, introducing unary-minus (2’s
complement) and subtraction wherever possible.

EXAMPLE

> wordsLib.WORD_SUB_CONV ``a + -3w * b + -1w * c = -1w * d + e: 'a word``;
val it =
   |- (a + -3w * b + -1w * c = -1w * d + e) <=> (a - 3w * b - c = e - d):
   thm

> wordsLib.WORD_SUB_CONV ``-1w * a: 'a word``;
val it = |- -1w * a = -a: thm

wordsLib.WORD_SUB_CONV ``-1w * a + -2w * b: 'a word``;
val it =
   |- -1w * a + -2w * b = -(2w * b + a):
   thm


COMMENTS
This conversion forms the basis of {wordsLib.WORD_SUB_ss}. Care should be taken
when using this conversion in combination with other bit-vector tools. For
example, {wordsLib.WORD_ARITH_CONV} will undo all of the work of
{WORD_SUB_CONV}.

SEEALSO
wordsLib.WORD_SUB_ss.

----------------------------------------------------------------------