# 2.3  Bit Extraction

Instead of Definition 2.0.2, we could have defined more directly as follows.

PROOF: By Lemmas 2.2.10 and 1.1.5 and Definition 1.2.1,

Here is an equivalent recursive definition that may be used in inductive proofs.

PROOF: The base case is the case of Lemma 2.3.1. The inductive case is an instance of Lemma 2.2.16, with and

Many of the results of this section are special cases of the results of Section 2.2.

(bitn-bvecp-forward) For all and , is a bit vector of width .

PROOF: This follows from Definition 2.0.2 and Lemma 2.2.1

PROOF: This is a case of Lemma 2.2.12

PROOF: This is a case of Lemma 2.2.15

PROOF: This is a case of Lemma 2.2.5

PROOF: This follows from Lemmas 2.3.6 and 2.3.6

PROOF: This is a case of Corollary 2.2.3

(bvecp-bitn-0) For all , if is an -bit vector, then .

PROOF: This is a case of Lemma 2.2.14

PROOF: This is a case of Lemma 2.2.7

PROOF: This is a case of Corollary 2.2.8

(neg-bitn-2) Let , , and . If and , then .

PROOF: Since , . By Lemma 2.3.1,

PROOF: This is a case of Lemma 2.3.12

PROOF: This is a case of Lemma 2.2.18

PROOF: This is a case of Lemma 2.2.16

(bitn-bits) For all , , , and , if , then

PROOF: This is a case of Lemma 2.2.23

PROOF: This is a case of Lemma 2.2.22

PROOF: This is a case of Lemma 2.2.22

The corollary of the following lemma justifies the informal characterization of bits given at the beginning of this chapter.

PROOF: If , then both sides of the equation reduce to 0 by Lemma 2.2.13. We proceed by induction. Thus, for , applying Lemma 2.3.17, we have

(sumbits-thm) If , , and is an n-bit vector, then

PROOF: This follows from Lemmas 2.3.19 and 2.2.5

The following lemma allows us to define a bit vector in a natural way as a sequence of bits. That is, given a sequence, of 1-bit vectors , we may say, without ambiguity, Let be the bit vector of width defined by for .... The existence of such a bit vector is guaranteed by Lemma 2.3.21; its uniqueness is ensured by Corollary 2.3.20.

(sum-bitn) Let , where and , . Then for , .

PROOF: Let and . Then

Since

by Lemma 1.2.15. But since

and

by Lemma 1.2.6. Thus, by Definitions 2.0.1 and 2.0.2,

A bit vector is uniquely determined by its binary representation:

(bit-diff-diff) Let and . If for all , then .

PROOF: The proof is by induction on .

Suppose . We must show that for some , . We may assume that , and hence , for otherwise

Since and , at least one of and must be different from both 0 and -1, and hence, by Lemma 1.1.6,

By induction, there exists such that , and consequently, by Lemma 2.3.15,

The remaining lemmas of this section deal with the computation of in various special cases.

(bvecp-bitn-1) For all , if is an -bit vector and , then .

PROOF: Since , , and by Definition 1.1.1, . Now by Lemma 2.3.1,

We have the following generalization of Lemma 2.3.23.

(bvecp-bitn-2) Let and , and let be an -bit vector. If and , then .

PROOF: Since , , and by Definition 1.1.1, . Now by Lemma 2.3.1,

Only one bit of a power of 2 is set.

PROOF: By Lemma 2.3.1,

PROOF: If , then is an -bit vector and Lemma 2.3.9 applies. If , then

When a power of 2 is added to a bit vector, the corresponding bit is toggled:

PROOF: By Lemma 2.3.1, and

which reduces, by Lemma 1.1.4, to . The result follows from Lemma 1.2.27

When a multiple of a power of 2 is added to a bit vector, the lower bits are unaffected:

PROOF: By Lemmas 2.3.1 and 1.1.4,

which reduces, by Lemma 1.1.4, to . The result follows from Lemmas 1.2.15 and 2.3.1

David Russinoff 2017-08-01