ch08.tex

\chapter{Multiplexers and Demultiplexers}
\label{ch:mux-dmx}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "book"
%%% End:

\section{Multiplexer}
\label{sec:mux}

Suppose you want to take two lists and shuffle them into one.
You're looking for a \index{perfect shuffle}\index{shuffle, perfect}perfect shuffle,
an element from one list,
then one from the other list, back to the first list, and so on.
This is sometimes called multiplexing.
The term comes from signal transmission.
When there are more signals than channels to send them on,
one way to share a channel between two signals is to
send a small part of one signal, then part of the other,
then part of the first one again, and so on.
There could be any number of signals sharing the channel,
and the same kind of round-robin approach would work.
We call the shuffle operator
\seeonlyindex{mux, mux2 (multiplexer)}{operator}\index{operator, by name!mux (multiplexer)}\textsf{mux}.
It follows the pattern of the following equation:

\hspace{1cm} \textsf{(mux [$x_1$ $x_2$ $x_3$ $\dots$] [$y_1$ $y_2$ $y_3$ $\dots$]) =
     [$x_1$ $y_1$ $x_2$ $y_2$ $x_3$ $y_3$ $\dots$]} \hfill \{\emph{mux}\}

As usual, we want to define the \textsf{mux} operator in terms of
a collection of comprehensive, consistent, and computational equations
that it would have to satisfy if it worked properly
(figure~\ref{fig:inductive-def-keys}, page \pageref{fig:inductive-def-keys}).
If both lists are nonempty,
then the first element of the multiplexed list is the first element of the first list,
and the second element of the multiplexed list is the first element of the other list.
So, the following formula would
get the first two elements into the right places in the multiplexed list:

\hspace{1cm} \textsf{(mux (cons $x$ $xs$) (cons $y$ $ys$))} $=$
(cons $x$ (cons $y$ ~~~$\dots$} \emph{rest of formula} $\dots$\textsf{))}

Fortunately, there is no great mystery concerning the missing part of the formula.
Multiplexing what's left of the two input lists will get all the elements
in the right place for a perfect shuffle.
That observation leads to an inductive equation that the \textsf{mux} operator
would satisfy if it worked properly.

\hspace{1cm} \textsf{(mux (cons $x$ $xs$) (cons $y$ $ys$)) $=$ (cons $x$ (cons $y$ (mux $xs$ $ys$)))}
\hfill \{\emph{mux11}\}

The \{\emph{mux11}\} equation covers the case when both lists are nonempty.
Since it's an inductive equation, we need to be careful to make sure
that operands of \textsf{mux} on the right-hand side of the equation
are closer to those in a noninductive equation than they are
to the operands on the left-hand side.
If not, the equation will fail to be computational and
will not define the \textsf{mux} operator.
We observe that the operands on the right
are one element shorter than the operands on the left.
Therefore, the equation \{\emph{mux11}\} can be used
as a defining axiom. It applies whenever both lists are nonempty.

If both lists are empty, there is nothing to multiplex,
so \textsf{mux} would deliver the empty list in that case, but
what should it deliver if one list is empty but the other isn't?
There is more than one reasonable choice, and each leads to
a different operator. One choice is to incorporate the elements
in the nonempty list, just as they are, into the
multiplexed list that \textsf{mux}  delivers.
That would make \textsf{mux} satisfy the following equations:

\index{operator, by name!mux (multiplexer)}\index{axiom, by name!\{mux0x\}, \{mux0y\}, \{mux1y\}, \{mux11\}}\index{equation, by name!\{mux0x\}, \{mux0y\}, \{mux1y\}, \{mux11\}}
\begin{center}
\begin{tabular}{ll}
\multicolumn{2}{c}{Axioms \textsf{mux} \label{axioms:mux}}\\
\hline
\textsf{(mux nil $ys$) $=$ $ys$}  & \{\emph{mux0x}\}     \\
\textsf{(mux $xs$ nil) $=$ $xs$}  & \{\emph{mux0y}\}     \\
\textsf{(mux (cons $x$ $xs$) (cons $y$ $ys$)) $=$ (cons $x$ (cons $y$ (mux $xs$ $ys$)))} & \{\emph{mux11}\} \\
\end{tabular}
\end{center}

