- WORD_DECIDE ``a && (b !! a) = a !! a && b``
<<HOL message: inventing new type variable names: 'a>>
> val it = |- a && (b !! a) = a !! a && b : thm

- WORD_DECIDE ``a + 2w <+ 4w = a <+ 2w \/ 13w <+ a :word4``
> val it = |- a + 2w <+ 4w = a <+ 2w \/ 13w <+ a : thm

- WORD_DECIDE ``a < 0w = 1w <+ a : word2``
> val it = |- a < 0w = 1w <+ a : thm

- WORD_DECIDE ``(?w:word4. 14w <+ w) /\ ~(?w:word4. 15w <+ w)``
> val it = |- (?w. 14w <+ w) /\ ~ ?w. 15w <+ w : thm