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

The translation of algorithm $DieHarder$ defines the next-state action
to equal:
\[ \begin{disj}
   \,\E\, j \in Jugs : F_{1} \V{.2}
   \,\E\, j \in Jugs : F_{2} \V{.2}
   \,\E\, j \in Jugs : F_{3} 
   \end{disj}
\]
for formulas $F_{1}$, $F_{2}$, and $F_{3}$.
The translation of the modified algorithm defines the next-state
action to be the equivalent formula:
 \[ \E\, j \in Jugs : F_{1} \/ F_{2} \/ F_{3}
 \]

\end{popup}
\makepopup