\label{def:mux}The three equations, \{\emph{mux0x}\}, \{\emph{mux0y}\}, and \{\emph{mux11}\},
are comprehensive (either both operands are nonempty
or at least one of them is empty) and computational (as discussed).
They are consistent because the only overlapping case
occurs when both lists are empty, and in that case,
the overlapping equations
(\{\emph{mux0x}\} and \{\emph{mux0y}\}) specify the same result
(namely, the empty list).
We can, therefore, take the equations as axioms
defining the \textsf{mux} operator.
Converting the axioms to ACL2 notation leads to the following
definition:

\label{mux-defun}\index{operator, by name!mux (multiplexer)}\index{equation, by name!\{mux0x\}, \{mux0y\}, \{mux1y\}, \{mux11\}}\index{axiom, by name!\{mux0x\}, \{mux0y\}, \{mux1y\}, \{mux11\}}
\begin{code}
\begin{verbatim}
(defun mux (xs ys)
  (if (not (consp xs))
      ys                                             ; {mux0x}
      (if (not (consp ys))
          xs                                         ; {mux0y}
          (cons (first xs)
                (cons (first ys)
                      (mux (rest xs) (rest ys))))))) ; {mux11}
\end{verbatim}
\end{code}

As always, the axioms that define an operator
determine not only the properties they specify directly
but all other properties of the operator, too.
What properties would we expect the \textsf{mux} operator to have?
Surely the number of elements in the multiplexed list
would be the sum of the lengths of its operands.
The following theorem states this property formally,
and ACL2 succeeds in finding a proof:

\label{mux-length-thm}\index{theorem, by name!\{mux-length\}}
\begin{code}
\begin{verbatim}
(defthm mux-length-thm
  (= (len (mux xs ys))
     (+ (len xs) (len ys))))
\end{verbatim}
\end{code}

For practice, let's construct a paper-and-pencil proof of the theorem. %'
Our strategy will be an induction on the length of the first operand.
We are trying to prove that the following equation holds for all natural numbers, $n$:\\
~\\
\index{theorem, by name!\{mux-length\}}Theorem \{mux-length\}: $\forall n.$L($n$)\\
where L($n$) $\equiv$ $($\textsf{(len(mux [$x_1$ $x_2$ $\dots$ $x_n$] $ys$)) $=$ $n +$ (len $ys$)}$)$\\
\emph{proof by induction}\\
\emph{Base case} (first operand empty): L($0$) $\equiv$ $($\textsf{(len(mux nil $ys$)) = $0 +$ (len $ys$)}$)$
~\\[-1.0em]
\begin{center}
\begin{tabular}{lll}
     & \textsf{(len(mux nil $ys$)})    &                   \\
 $=$ & \textsf{(len $ys$)}             & \{\emph{mux0x}\}  \\
 $=$ & \textsf{$0 +$ (len $ys$)}       & \{\emph{algebra}\}\\
\end{tabular}
\end{center}
\label{mux-length-thm-induc-case}\emph{Inductive case} (first operand has $n+1$ elements):\\
\hspace*{1cm}L($n+1$) $\equiv$ $($\textsf{(len(mux [$x_1$ $x_2$ $\dots$ $x_{n+1}$] $ys$)) $=$ $(n+1)$ + (len $ys$)}$)$

We split the inductive case, $L(n+1)$, into two parts.
The second operand of \textsf{mux} is either \textsf{nil} or it's not. %'
We derive the conclusion from both possibilities,
and that completes the proof because we can infer
that the conclusion holds in all
circumstances.\footnote{Case-by-case proofs of this kind
would cite the \{$\vee$ elimination\} inference rule
(page \pageref{fig-02-deduction-rules}) if they
took the form of natural deduction.
The proof here is rigorous but not formal.
ACL2 carries out a formal proof.}

