1\DOC 2 3\TYPE {WORD_CANCEL_ss : ssfrag} 4 5\SYNOPSIS 6 7Simplification fragment for words. 8 9\KEYWORDS 10 11simplification, words. 12 13\DESCRIBE 14 15The fragment {WORD_CANCEL_ss} helps simplify linear equations over bit-vectors. 16This fragment is designed to work in concert with {wordsLib.WORD_ARITH_ss}. The 17procedure will endeavour to ensure that all coefficients appear in positive 18form. Furthermore, the leftmost coefficient will be highest on the left-hand 19side of equations. 20 21\EXAMPLE 22 23{ 24> SIMP_CONV (pure_ss++wordsLib.WORD_ARITH_ss++wordsLib.WORD_CANCEL_ss) [] 25 ``-3w * b + a = -2w * a + b: word32``; 26val it = 27 |- (-3w * b + a = -2w * a + b) <=> (4w * b = 3w * a): 28 thm 29} 30 31\COMMENTS 32 33This fragment can be viewed as a superior version of {wordsLib.WORD_ARITH_EQ_ss}. 34 35\SEEALSO 36 37wordsLib.WORD_ARITH_ss, wordsLib.WORD_ARITH_EQ_ss 38 39\ENDDOC 40