\documentclass[fleqn,leqno]{article}
\usepackage{hypertlabook}
\pdftitle{ASCII Text}
\fixverbatim
\begin{popup}
\begin{verbatim*}
Liveness == \A i \in Nat, j \in 1..N : 
              (Len(out) = i) /\ (Len(ch) = j) ~> (Len(out) = i+j)
\end{verbatim*}
\end{popup}
\makeasciipopup