Lines Matching refs:word
65 ``IncPC ()``, ``PSR_IT``, ``(h >< l) : 'a word -> 'b word``] @
590 : arm_state -> ('a word # bool) # arm_state``
601 ``(if n = 0 then (x: 'a word,s) else (x #>> n, ^st)) = (x #>> n, s)``
605 ``ROR (x: 'a word, n)``
727 GSYM (Q.ISPEC `MemA x s : 'a word # arm_state` pairTheory.PAIR)
976 ``(a: 'a word - 4w * b + 4w + 4w * c = a + 4w * (c - b + 1w)) /\
1334 ``aligned c (a + b : 'a word)``
3267 [``Extend (T, w:'a word): 'b word``,
3268 ``Extend (F, w:'a word): 'b word``]
4085 ((((a : 'a word) @@ (b : 'b word)) : 'c word) ' n = b ' n)`,
4093 ((((a : 'a word) @@ (b : 'b word)) : 'c word) ' n =