WORD_LOGIC_CONV

wordsLib.WORD_LOGIC_CONV : conv

Conversion based on WORD_LOGIC_ss.

The conversion WORD_LOGIC_CONV converts word logic expressions into a canonical form.

Example

> wordsLib.WORD_LOGIC_CONV “a && (b !! ~a !! c)”
val it = ⊢ a && (b ‖ ¬a ‖ c) = a && b ‖ a && c: thm

See also

wordsLib.WORD_LOGIC_ss, wordsLib.WORD_ARITH_CONV, wordsLib.WORD_MUL_LSL_CONV, wordsLib.WORD_CONV, wordsLib.WORD_BIT_EQ_CONV, wordsLib.WORD_EVAL_CONV