[isabelle] And mask
sorry for my english. I would be delighted if you could help me.
I use theory WordMain and i would like to show the following lemma:
lemma "[| uint w < 256 |] ==> (w :: 16 word) AND 0x00FF = w"
w is a word with length 16 and if the value of w is < as 256, then after application of mask the value don't change.
Thanks in advance!
Computer Bild Tarifsieger! GMX FreeDSL - Telefonanschluss + DSL
für nur 17,95 ¿/mtl.!* http://dsl.gmx.de/?ac=OM.AD.PD003K11308T4569a
This archive was generated by a fusion of
Pipermail (Mailman edition) and