\documentclass[fleqn,leqno]{article}
\usepackage{hypertlabook}
\pdftitle{Answer}
\begin{popup}
\subsection*{Answer}

We let $Put(box)$ and $Get(box)$ be the set of all possible next
values of $box$ after executing the $put$ and $get$ operations.  We
can then write the $put$ operation as
\begin{display}
\textbf{with (}\,$v \in Put(box)$\,\textbf{) \{} 
    $box := v$ \textbf{\}}
\end{display}
and the $get$ operation as
\begin{display}
\textbf{with (}\,$v \in Get(box)$\,\textbf{) \{} 
    $box := v$ \textbf{\}}
\end{display}


\end{popup}
\makepopup