\begin{aside}{aside:mux-val-thm}{Formal Version of Mux-Val Theorem}
In exercise \ref{ex:mul-val-thm} (page \pageref{ex:mul-val-thm})
the mux-val theorem
and the axioms of the \textsf{occurs-in} predicate
have been stated in the form we use for paper-and-pencil proofs.
These proofs are rigorous but not formal
in the sense of the mechanized proofs of ACL2.
Below is an ACL2 formalization of these ideas,
which the ACL2 system succeeds in admitting.
\label{acl2:iff}
The
\index{Boolean!equivalence ($\leftrightarrow$, iff)}\index{operator, logic!Boolean equivalence ($\leftrightarrow$, iff)}\index{equivalence!Boolean ($\leftrightarrow$, iff)}\index{iff (\emph{see also} operator)}\textsf{iff}
operator is Boolean equivalence
(box~\ref{aside:boolean-equivlance}, page \pageref{aside:boolean-equivlance}).

\label{defun:occurs-in}
\begin{code}
\begin{verbatim}
(defun occurs-in (x xs)
  (if (consp xs)
      (or (equal x (first xs))
          (occurs-in x (rest xs)))
      nil))
(defthm mux-val-thm
  (iff (occurs-in v (mux xs ys))
       (or (occurs-in v xs)
           (occurs-in v ys))))
\end{verbatim}
\end{code}\index{theorem, by name!\{mux-val\}}\index{predicate, by name!occurs-in (list)}\index{operator, by name!occurs-in (\emph{see} predicate)}
%\caption{Formal Version of Mux-Val Theorem}
%\label{aside:mux-val-thm}\label{defthm:mux-val}
\end{aside}

The proof of the inductive case when $ys$ is \textsf{nil}
is like the proof when $xs$ is \textsf{nil},
except that it cites \{\emph{mux0y}\} instead of \{\emph{mux0x}\}.
Figure~\ref{fig:prf-mux-len-induc} (page \pageref{fig:prf-mux-len-induc})
presents a proof  of the inductive case when both operands are nonempty.
That is, when the second operand has the form \textsf{(cons $y$ $ys$)}
and the first operand has $n+1$ elements.
This completes the proof by mathematical induction of
theorem \{mux-length\}: $\forall n.$L($n$).

\begin{figure}
\begin{center}
L($n+1$) $\equiv$ \textsf{(len(mux [$x_1$ $x_2$ $\dots$ $x_{n+1}$] (cons $y$ $ys$))) $=$ $(n+1)$ $+$ (len (cons $y$ $ys$))}
\begin{tabular}{lll}
\hline\\[-1.0em]
    & \textsf{(len(mux [$x_1$ $x_2$ $\dots$ $x_{n+1}$] (cons $y$ $ys$)))}        &   \\
$=$ & \textsf{(len(mux (cons $x_1$ [$x_2$ $\dots$ $x_{n+1}$] (cons $y$ $ys$))))} & \{\emph{cons}\} \emph{(page \pageref{first-rest-cons})} \\
$=$ & \textsf{(len(cons $x_1$ (cons $y$ (mux [$x_2$ $\dots$ $x_{n+1}$] $ys$))))} & \{\emph{mux11}\} \emph{(page \pageref{axioms:mux})}\\
$=$ & $1 + (1 +$ \textsf{(len(mux [$x_2$ $\dots$ $x_{n+1}$] $ys$))})             & \{\emph{len1}\} \emph{twice (page \pageref{len-equations})}\\
$=$ & $1 + (1 + (n$ $+$ \textsf{(len $ys$)}$))$                                  & \{\emph{L(n)}\} \emph{induction hypothesis} \\
$=$ & $(n + 1) + (1$ $+$ \textsf{(len $ys$)}$)$                                  & \{\emph{algebra}\} \\
$=$ & $(n + 1)$ $+$ \textsf{(len(cons $y$ $ys$))}                                & \{\emph{len1}\} \\
\end{tabular}
\end{center}\index{theorem, by name!\{mux-length\}}
\caption{Theorem \{mux-length\}: inductive case when both operands are nonempty.}
\label{fig:prf-mux-len-induc}
\end{figure}

