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

To show that formula $Inv$ is not an inductive invariant,
consider a step that starts with control at $d$ and $x$ equal to $y$.
I believe the simplest inductive invariant that implies
$PartialCorrectness$ is:
 \[ \begin{conj}
    Inv \V{.2}
    (pc = "d") => (x # y)
    \end{conj}
 \]
\end{popup}
\makepopup