\newcommand{\LD}[2]{$\cal L\!D$\ldb {#1}\rdb\ldb {#2}\rdb}
\newcommand{\av}{$a$ $v$}

\begin{tt}
\begin{tabular}{lr@{\ $=$\ }l}
\LF{\unfold\ $P$ $F$ $V$} & \aut & 
\begin{minipage}[t]{6in}
\begin{tabbing}
let h v acc \= | \LE{$P$} = acc\+\\
               | ot\= herwise = \LD{h v'}{acc} $a$ $(u$ e$)$ \+\\
                        where (e,v') = \LE{$F$} v \- \- \\
in h \LE{$V$} $t$
\end{tabbing}
\end{minipage}
\\
\multicolumn{3}{r}{\rm omitting $\cal L\!E$ when $u \neq u_{list}$}\\
\LF{$E$} &      $a$ $u_{list}$ $t$ &    \LE{$E$} ++ $t$ \\
\multicolumn{3}{l}{Otherwise:}\\
\LF{$E$} & \aut &
\begin{minipage}[t]{6in}
\begin{tabbing}
let \=  h []~~~~~acc = acc\+\\
        h (e:es) acc = \LD{h es}{acc} $a$ $(u$ e$)$ \-\\
in h \LE{$E$} $t$
\end{tabbing}
\end{minipage}
\\
\multicolumn{3}{c}{}
\end{tabular}
\begin{tabular}{lr@{\ $=$\ }ll}
\multicolumn{4}{c}{}\\
\multicolumn{4}{l}{\rm When $a$ is from a reduction or is {\tt bothways}:}\\
\LD{$R$}{$A$}& \av & $R$ $(v\:A)$ &     $a=$bothways (.){\rm , $v$ strict}\\
\LD{$R$}{$A$}& \av & $R$ $(a\:(\lambda x.\:A)\:v\:A)$ &
        $a$ {\rm strict in second argument}\\
\LD{$R$}{$A$}& \av & $R$ $(a\:v\:(\lambda x.\:A)\:A)$ &
        $a=$bothways $a'$, $a$ {\rm strict in first argument}\\
\multicolumn{4}{l}{\rm If none of the above apply:}\\
\LD{$R$}{$A$}& \av & $a$ $v$ ($R$) $A$ &\\
\multicolumn{4}{c}{}\\
\end{tabular}
\end{tt}