# 2.1  Recognizing Bit Vectors

Non-negative bit vectors of a given width are recognized by the following predicate:

Definition 2.1.1   (bvecp) Let and . Then

Note that no natural number has a well-defined width, e.g., is a 4-bit vector, but more generally a -bit vector for all . 0 is a -bit vector for all .

(bvecp-monotone) Let , , and . If and is an -bit vector, then is an -bit vector.

PROOF: Since and , we have , which implies

(bvecp-shift-down) Let , , and . If is an -bit vector, then is an -bit vector.

PROOF: By Definition 2.1.1,

(bvecp-shift-up) Let , , and . If is an -bit vector, then is an -bit vector.

PROOF: By Definition 2.1.1,

(bvecp-product) Let , , and . If is an -bit vector and is an -bit vector, then is an -bit vector.

PROOF: and

(bvecp-1-rewrite) Let . If is a 1-bit vector, then .

PROOF:   .

David Russinoff 2017-08-01