WORD_BIT_EQ_CONV

wordsLib.WORD_BIT_EQ_CONV : conv

Conversion based on WORD_BIT_EQ_ss.

The conversion WORD_BIT_EQ_CONV performs simplification using fcpLib.FCP_ss.

Example

> wordsLib.WORD_BIT_EQ_CONV “a << 2 >>> 1 = ((5 -- 0) a << 1) :word8”
val it = ⊢ a ≪ 2 ⋙ 1 = (5 -- 0) a ≪ 1 ⇔ T: thm

See also

wordsLib.WORD_BIT_EQ_ss, blastLib.BBLAST_CONV, wordsLib.WORD_ARITH_CONV, wordsLib.WORD_LOGIC_CONV, wordsLib.WORD_MUL_LSL_CONV, wordsLib.WORD_CONV, wordsLib.WORD_EVAL_CONV