The next section discusses an operator that goes in the other direction.
It ``demultiplexes'' a list into two lists, reversing the perfect shuffle.
We will prove that \textsf{dmx} undoes the effect of \textsf{mux} and vice versa.
That is, the two operators invert each other.

\begin{aside}{aside:mux-2eq}{Multiplexer: A Two-Equation Definition}
The multiplexer operator can be defined with two equations instead of three
by swapping the operands in the inductive equation.
When the first operand is nonempty, \textsf{mux} satisfies the following equation.\\
\hspace*{1cm}\textsf{(mux (cons $x$ $xs$) $ys$) = (cons $x$ (mux $ys$ $xs$))} ~~ \{mux1y\}

The inductive invocation, \textsf{(mux $ys$ $xs$)},
on the right-hand side of \{mux1y\}
delivers a list that starts with the first element of $ys$,
then alternates between $xs$ and $ys$.
Perfect shuffle.
It's a two-equation definition. %'

\label{mux-2eq-defun}\index{operator, by name!mux (multiplexer)}\index{operator, by name!mux2 (multiplexer)}\index{axiom, by name!\{mux2-0x\}, \{mux2-1x\}}\index{equation, by name!\{mux2-0x\}, \{mux2-1x\}}\index{defun!induction hint}\index{definition!defun hint}\index{directive!induction hint}
\begin{code}
\begin{verbatim}
(defun mux2 (xs ys) ; declare induction scheme
   (declare (xargs :measure (+ (len xs) (len ys))))
   (if (consp xs)
       (cons (first xs) (mux2 ys (rest xs))) ; {mux2-1x}
       ys))                                  ; {mux2-0x}
\end{verbatim}
\end{code}

The equations define an operator \textsf{mux2} that produces
the same results as \textsf{mux}.
However, the new definition makes reasoning more complicated
because the operands switch roles in the inductive invocation.
A \textsf{declare} directive in the definition
helps ACL2 cope with this wrinkle in its
proof that \textsf{mux2} terminates,
which the mechanized logic must complete before
admitting the operator to the logic.
%\caption{Multiplexer: a Two Equation Definition}
%\label{aside:mux-2eq}
\end{aside}

\begin{exercises}
\exer {%
Our proof of the inductive case, L($n+1$), of the mux-length theorem
(page \pageref{mux-length-thm-induc-case})
glossed over the part when the second operand is empty.
Complete that part of the proof. That is, prove the following equation:\\
\hspace*{1cm} \textsf{(len(mux [$x_1$ $x_2$ $\dots$ $x_{n+1}$] nil)) $=$ $(n+1)$ $+$ (len nil)}}

\exer {\label{ex:mul-val-thm}%
Prove that the \textsf{mux} operator neither adds nor loses values from its operands.
That is, a value that occurs in either $xs$ or $ys$ also occurs in \textsf{(mux $xs$ $ys$)}
and, vice versa, a value that occurs in \textsf{(mux $xs$ $ys$)} also occurs in either $xs$ or $ys$.\\
\index{theorem, by name!\{mux-val\}}\label{thm:mux-val}Theorem \{mux-val\}:
$\forall v.(($\textsf{(occurs-in $v$ $xs$)} $\vee$ \textsf{(occurs-in $v$ $ys$)}$) \leftrightarrow$ \textsf{(occurs-in $v$ (mux $xs$ $ys$))}$)$ \\
\emph{Note}: The ``$\leftrightarrow$'' operator
is Boolean equivalence (box~\ref{aside:boolean-equivlance}, page \pageref{aside:boolean-equivlance}).\\
\emph{Note}: The occurs-in predicate is defined as
follows:\index{predicate, by name!occurs-in (list)}\index{operator, by name!occurs-in (\emph{see} predicate)}\seeonlyindex{occurs-in list}{predicate}\\
\label{def:occurs-in}
\hspace*{5mm}\textsf{(occurs-in $v$ $xs$)} $=$ \textsf{(consp $xs$)} $\wedge$ $((v$ $=$ \textsf{(first $xs$)}$)$ $\vee$ \textsf{(occurs-in $v$ (rest $xs$))}$)$ ~ \{\emph{occurs-in}\}\\
\emph{Hint:} For the inductive case of your proof
(that is, the case when $xs$ is nonempty),
split the proof into two parts,
as in the proof of the mux-length theorem (page \pageref{mux-length-thm}).
In one part, the value $v$ will be equal to
the first element of $xs$:
$v$ $=$ \textsf{(first $xs$)}.
In the other part, $v$ will occur in \textsf{(rest $xs$)}.
That is, \textsf{(occurs-in $v$ (rest $xs$))} will be true.
Prove each part separately.
Since the two parts cover all the possibilities,
you can infer that the inductive case is true.}

