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

You must have TLC check that 
  \[~((pc[0] = "put") /\ (pc[1] = "get"))\]
is an invariant of algorithm $AltSpec$.
\end{popup}
\makepopup