Lines Matching refs:word
34 ``!v w. (v ?? w = 0w) = (v = w:'a word)``,
60 ``!n. (n2w n) && 1w = n2w (n MOD 2):'a word``,
67 ``!n. (n2w n) && 3w = n2w (n MOD 4):'a word``,
74 ``!n. (n2w n) && 7w = n2w (n MOD 8):'a word``,
316 ``!n m. (n2w n + n2w m = n2w (n + m):'a word) /\
317 (x + n2w n + n2w m = x + n2w (n + m):'a word) /\
318 (x - n2w n - n2w m = x - n2w (n + m):'a word)``,
322 ``!n m. n2w n - (n2w m) :'a word =
334 ``!x n m. x - n2w m + n2w n :'a word = if n < m then x - (n2w (m-n)) else x + n2w (n-m)``,
340 ``!x n m. x + n2w n - n2w m :'a word = if n < m then x - (n2w (m-n)) else x + n2w (n-m)``,
353 ``!x m. 0 < m /\ w2n x + m < dimword (:'a) ==> ~((x:'a word) + n2w m = 0w)``,
599 ((~(word_msb (a - b) = word_msb a) /\ ~(word_msb b = word_msb a) = word_msb (a - b)) = b <= a:('a word))``,
601 val lemma1 = prove(``!a:'a word b. (b <=+ a) /\ ~(a = b) = b <+ a``,
603 val lemma2 = prove(``!a:'a word b. ~(a = b) /\ (b <=+ a) = b <+ a``,
605 val lemma3 = prove(``!a:'a word b. (b <= a) /\ ~(a = b) = b < a``,
607 val lemma4 = prove(``!a:'a word b. ~(a = b) /\ (b <= a) = b < a``,
617 ``!m k. ((n2w m):'a word) << k = n2w (m * 2 ** k)``,
624 ((w = w + x) = (x = 0w)) /\ ((w + v = w) = (v = 0w: 'a word))``,
671 ``!w:'a word. 2w * w = w + w``,
676 ``!x y:'a word.
686 ``!(x:'a word) n. x + n2w n * x = n2w (n + 1) * x``,
692 ``!(x:'a word) n p.