\exer {\label{mux-val-len-not-enough}%
Give an example of lists \textsf{[$x$]}, \textsf{[$y$]}, and \textsf{[$u$ $w$]} for which
\textsf{[$u$ $w$]} $\neq$ \textsf{(mux [$x$] [$y$])} but the following formula is true:\\
\hspace*{1cm}$\forall v.(($\textsf{(occurs-in $v$ [$x$])} $\vee$ \textsf{(occurs-in $v$ [$y$])}$)
\leftrightarrow$ \textsf{(occurs-in $v$ [$u$ $w$])}$)$}

\exer {\label{mux2-eq-mux}%
Do a paper-and-pencil proof that
\textsf{(mux2 $xs$ $ys$)} is the same as \textsf{(mux $xs$ $ys$)}.\\
\emph{Note}: \textsf{mux2} is defined in
box~\ref{aside:mux-2eq}, page \pageref{aside:mux-2eq},
and \textsf{mux} is defined on page \pageref{mux-defun}.}

\exer {Formalize the theorem of exercise~\ref{mux2-eq-mux} in ACL2.}

\end{exercises}

\section{Demultiplexer}
\label{sec:dmx}

A demultiplexer transforms a list of signals that alternate between
$x$-values and $y$-values into two lists,
with the $x$-values in one list and $y$-values in the other.\\
\hspace*{1cm} \textsf{(dmx [$x_1$ $y_1$ $x_2$ $y_2$ $x_3$ $y_3$ $\dots$]) $=$
[[$x_1$ $x_2$ $x_3$ $\dots$] [$y_1$ $y_2$ $y_3$ $\dots$]]}
\hfill \{\emph{dmx}\}

The following equations form an inductive definition of \textsf{dmx}.
The inductive equation covers the case when
the operand has at least two elements
(that is, it starts with an $x$ and then a $y$),
and the noninductive equations cover the cases
when the operand has just one element or none.

\index{axiom, by name!\{dmx0\}, \{dmx1\}, \{dmx2\}}\index{equation, by name!\{dmx0\}, \{dmx1\}, \{dmx2\}}
\begin{center}
\begin{tabular}{ll}
\multicolumn{2}{c}{Axioms \textsf{dmx}}\\
\hline
\textsf{(dmx [$x_1$ $y_1$ $x_2$ $y_2$ $\dots$ $x_{n+1}$ $\dots$])} $=$ \textsf{[(cons $x_1$ $xs$) (cons $y_1$ $ys$)] }&\{\emph{dmx2}\} \\
~~~~~~where \textsf{[$xs$ $ys$]} $=$ \textsf{(dmx [$x_2$ $y_2$ $\dots$ $x_{n+1}$ $\dots$])}       &\\
\textsf{(dmx [$x_1$]) $=$  [[$x_1$] nil]}                                                         &\{\emph{dmx1}\} \\
\textsf{(dmx nil) $=$ [nil nil] }                                                                 &\{\emph{dmx0}\} \\
\end{tabular}
\end{center}
\label{dmx-defun}\index{axiom, by name!\{dmx0\}, \{dmx1\}, \{dmx2\}}\index{equation, by name!\{dmx0\}, \{dmx1\}, \{dmx2\}}\index{operator, by name!dmx (demultiplexer)}\seeonlyindex{dmx, dmx2 (demultiplexer)}{operator}
\begin{code}
\begin{verbatim}
(defun dmx (xys)
  (if (consp (rest xys)) ; 2 or more elements?
      (let* ((x (first xys))
             (y (second xys))
             (xsys (dmx (rest (rest xys))))
             (xs (first xsys))
             (ys (second xsys)))
        (list (cons x xs) (cons y ys)))      ; {dmx2}
      (list xys nil)))  ; 1 element or none  ; {dmx1}
