Lines Matching defs:b3
938 `(!p. ((if p then v2w [b1; b2; b3] else v2w [b4; b5; b6]) = 7w : word3) =
939 (if p then b1 /\ b2 /\ b3 else b4 /\ b5 /\ b6)) /\
940 (!p. ((if p then v2w [b1; b2] else v2w [b3; b4]) = 0w : word2) =
941 (if p then ~b1 /\ ~b2 else ~b3 /\ ~b4))`,
1013 val (b3, b4) = Lib.split_after 8 l
1015 (b1, b2, b3, b4)
1032 val (b1, b2, b3, b4) = bytes4 v
1034 if e then build_byte 24 b4 @ build_byte 16 b3 @
1036 else build_byte 24 b3 @ build_byte 16 b4 @
1833 (t, w2w (v2w [b7; b6; b5; b4; b3; b2; b1; b0; F; F] : word10))``
1889 ``word_bit 8 (v2w [b8; b7; b6; b5; b4; b3; b2; b1; b0] : word9)``