3.1  Binary Operations

The binary functions logand, logior, and logxor are ACL2 primitives. The “definitions” presented below are actually formalized as theorems derived from ACL2 axioms.

Definition 3.1.1   (logand-def) For all $ x \in \mathbb{Z}$ and $ y
\in \mathbb{Z}$,

$\displaystyle \mathit{logand}(x,y) = \left\{\begin{array}{ll}
0 & \mbox{if $x=...
...+ \mathit{logand}(x \bmod 2, y \bmod 2) & \mbox{otherwise}. \end{array} \right.$

The definition is extended recursively to $ k$ arguments for arbitrary $ k \geq 2$:

$\displaystyle \mathit{logand}(x_1,\ldots,x_k) = \mathit{logand}(x_1, \mathit{logand}(x_2,\ldots,x_k)).
$

It is not obvious that Definition 3.1.1 is an admissible recursive definition. In order to establish that it is satisfied by a unique function, it will suffice to demonstrate the existence of a measure function $ \mu: \mathbb{Z} \times \mathbb{Z} \to \mathbb{N}$ that strictly decreases on each recursive call. Thus, we define

$\displaystyle \mu(x, y) = \left\{\begin{array}{ll}
0 & \mbox{if $x=y$}\\
\vert xy\vert & \mbox{if $x \neq y$.}\end{array}\right.$

We must show that $ \mu$ satisfies the following two inequalities, corresponding to the two recusive calls of logand, under the restrictions $ x \neq 0$, $ y \neq 0$, and $ x \neq y$:

(1) $ \mu(\lfloor x/2 \rfloor, \lfloor y/2 \rfloor) < \mu(x, y)$.

(2) $ \mu(x \bmod 2, y \bmod 2) < \mu(x, y).$.

Since the restrictions imply that at least one of $ x$ and $ y$ is neither 0 nor -1, (1) follows from Lemma 1.1.6. To establish (2), note that either $ x \bmod 2 = 0$, $ y \bmod 2 = 0$, or $ x \bmod 2 = 1 = y \bmod 2$. In any case,

$\displaystyle \mu(x \bmod 2, y \bmod 2) = 0 < \vert xy\vert = \mu(x, y).
$

Precisely the same argument applies to the following two definitions.

Definition 3.1.2   (logior-def) For all $ x \in \mathbb{Z}$ and $ y
\in \mathbb{Z}$,

$\displaystyle \mathit{logior}(x,y) = \left\{\begin{array}{ll}
y & \mbox{if $x=...
...+ \mathit{logior}(x \bmod 2, y \bmod 2) & \mbox{otherwise}. \end{array} \right.$

The definition is extended recursively to $ k$ arguments for arbitrary $ k \geq 2$:

$\displaystyle \mathit{logior}(x_1,\ldots,x_k) = \mathit{logior}(x_1, \mathit{logior}(x_2,\ldots,x_k)).
$

Definition 3.1.3   (logxor-def) For all $ x \in \mathbb{Z}$ and $ y
\in \mathbb{Z}$,

$\displaystyle \mathit{logxor}(x,y) = \left\{\begin{array}{ll}
y & \mbox{if $x=...
...+ \mathit{logxor}(x \bmod 2, y \bmod 2) & \mbox{otherwise}. \end{array} \right.$

The definition is extended recursively to $ k$ arguments for arbitrary $ k \geq 2$:

$\displaystyle \mathit{logxor}(x_1,\ldots,x_k) = \mathit{logxor}(x_1, \mathit{logxor}(x_2,\ldots,x_k)).
$

Notation: We adopt the following standard notation:

$ \blacktriangleright$ $ x \;\verb!&!\; y = \mathit{logand}(x, y)$;

$ \blacktriangleright$ $ x \;\verb!\vert!\; y = \mathit{logior}(x, y)$;

$ \blacktriangleright$ $ x \;\verb!^!\; y = \mathit{logxor}(x, y)$.

  (logand-bnd) If $ x \in \mathbb{N}$ and $ y
\in \mathbb{Z}$, then $ 0 \leq x \;\verb!&!\; y \leq x$.

PROOF: We may assume that $ x \neq 0$, $ y \neq 0$, and $ x \neq y$. Thus,

$\displaystyle x \;\verb!&!\; y = 2(\lfloor x/2 \rfloor \;\verb!&!\; \lfloor y/2 \rfloor) + x \bmod 2 \;\verb!&!\; y \bmod 2
$

and by induction,

$\displaystyle 0 \leq x \;\verb!&!\; \leq 2\lfloor x/2 \rfloor + x \bmod 2 = x. $

  (logand-bvecp) If $ x$ is an $ n$-bit vector, where $ n \in \mathbb{N}$, and $ y
\in \mathbb{Z}$, then $ x \;\verb!&!\; y$ is an $ n$-bit vectors.

PROOF: By Lemma 3.1.1, $ 0 \leq x \;\verb!&!\; y \leq x < 2^n$ 

  (logior-bvecp, logxor-bvecp) If $ x$ and $ y$ and $ n$-bit vectors, where $ n \in \mathbb{N}$, then so are $ x \;\verb!\vert!\; y$ and $ x \;\verb!^!\; y$.

PROOF: The same argument applies to both operations. The claim is trivial if $ n = 0$, $ x = 0$, $ y = 0$, or $ x = y$. In all other cases, $ \lfloor x/2 \rfloor$ and $ \lfloor y/2 \rfloor$ are $ (n-1)$-bit vectors and by induction, so is, for example, $ \lfloor x/2 \rfloor \;\verb!\vert!\; \lfloor y/2 \rfloor$. Thus,

$\displaystyle x \;\verb!&!\; y = 2(\lfloor x/2 \rfloor \;\verb!\vert!\; \lfloor...
...(x \bmod 2) \;\verb!\vert!\; (y \bmod 2)
\leq 2 \cdot (2^{n-1} - 1) + 1
< 2^n. $

  (logand-mod,logior-mod,logxor-mod) For all $ x \in \mathbb{Z}$, $ y
\in \mathbb{Z}$, and $ n \in \mathbb{N}$,

(a) $ (x \;\verb!&!\; y) \bmod 2^n = (x \bmod 2^n) \;\verb!&!\; (y \bmod 2^n)$
(b) $ (x \;\verb!\vert!\; y) \bmod 2^n = (x \bmod 2^n) \;\verb!\vert!\; (y \bmod 2^n)$
(c) $ (x \;\verb!^!\; y) \bmod 2^n = (x \bmod 2^n) \;\verb!^!\; (y \bmod 2^n)$

PROOF: We present the proof for (a); (b) and (c) are similar.

We may assume that $ n > 0$, $ x \neq 0$, $ y \neq 0$, and $ x \neq y$. By Definition 3.1.1 and Lemma 1.2.18,

$\displaystyle (x \;\verb!&!\; y) \bmod 2^n$ $\displaystyle =$ $\displaystyle \left(2 \cdot (\lfloor x/2 \rfloor \;\verb!&!\; \lfloor y/2 \rfloor) + (x \bmod 2) \;\verb!&!\; (y \bmod 2)\right) \bmod 2^n$  
  $\displaystyle =$ $\displaystyle \left(\left(2 \cdot (\lfloor x/2 \rfloor \;\verb!&!\; \lfloor y/2...
...loor)\right) \bmod 2^n + (x \bmod 2) \;\verb!&!\; (y \bmod 2)\right) \bmod 2^n.$  

By Lemma 1.2.22, induction, Lemma 2.2.4, and Lemma 2.2.17, the first addend my be written as
$\displaystyle \left(2 \cdot (\lfloor x/2 \rfloor \;\verb!&!\; \lfloor y/2 \rfloor)\right) \bmod 2^n$ $\displaystyle =$ $\displaystyle 2 \cdot \left((\lfloor x/2 \rfloor \;\verb!&!\; \lfloor y/2 \rfloor) \bmod 2^{n-1}\right)$  
  $\displaystyle =$ $\displaystyle 2 \cdot \left((\lfloor x/2 \rfloor \bmod 2^{n-1}) \;\verb!&!\; (\lfloor y/2 \rfloor \bmod 2^{n-1})\right)$  
  $\displaystyle =$ $\displaystyle 2 \cdot \left(\lfloor x/2 \rfloor[n-2:0] \;\verb!&!\; \lfloor y/2 \rfloor[n-2:0]\right)$  
  $\displaystyle =$ $\displaystyle 2 \cdot \left(\lfloor x[n-1:0]/2 \rfloor \;\verb!&!\; \lfloor y[n-1:0]/2 \rfloor\right),$  

and by Lemmas 2.3.2 and 2.3.16, the second addend is

$\displaystyle (x \bmod 2) \;\verb!&!\; (y \bmod 2) = x[0] \;\verb!&!\; y[0] = x...
...\;\verb!&!\; y[n-1:0][0] = (x[n-1:0] \bmod 2) \;\verb!&!\; (y[n-1:0] \bmod 2).
$

Thus, by Definition 3.1.1 and Lemmas 3.1.2 and 2.2.4,
$\displaystyle (x \;\verb!&!\; y) \bmod 2^n$ $\displaystyle =$ $\displaystyle \left(2 \cdot \left(\lfloor x[n-1:0]/2 \rfloor \;\verb!&!\; \lflo...
...or\right)
+ (x[n-1:0] \bmod 2) \;\verb!&!\; (y[n-1:0] \bmod 2)\right) \bmod 2^n$  
  $\displaystyle =$ $\displaystyle \left(x[n-1:0] \;\verb!&!\; y[n-1:0]\right) \bmod 2^n$  
  $\displaystyle =$ $\displaystyle x[n-1:0] \;\verb!&!\; y[n-1:0]$  
  $\displaystyle =$ $\displaystyle (x \bmod 2^n) \;\verb!&!\; (y \bmod 2^n). $  

  (fl-logand,fl-logior,fl-logxor) For all $ x \in \mathbb{Z}$, $ y
\in \mathbb{Z}$, and $ n \in \mathbb{N}$,

(a) $ \lfloor (x \;\verb!&!\; y)/2^n \rfloor = \lfloor x/2^n \rfloor \;\verb!&!\; \lfloor y/2^n \rfloor$;
(b) $ \lfloor (x \;\verb!\vert!\; y)/2^n \rfloor = \lfloor x/2^n \rfloor \;\verb!\vert!\; \lfloor y/2^n \rfloor$;
(c) $ \lfloor (x \;\verb!^!\; y)/2^n \rfloor = \lfloor x/2^n \rfloor \;\verb!^!\; \lfloor y/2^n \rfloor$.

PROOF: We present the proof for (a); (b) and (c) are similar.

We may assume that $ n > 0$, $ x \neq 0$, $ y \neq 0$, and $ x \neq y$. By Lemma 1.1.5, induction, and Definition 3.1.1,

$\displaystyle \lfloor (x \;\verb!&!\; y)/2^n \rfloor$ $\displaystyle =$ $\displaystyle \left\lfloor \lfloor (x \;\verb!&!\; y)/2^{n-1} \rfloor /2 \right\rfloor$  
  $\displaystyle =$ $\displaystyle \left\lfloor (\lfloor x/2^{n-1} \rfloor \;\verb!&!\; \lfloor y/2^{n-1} \rfloor)/2 \right\rfloor$  
  $\displaystyle =$ $\displaystyle \left\lfloor \lfloor x/2^{n-1} \rfloor/2 \rfloor \;\verb!&!\; \lfloor x/2^{n-1} \rfloor/2 \rfloor\right\rfloor$  
  $\displaystyle =$ $\displaystyle \left\lfloor x/2^n \rfloor \;\verb!&!\; \lfloor y/2^n \right\rfloor. $  

  (logand-cat,logior-cat,logxor-cat)
For all $ x_1 \in \mathbb{N}$, $ y_1 \in \mathbb{N}$, $ x_2 \in \mathbb{N}$, $ y_2 \in \mathbb{N}$, $ m \in \mathbb{N}$, and $ n \in \mathbb{N}$,

(a) $ \{x_1[m$-$ 1:0],y_1[n$-$ 1:0]\} \;\verb!&!\; \{x_2[m$-$ 1:0],y_2[n$-$ 1:0]\}$
            = $ \{x_1[m$-$ 1:0] \;\verb!&!\; x_2[m$-$ 1:0],y_1[n$-$ 1:0] \;\verb!&!\; y_2[n$-$ 1:0]\}$

(b) $ \{x_1[m$-$ 1:0],y_1[n$-$ 1:0]\} \;\verb!\vert!\; \{x_2[m$-$ 1:0],y_2[n$-$ 1:0]\}$
            = $ \{x_1[m$-$ 1:0] \;\verb!\vert!\; x_2[m$-$ 1:0],y_1[n$-$ 1:0] \;\verb!\vert!\; y_2[n$-$ 1:0]\}$

(c) $ \{x_1[m$-$ 1:0],y_1[n$-$ 1:0]\} \;\verb!^!\; \{x_2[m$-$ 1:0],y_2[n$-$ 1:0]\}$
            = $ \{x_1[m$-$ 1:0] \;\verb!^!\; x_2[m$-$ 1:0],y_1[n$-$ 1:0] \;\verb!^!\; y_2[n$-$ 1:0]\}$

PROOF: We present the proof for (a); (b) and (c) are similar.

Let $ C = \{x_1[m$-$ 1:0],y_1[n$-$ 1:0]\} \;\verb!&!\; \{x_2[m$-$ 1:0],y_2[n$-$ 1:0]\}$. By Lemmas 3.1.4 and 2.4.13,

$\displaystyle C \bmod 2^n$ $\displaystyle =$ $\displaystyle \{x_1[m$-$\displaystyle 1:0],y_1[n$-$\displaystyle 1:0]\}[n$-$\displaystyle 1:0] \;\verb!&!\; \{x_2[m$-$\displaystyle 1:0],y_2[n$-$\displaystyle 1:0]\}[n$-$\displaystyle 1:0]$  
  $\displaystyle =$ $\displaystyle y_1[n$-$\displaystyle 1:0] \;\verb!&!\; y_2[n$-$\displaystyle 1:0].$  

By Lemma 3.1.5,

$\displaystyle \lfloor C/2^n \rfloor = \lfloor \{x_1[m$-$\displaystyle 1:0],y_1[n$-$\displaystyle 1:0]\}/2^n\rfloor \;\verb!&!\;
\lfloor \{x_2[m$-$\displaystyle 1:0],y_2[n$-$\displaystyle 1:0]\}/2^n\rfloor,$

where, by Definition 2.4.1 and the properties of the floor,
$\displaystyle \lfloor \{x_i[m$-$\displaystyle 1:0],y_i[n$-$\displaystyle 1:0]\}/2^n\rfloor$ $\displaystyle =$ $\displaystyle \lfloor (2^nx_i[m$-$\displaystyle 1:0]+y_i[n$-$\displaystyle 1:0])/2^n\rfloor$  
  $\displaystyle =$ $\displaystyle x_i[m$-$\displaystyle 1:0]+\lfloor y_i[n$-$\displaystyle 1:0]/2^n\rfloor$  
  $\displaystyle =$ $\displaystyle x_i[m$-$\displaystyle 1:0].$  

Thus,

$\displaystyle \lfloor C/2^n \rfloor = x_1[m$-$\displaystyle 1:0] \;\verb!&!\; x_2[m$-$\displaystyle 1:0].$

Finally, by Definitions 1.2.1 and 2.4.1,
$\displaystyle C$ $\displaystyle =$ $\displaystyle \lfloor C/2^n \rfloor 2^n + (C \bmod2^n))$  
  $\displaystyle =$ $\displaystyle 2^n(x_1[m$-$\displaystyle 1:0] \;\verb!&!\; x_2[m$-$\displaystyle 1:0]) + y_1[m$-$\displaystyle 1:0] \;\verb!&!\; y_2[m$-$\displaystyle 1:0])$  
  $\displaystyle =$ $\displaystyle \{x_1[m$-$\displaystyle 1:0] \;\verb!&!\; x_2[m$-$\displaystyle 1:0],y_1[n$-$\displaystyle 1:0] \;\verb!&!\; y_2[n$-$\displaystyle 1:0]\}.$  

  (logand-shift,logior-shift,logxor-shift) For all $ x \in \mathbb{Z}$, $ y
\in \mathbb{Z}$, and $ n \in \mathbb{N}$,

(a) $ 2^n(x \;\verb!&!\; y) = 2^nx \;\verb!&!\; 2^ny$;
(b) $ 2^n(x \;\verb!\vert!\; y) = 2^nx \;\verb!\vert!\; 2^ny$;
(c) $ 2^n(x \;\verb!^!\; y) = 2^nx \;\verb!^!\; 2^ny$.

PROOF: We present the proof for (a); (b) and (c) are similar.

We may assume that $ n > 0$, $ x \neq 0$, $ y \neq 0$, and $ x \neq y$. By induction and Definition 3.1.1,

$\displaystyle 2^n(x \;\verb!&!\; y)$ $\displaystyle =$ $\displaystyle 2\left(2^{n-1}(x \;\verb!&!\; y)\right)$  
  $\displaystyle =$ $\displaystyle 2\left(2^{n-1}x \;\verb!&!\; 2^{n-1}y\right)$  
  $\displaystyle =$ $\displaystyle 2\left(\lfloor 2^nx/2 \rfloor \;\verb!&!\; \lfloor 2^nx/2 \rfloor \right) + (2^nx \bmod 2) \;\verb!&!\; (2^ny \bmod 2)$  
  $\displaystyle =$ $\displaystyle 2^nx \;\verb!&!\; 2^ny. $  

  (logand-expt,logior-expt,logxor-expt) For all $ x \in \mathbb{Z}$, $ y
\in \mathbb{Z}$, and $ n \in \mathbb{N}$,

(a) $ 2^nx \;\verb!&!\; y = 2^n(x \;\verb!&!\; \lfloor y/2^n)$;
(b) $ 2^nx \;\verb!\vert!\; y = 2^n(x \;\verb!\vert!\; \lfloor y/2^n) + y \bmod 2^n$;
(c) $ 2^nx \;\verb!^!\; y = 2^n(x \;\verb!^!\; \lfloor y/2^n) + y \bmod 2^n$.

PROOF:

(a) The claim is trivial if $ x = 0$, $ y = 0$, or $ y = 2^nx$; otherwise, by Definition 3.1.1, induction, and Lemma 1.1.5,

$\displaystyle 2^nx \;\verb!&!\; y$ $\displaystyle =$ $\displaystyle 2\left(\lfloor 2^nx/2 \rfloor \;\verb!&!\; \lfloor y/2 \rfloor\right) + (2^nx \bmod 2) \;\verb!&!\; (y \bmod 2)$  
  $\displaystyle =$ $\displaystyle 2(2^{n-1}x \;\verb!&!\; \lfloor y/2 \rfloor) + 0$  
  $\displaystyle =$ $\displaystyle 2\left(2^{n-1}(x \;\verb!&!\; \left\lfloor \lfloor y/2 \rfloor/2^{n-1}\right\rfloor)\right)$  
  $\displaystyle =$ $\displaystyle 2^n(x \;\verb!&!\; \lfloor y/2^n\rfloor).$  

(b) Similarly,

$\displaystyle 2^nx \;\verb!\vert!\; y$ $\displaystyle =$ $\displaystyle 2\left(\lfloor 2^nx/2 \rfloor \;\verb!\vert!\; \lfloor y/2 \rfloor\right) + (2^nx \bmod 2) \;\verb!\vert!\; (y \bmod 2)$  
  $\displaystyle =$ $\displaystyle 2(2^{n-1}x \;\verb!\vert!\; \lfloor y/2 \rfloor) + y \bmod 2$  
  $\displaystyle =$ $\displaystyle 2\left(2^{n-1}\left(x \;\verb!\vert!\; \left\lfloor \lfloor y/2 \...
...n-1}\right\rfloor\right) + \lfloor y/2 \rfloor \bmod 2^{n-1}\right) + y \bmod 2$  
  $\displaystyle =$ $\displaystyle 2^n(x \;\verb!\vert!\; \lfloor y/2^n \rfloor) + 2(\lfloor y/2 \rfloor \bmod 2^{n-1}) + y \bmod 2,$  

where, by Lemmas 2.2.4 and 2.2.16,

$\displaystyle 2(\lfloor y/2 \rfloor \bmod 2^{n-1}) + y \bmod 2 = 2\lfloor y/2 \rfloor[n-2:0] + y[0] = 2y[n-1:1] + y[0] = y[n-1:0] = y \bmod 2^n.
$

(c) is similar to (b). 

  (logior-expt-cor) Let $ x \in \mathbb{Z}$ and let $ y$ be an $ n$-bit vector, where $ n \in \mathbb{N}$. Then

$\displaystyle 2^nx \;\verb!\vert!\; y = 2^nx + y.
$

PROOF: By Lemmas 3.1.8 and 1.2.6 and Definition 3.1.2,

$\displaystyle 2^nx \;\verb!\vert!\; y = 2^n(x \;\verb!\vert!\; \lfloor y/2^n) + y \bmod 2^n = 2^n(x \;\verb!\vert!\; 0) + y = 2^nx + y. $

  (logior-2**n) For all $ x \in \mathbb{Z}$ and $ n \in \mathbb{N}$, $ 2^n \;\verb!\vert!\; x = \left\{\begin{array}{ll}
x & \mbox{if $x[n] = 1$}\\
x + 2^n & \mbox{if $x[n] = 0$.}\end{array}\right.$

PROOF: By Definition 2.0.1 and Lemmas 3.1.4, 3.1.6, and 2.3.17,

$\displaystyle (2^n \;\verb!\vert!\; x) \bmod {2^{n+1}}$ $\displaystyle =$ $\displaystyle (2^n \;\verb!\vert!\; x)[n:0]$  
  $\displaystyle =$ $\displaystyle (2^n)[n:0] \;\verb!\vert!\; x[n:0]$  
  $\displaystyle =$ $\displaystyle \{1'1, 0'(n-1)\} \;\verb!\vert!\; \{x[n], x[n-1:0]\}$  
  $\displaystyle =$ $\displaystyle \{1'1, x[n-1:0]\}$  
  $\displaystyle =$ $\displaystyle \left\{\begin{array}{ll}
x[n:0] & \mbox{if $x[n] = 1$}\\
x[n:0] + 2^n & \mbox{if $x[n] = 0$}\end{array}\right.$  
  $\displaystyle =$ $\displaystyle \left\{\begin{array}{ll}
x \bmod {2^{n+1}} & \mbox{if $x[n] = 1$}\\
x \bmod {2^{n+1}} + 2^n & \mbox{if $x[n] = 0$.}\end{array}\right.$  

By Lemma 3.1.5,

$\displaystyle \lfloor(2^n \;\verb!\vert!\; x)/2^{n+1} \rfloor = 0 \;\verb!\vert!\; \lfloor x/2^{n+1} \rfloor = \lfloor x/2^{n+1} \rfloor.
$

The lemma follows from Definition 1.2.1


The logical “and” operator may be used to extract a bit slice:

  (logand-bits) Let $ x \in \mathbb{Z}$, $ n \in \mathbb{N}$, and $ k \in \mathbb{N}$. If $ k<n$, then

$\displaystyle x \;\verb!&!\; (2^n - 2^k) = 2^kx[n-1:k].
$

PROOF: The proof is by induction on $ n$. If $ n=1$, then $ k=0$ and

$\displaystyle x \;\verb!&!\; (2^n - 2^k) = x \;\verb!&!\; 1 = 2(\lfloor x/2 \rfloor \;\verb!&!\; 0) + (x \bmod 2) \;\verb!&!\; 1 = 0 + x[0] = x[n-1:k].
$

If $ n>1$ and $ k=0$, then by induction and Lemmas 2.2.16 and 2.3.17,
$\displaystyle x \;\verb!&!\; (2^n - 2^k)$ $\displaystyle =$ $\displaystyle x \;\verb!&!\; (2^n - 1)$  
  $\displaystyle =$ $\displaystyle 2(\lfloor x/2 \rfloor \;\verb!&!\; \lfloor (2^n - 1)/2 \rfloor) + (x \bmod 2) \;\verb!&!\; ((2^n-1) \bmod 2)$  
  $\displaystyle =$ $\displaystyle 2(\lfloor x/2 \rfloor \;\verb!&!\; (2^{n-1} - 1)) + (x \bmod 2) \;\verb!&!\; 1$  
  $\displaystyle =$ $\displaystyle 2\lfloor x/2 \rfloor[n-2:0] + x[0]$  
  $\displaystyle =$ $\displaystyle 2x[n-1:1] + x[0]$  
  $\displaystyle =$ $\displaystyle x[n-1:0].$  

In the remaining case, $ n>k>1$ and
$\displaystyle x \;\verb!&!\; (2^n - 2^k)$ $\displaystyle =$ $\displaystyle 2(\lfloor x/2 \rfloor \;\verb!&!\; \lfloor (2^n - 1)/2 \rfloor) + (x \bmod 2) \;\verb!&!\; ((2^n - 2^k) \bmod 2)$  
  $\displaystyle =$ $\displaystyle 2(\lfloor x/2 \rfloor \;\verb!&!\; (2^{n-1} - 2^{k-1})) + (x \bmod 2) \;\verb!&!\; 0$  
  $\displaystyle =$ $\displaystyle 2\lfloor x/2 \rfloor[n-2:k-1]$  
  $\displaystyle =$ $\displaystyle x[n-1:k]. $  

  (logand-bit) For all $ x \in \mathbb{Z}$ and $ n \in \mathbb{N}$, $ x \;\verb!&!\; 2^n = 2^nx[n]$.

PROOF: By Lemma 3.1.11,

$\displaystyle x \;\verb!&!\; 2^n = x \;\verb!&!\; (2^{n+1} - 2^n) = x[n:n] = x[n]. $

All three binary logical operators commute with the bit slice operator:

  (bits-logand,bits-logior,bits-logxor) For all $ x \in \mathbb{Z}$, $ y
\in \mathbb{Z}$, $ i \in \mathbb{N}$, and $ j \in \mathbb{N}$,
(a) $ (x \;\verb!&!\; y)[i:j] = x[i:j] \;\verb!&!\; y[i:j]$;
(b) $ (x \;\verb!\vert!\; y)[i:j] = x[i:j] \;\verb!\vert!\; y[i:j]$;
(c) $ (x \;\verb!^!\; y)[i:j] = x[i:j] \;\verb!^!\; y[i:j]$.

PROOF: We present the proof for (a); (b) and (c) are similar.

We may assume that $ n > 0$, $ x \neq 0$, $ y \neq 0$, and $ x \neq y$. By Definition 2.0.1 and Lemmas 3.1.4 and 3.1.5,

$\displaystyle (x \;\verb!&!\; y)[i:j]$ $\displaystyle =$ $\displaystyle \left\lfloor ((x \;\verb!&!\; y) \bmod 2^{i+1})/2^{j} \right\rfloor$  
  $\displaystyle =$ $\displaystyle \left\lfloor ((x \bmod 2^{i+1}) \;\verb!&!\; (y \bmod 2^{i+1}))/2^{j}\right\rfloor$  
  $\displaystyle =$ $\displaystyle \lfloor(x \bmod 2^{i+1})/{2^{j}} \rfloor \;\verb!&!\; \lfloor(y \bmod 2^{i+1})/{2^{j}} \rfloor$  
  $\displaystyle =$ $\displaystyle x[i:j] \;\verb!&!\; y[i:j]. $  

Corollary 3.1.14   (bitn-logand,bitn-logior,bitn-logxor) For all $ x \in \mathbb{Z}$, $ y
\in \mathbb{Z}$, and $ k \in \mathbb{N}$,
(a) $ (x \;\verb!&!\; y)[n] = x[n] \;\verb!&!\; y[n]$;
(b) $ (x \;\verb!\vert!\; y)[n] = x[n] \;\verb!\vert!\; y[n]$;
(c) $ (x \;\verb!^!\; y)[n] = x[n] \;\verb!^!\; y[n]$.

Notation: If $ \phi$ and $ \psi$ are expressions of sizes $ m$ and $ n$, respectively, then we define the size of each of the expressions $ \phi \;\verb!&!\; \psi$, $ \phi \;\verb!\vert!\; \psi$, and $ \phi \;\verb!^!\; \psi$ to be $ max(m, n)$. As a consequence of Lemma 3.1.2, it remains true that if $ \phi$ is any expression of size $ n$, then the value of $ \phi$ is a bit vector of width $ n$.

Thus, for example, by Lemma 3.1.13,

$\displaystyle \{3\verb!'b!101, x[n-1:0] \;\verb!&!\; y[n-1:0]\} = \{3\verb!'b!101, (x \;\verb!&!\; y)[n-1:0]\} = cat(5, 3, x \;\verb!&!\; y, n).
$

David Russinoff 2017-08-01