\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 nqthm} theory.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  plus-difference-shit \\ \index{plus-difference-shit}
\=\+(({\it{z\/}} $<$ {\it{y\/}}) $\wedge$ ({\it{b\/}} $\leq$ {\it{a\/}})) \\ 
$\rightarrow$$\;\;\;\;$((({\it{y\/}} $+$ {\it{a\/}}) $-$ ({\it{z\/}} $+$ {\it{b\/}})) $=$ (({\it{y\/}} $-$ {\it{z\/}}) $+$ ({\it{a\/}} $-$ {\it{b\/}})))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  times-lessp \\ \index{times-lessp}
({\it{b\/}} $\not<$ {\it{a\/}}) $\rightarrow$ ((({\it{x\/}} $*$ {\it{b\/}}) $<$ ({\it{x\/}} $*$ {\it{a\/}})) $=$ {\bf{f}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  difference-lessp \\ \index{difference-lessp}
({\it{a\/}} $\not<$ {\it{b\/}}) $\rightarrow$ (({\it{b\/}} $-$ {\it{a\/}}) $=$ {\tt{0}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-plus \\ \index{lessp-plus}
(({\it{a\/}} $\not<$ {\it{b\/}}) $\wedge$ ({\it{c\/}} $\not<$ {\it{d\/}})) $\rightarrow$ ((({\it{a\/}} $+$ {\it{c\/}}) $<$ ({\it{b\/}} $+$ {\it{d\/}})) $=$ {\bf{f}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  times-difference-dist \\ \index{times-difference-dist}
({\it{x\/}} $*$ ({\it{y\/}} $-$ {\it{z\/}})) $=$ (({\it{x\/}} $*$ {\it{y\/}}) $-$ ({\it{x\/}} $*$ {\it{z\/}}))
\end{tabbing}

%\end{list}
\printindex
\end{document}
