# 2.2  Bit Slices

Since bitn is defined as a special case of bits, we discuss the latter function first.

(bits-bvecp) For all , , and , is an -bit vector.

PROOF: By Lemmas 1.1.1 and 1.2.2, . By Lemma 1.2.3,

Example: Let . Then

is a 3-bit vector and

is a 4-bit vector.

PROOF:

PROOF: By Lemma 1.2.21,

If the lower limit of a bit slice is 0, it reduces to a call to :

PROOF:

Calls to bits may often be eliminated by means of the following.

(bits-tail) Let and . If is an -bit vector, then .

PROOF: Since , by Lemmas 2.2.4 and 1.2.6,

Lemma 2.2.5 may be generalized to cover negative bit vectors:

PROOF: For , by Lemmas 2.2.4, 1.2.15, and 1.2.6,

If , then is the bit vector of width consisting of all 1's:

(neg-bits-1) Let , , and . If and , then .

PROOF: By Lemmas 2.2.4 and 1.2.15, . Thus, by Definition 2.0.1, Lemma 1.1.4, and Definition 1.1.1,

Corollary 2.2.8   (bits-minus-1) If , , and , then .

The following results are derived from corresponding properties of mod.

(bits-bits-sum, bits-bits-diff, bits-bits-prod) For all , , , , and , if and , then

(a) ;

(b) ;

(c) .

PROOF: By Definition 2.0.1 and Lemmas 1.2.18 and 1.2.20,

The other results follow similarly from Lemmas 1.2.19 and 1.2.23.

By expanding , we may express a bit slice in terms of the floor alone:

PROOF: Applying Definitions 2.0.1 and 1.2.1 and Lemma 1.1.4, we have

PROOF: This follows from Definition 1.2.1 and Lemmas 2.2.10 and 1.1.5:

In most cases of interest, the index arguments of satisfy . However, the following two lemmas are worth noting.

PROOF: Since , . Applying Definition 1.2.1 and Lemma 1.1.1, we have

PROOF: By Lemma 1.2.3,

and hence

which, together with Lemma 2.2.1, implies

Here is another case in which a bit slice may be reduced to 0:

(bvecp-bits-0) Let , , and . If is a -bit vector, then .

PROOF: By Lemmas 1.2.2 and 1.2.5,

Therefore, by Lemma 1.1.3 and Definition 1.1.1,

which, together with Lemma 2.2.1, implies

Corollary 2.2.15   (bits-0) For all and , .

According to our next lemma, a slice of a right-shifted bit vector, , may always be represented as a slice of .

PROOF: Let and , so that and . Then

where . Hence,

and by Definition 2.0.1 and Lemma 1.1.5,

PROOF: Applying Lemma 2.2.16, Definition 2.0.1, and Lemma 2.2.4 in succession, we have

PROOF: If , then by Definition 2.0.1 and Lemma 1.2.22,

If , then by Definition 2.0.1 and Corollary 1.2.9,
 0

and by Lemma 2.2.13

The next lemma provides an alternate expression for a left-shifted bit slice with lower limit 0:

PROOF: By Lemmas 1.2.22 and 2.2.4,

We note two cases in which a bit slice of can be simplified.

(bits-plus-mult-1) Let , , , , and . If and , then

PROOF: By Lemma 2.2.13, we may assume that . Since ,

We apply Lemma 2.2.16, substituting for , for , and for :

PROOF: Since , where , Lemma 1.2.15 implies The lemma now follows from Lemma 2.2.2

Here is an important lemma that decomposes a slice into two subslices.

PROOF: The proof consists of three applications of Lemma 2.2.10:

and hence,

Compositions of bit slices may be reduced by means of the following.

PROOF: By Lemma 2.2.16,

If , then this reduces, by Corollary 1.2.21, to

On the other hand, if , then by Lemma 1.2.3,

and by Lemma 1.2.6, the expression reduces instead to

David Russinoff 2017-08-01