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