\end{verbatim}
\end{code}

The informal axioms for \textsf{dmx} provide a basis for a formal definition.
The formal version takes advantage of the fact that if the operand
has less than two elements, then it is the first component of the result
and the second component is the empty list.
Like the multiplexer,
the demultiplexer preserves the total length
and preserves the values in its operand.
ACL2 succeeds in verifying these facts without assistance,
and the paper-and-pencil proofs are similar to the corresponding
theorems for the multiplexer.

The two operators also satisfy some \index{property!round-trip}\index{round-trip property}round-trip properties
that bolster our confidence that they do what we expect them to do.
Demultiplexing a list of $x$-$y$ values into the list of
$x$-values and the list of $y$-values and then multiplexing
those two lists reproduces the original list of $x$-$y$ values.
It works the other way around too if the operands of
the \textsf{mux} operator are lists of the same length.\footnote{Both
of the round-trip properties require the operands to be
true lists because the multiplexer can lose information
if its operands aren't true lists.
(The term ``true list'' is defined on page \pageref{true-list-def}.)}

\label{thm:mux-inverts-dmx}\label{thm:dmx-inverts-mux}\index{theorem, by name!\{mux-inverts-dmx\}}\index{theorem, by name!\{dmx-inverts-mux\}}
\begin{code}
\begin{verbatim}
(defthm mux-inverts-dmx-thm
  (implies (true-listp xys)
           (equal (mux (first  (dmx xys))
                       (second (dmx xys)))
                  xys)))
(defthm dmx-inverts-mux-thm
  (implies (and (true-listp xs) (true-listp ys)
                (= (len xs) (len ys)))
           (equal (dmx (mux xs ys))
                  (list xs ys))))
\end{verbatim}
\end{code}

The \textsf{dmx} operator delivers every other element of the operand in
one component of a list and the remaining elements in the other component.
That means that each component of the result is half as long as the operand.
If the operand has an odd number of elements, the extra one goes into the first component.
These length properties can be specified in terms of the \textsf{floor} and \textsf{ceiling}
operators (box~\ref{floor-ceiling-ops-brackets}, page \pageref{floor-ceiling-ops-brackets}).
The length of the first component is the length of the operand divided by two
and rounded up to the next integer if the operand has an odd number of elements.
The second component is also half the length of the operand but rounded down if necessary.
The mechanized logic of ACL2 succeeds in proving these theorems,
but it needs the help of some theorems about arithmetic.

\label{thm:dmx-length-first-second}\seeonlyindex{mux theorems}{theorem}\seeonlyindex{dmx theorems}{theorem}\index{theorem, by name!\{dmx-len-first\}, \{dmx-len-second\}}\index{book!arithmetic-3/top}\index{directory (:dir)!:system}\index{directive!include-book}\index{system, :dir}\index{book!directory (:dir)}
\begin{code}
\begin{verbatim}
(include-book "arithmetic-3/top" :dir :system)
(defthm dmx-len-first
   (= (len (first (dmx xs)))
      (ceiling (len xs) 2)))
(defthm dmx-len-second
   (= (len (second (dmx xs)))
      (floor (len xs) 2)))
\end{verbatim}
\end{code}

