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

In such a behavior $s_{1}->s_{2}->\cdots$, there is no $j$ such that
$<<Proc(i)>>_{vars}$ is enabled for all states $s_{k}$ with $k\geq j$,
so $\WF_{vars}(Proc(i))$ is true in this behavior even if there are no
$Proc(i)$ steps.

\end{popup}
\makepopup