\documentclass[fleqn,leqno]{article}
\usepackage{hypertlabook}
\pdftitle{ASCII Text}
\fixverbatim
\begin{popup}
\begin{verbatim*}
THEOREM Induction == Inv /\ Next => Inv'
<1>1. SUFFICES ASSUME Inv, Next
               PROVE  Inv'
  OBVIOUS

<1>2. CASE /\ x > y
           /\ x' = x - y
           /\ y' = y  
  <2>1. TypeOK'   
    BY <1>1, <1>2, SimpleArithmetic DEF Inv, TypeOK
  <2>2. GCDInv'  
    <3>1. GCD(y, x) = GCD(y', x')
      BY <1>1, <1>2, GCD3 DEF Inv, TypeOK
    <3>2. QED
      BY <1>1, <3>1, <2>1, GCD2 DEF Inv, TypeOK, GCDInv
  <2>3. QED
    BY <2>1, <2>2 DEF Inv
 
<1>3. CASE /\ y > x
           /\ y' = y - x
           /\ x' = x
  <2>1. TypeOK'   
    BY <1>1, <1>3, SimpleArithmetic DEF Inv, TypeOK
  <2>2. GCDInv'
    BY  <1>1, <1>3, GCD3 DEF Inv, TypeOK, GCDInv
  <2>3. QED
    BY <2>1, <2>2 DEF Inv  
    
<1>4. QED
  BY <1>1, <1>2, <1>3 DEF Next
\end{verbatim*}
\end{popup}
\makeasciipopup