\begin{aside}{aside:dmx-defun-trick}{Cleverness Sometimes Complicates Reasoning}
An alternate definition of a demultiplexer
observes that if the operand alternates between $x$ and $y$ values,
starting with an $x$,
then the same list without its first element also alternates
but starting with a $y$. The definition is shorter,
but it complicates reasoning.

\begin{center}
\begin{tabular}{ll}
\multicolumn{2}{c}{Axioms \textsf{dmx2} (maybe too clever by half)}\\
\hline
\textsf{(dmx2 (cons $x$ $yxs$)) $=$ [(cons $x$ $xs$) $ys$]}& \{\emph{dmx2-1x}\} \\
~~~~~~where \textsf{[$ys$ $xs$] $=$ (dmx2 $yxs$)}          & \\
\textsf{(dmx2 nil) $=$ [nil nil] }                         & \{\emph{dmx2-0x}\} \\
\end{tabular}
\end{center}\index{axiom, by name!\{dmx2-0x\}, \{dmx2-1x\}}\index{equation, by name!\{dmx2-0x\}, \{dmx2-1x\}}\index{operator, by name!dmx2 (demultiplexer)}
%\caption{Cleverness Sometimes Complicates Reasoning}
%\label{aside:dmx-defun-trick}
\end{aside}

\begin{exercises}
\exer {Prove that the \textsf{dmx} operator preserves total length.
That is, prove the theorem
stated formally in ACL2 as follows:}

\index{theorem, by name!\{dmx-length\}}
\label{thm:dmx-length}
\begin{quote}
\begin{verbatim}
(defthm dmx-length-thm
  (= (len xys)
     (+ (len (first (dmx xys)))
        (len (second (dmx xys))))))
\end{verbatim}
\end{quote}

\exer {Do paper-and-pencil proofs of the dmx-len-first and dmx-len-second
theorems (page \pageref{thm:dmx-length-first-second}).
You may find the proofs easier if you split them into
two cases, one when the operand has an even number of elements
(that is, $2n$ for some natural number $n$),
the other when it has an odd number of elements $(2n+1)$.}

\exer {\label{dmx-val-len-not-enough}%
Give an example of lists
\textsf{[$x$ $y$]}, \textsf{[$u$]}, and \textsf{[$w$]} for which
\textsf{[[$u$] [$w$]]} $\neq$ \textsf{(dmx [$x$ $y$])} but the following formula is true:\\
\hspace*{1cm}$\forall v.(($\textsf{(occurs-in $v$ [$u$])} $\vee$ \textsf{(occurs-in $v$ [$w$])}$)
\leftrightarrow$ \textsf{(occurs-in $v$ [$x$ $y$])}$)$\\
\emph{Note}: Such an example demonstrates that length and value
preservation are not enough to guarantee that \textsf{dmx} delivers the right value.
They aren't enough for the \textsf{mux} operator either %'
(exercise~\ref{mux-val-len-not-enough}, page \pageref{mux-val-len-not-enough}).}

\exer {\label{ex:dmx-val-thm}%
State formally, in ACL2, the dmx-val theorem
analogous to the mux-val theorem (page \pageref{aside:mux-val-thm}).}

\exer {The dmx-val theorem (exercise \ref{ex:dmx-val-thm})
says that \textsf{dmx} neither adds nor drops values from its operand.
Do a paper-and-pencil proof of the dmx-val theorem.}

\exer {\index{theorem, by name!\{dmx-val\}}%
Do a paper-and-pencil proof of the mux-inverts-dmx theorem
(page \pageref{thm:mux-inverts-dmx}).}

\exer {Do a paper-and-pencil proof of the dmx-inverts-mux theorem
(page \pageref{thm:dmx-inverts-mux}).}

\exer {\label{dmx2-eq-dmx}%
Do a paper-and-pencil proof that
\textsf{(dmx2 $xs$)} $=$ \textsf{(dmx $xs$)}.\\
\emph{Note}: \textsf{dmx2} is defined in
box~\ref{aside:dmx-defun-trick}, page \pageref{aside:dmx-defun-trick},
and \textsf{dmx} is defined on page \pageref{dmx-defun}.}

\end{exercises}