1\DOC 2 3\TYPE {WORD_SUB_CONV : conv} 4 5\DESCRIBE 6 7The conversion {WORD_SUB_CONV} is designed to eliminate occurrences of 8multiplication by a negative coefficient, introducing unary-minus (2's 9complement) and subtraction wherever possible. 10 11\EXAMPLE 12{ 13> wordsLib.WORD_SUB_CONV ``a + -3w * b + -1w * c = -1w * d + e: 'a word``; 14val it = 15 |- (a + -3w * b + -1w * c = -1w * d + e) <=> (a - 3w * b - c = e - d): 16 thm 17 18> wordsLib.WORD_SUB_CONV ``-1w * a: 'a word``; 19val it = |- -1w * a = -a: thm 20 21wordsLib.WORD_SUB_CONV ``-1w * a + -2w * b: 'a word``; 22val it = 23 |- -1w * a + -2w * b = -(2w * b + a): 24 thm 25} 26 27\COMMENTS 28 29This conversion forms the basis of {wordsLib.WORD_SUB_ss}. Care should be taken 30when using this conversion in combination with other bit-vector tools. For 31example, {wordsLib.WORD_ARITH_CONV} will undo all of the work of 32{WORD_SUB_CONV}. 33 34\SEEALSO 35 36wordsLib.WORD_SUB_ss 37 38\ENDDOC 39