\documentstyle[makeidx]{article}
\makeindex
%\setlength{\oddsidemargin}{.5in}
%\setlength{\evensidemargin}{.5in}
%\setlength{\textwidth}{5.8in}
\begin{document}
%\setlength{\parindent}{0pt}
%\newcounter{bean}
%\begin{list}{\arabic{bean}.}{\usecounter{bean}\setlength{\leftmargin}{0pt}\setlength{\rightmargin}{0pt}\setlength{\listparindent}{20pt}\setlength{\parsep}{5pt}}
%\item[]


\noindent{\sc Event}:   Start with the initial {\bf thm} theory.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{merge} \\  
\=\+{\rm{merge}}\,({\it{l\/}}, {\it{m\/}})\index{merge} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{l\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\it{m\/}} \\ 
{\bf elseif }{\it{m\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\it{l\/}} \\ 
{\bf elseif }{\rm{car}}\,({\it{l\/}}) $<$ {\rm{car}}\,({\it{m\/}})$\;\;${\bf then }{\rm{cons}}\,({\rm{car}}\,({\it{l\/}}), {\rm{merge}}\,({\rm{cdr}}\,({\it{l\/}}), {\it{m\/}})\index{merge}) \\ 
{\bf else }{\rm{cons}}\,({\rm{car}}\,({\it{m\/}}), {\rm{merge}}\,({\it{l\/}}, {\rm{cdr}}\,({\it{m\/}}))\index{merge})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{evens} \\  
\=\+{\rm{evens}}\,({\it{l\/}})\index{evens} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{l\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf elseif }{\rm{cdr}}\,({\it{l\/}}) $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{cons}}\,({\rm{cadr}}\,({\it{l\/}}), {\rm{evens}}\,({\rm{cddr}}\,({\it{l\/}}))\index{evens})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{odds} \\  
\=\+{\rm{odds}}\,({\it{l\/}})\index{odds} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{l\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{cons}}\,({\rm{car}}\,({\it{l\/}}), {\rm{odds}}\,({\rm{cddr}}\,({\it{l\/}}))\index{odds})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  evens-length \\ \index{evens-length}
(({\it{l\/}} $\not\simeq\;${{\bf{nil}}}${}$) $\wedge$ ({\rm{cdr}}\,({\it{l\/}}) $\not\simeq\;${{\bf{nil}}}${}$)) $\rightarrow$ ({\rm{length}}\,({\rm{evens}}\,({\it{l\/}})\index{evens})\index{length} $<$ {\rm{length}}\,({\it{l\/}})\index{length})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{mergesort} \\  
\=\+{\rm{mergesort}}\,({\it{l\/}})\index{mergesort} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{l\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf elseif }{\rm{cdr}}\,({\it{l\/}}) $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\it{l\/}} \\ 
{\bf else }{\rm{merge}}\,({\rm{mergesort}}\,({\rm{evens}}\,({\it{l\/}})\index{evens})\index{mergesort}, {\rm{mergesort}}\,({\rm{odds}}\,({\it{l\/}})\index{odds})\index{mergesort})\index{merge}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; Interestingly, the prover can now prove (SORTEDP (MERGESORT L)) automatically,
; but we won't bother with that here.
\end{verbatim}
%\end{list}
\printindex
\end{document}
