1\DOC
2
3\TYPE {WORD_BIT_EQ_CONV : conv}
4
5\SYNOPSIS
6
7Conversion based on {WORD_BIT_EQ_ss}.
8
9\DESCRIBE
10
11The conversion {WORD_BIT_EQ_CONV} performs simplification using {fcpLib.FCP_ss}.
12
13\EXAMPLE
14{
15- WORD_BIT_EQ_CONV ``a << 2 >>> 1 = ((5 -- 0) a << 1) :word8``
16> val it = |- (a << 2 >>> 1 = (5 -- 0) a << 1) = T : thm
17}
18
19\SEEALSO
20
21wordsLib.WORD_BIT_EQ_ss, blastLib.BBLAST_CONV, wordsLib.WORD_ARITH_CONV,
22wordsLib.WORD_LOGIC_CONV, wordsLib.WORD_MUL_LSL_CONV, wordsLib.WORD_CONV,
23wordsLib.WORD_EVAL_CONV
24
25\ENDDOC
26