\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[]

\begin{verbatim}; Pigeon hole principle, as suggested by Randy Pollack.

\end{verbatim}
\noindent{\sc Event}:   Start with the initial {\bf nqthm} theory.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{subsetp} \\  
\=\+{\rm{subsetp}}\,({\it{x\/}}, {\it{y\/}})\index{subsetp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\rm{car}}\,({\it{x\/}}) $\in$ {\it{y\/}}$\;\;${\bf then }{\rm{subsetp}}\,({\rm{cdr}}\,({\it{x\/}}), {\it{y\/}})\index{subsetp} \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{dups} \\  
\=\+{\rm{dups}}\,({\it{l\/}})\index{dups} \\ 
$=$$\;\;\;\;$\=\+{\bf if }$\neg$ {\rm{listp}}\,({\it{l\/}})$\;\;${\bf then }{\bf{f}} \\ 
{\bf elseif }{\rm{car}}\,({\it{l\/}}) $\in$ {\rm{cdr}}\,({\it{l\/}})$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{dups}}\,({\rm{cdr}}\,({\it{l\/}}))\index{dups}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{remove} \\  
\=\+{\rm{remove}}\,({\it{x\/}}, {\it{z\/}})\index{remove} \\ 
$=$$\;\;\;\;$\=\+{\bf if }$\neg$ {\rm{listp}}\,({\it{z\/}})$\;\;${\bf then }{\it{z\/}} \\ 
{\bf elseif }{\it{x\/}} $=$ {\rm{car}}\,({\it{z\/}})$\;\;${\bf then }{\rm{remove}}\,({\it{x\/}}, {\rm{cdr}}\,({\it{z\/}}))\index{remove} \\ 
{\bf else }{\rm{cons}}\,({\rm{car}}\,({\it{z\/}}), {\rm{remove}}\,({\it{x\/}}, {\rm{cdr}}\,({\it{z\/}}))\index{remove})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remove-preserves-subsetp \\ \index{remove-preserves-subsetp}
({\rm{listp}}\,({\it{a\/}}) $\wedge$ {\rm{subsetp}}\,({\it{a\/}}, {\it{b\/}})\index{subsetp}) $\rightarrow$ {\rm{subsetp}}\,({\rm{remove}}\,({\it{x\/}}, {\it{a\/}})\index{remove}, {\rm{remove}}\,({\it{x\/}}, {\it{b\/}})\index{remove})\index{subsetp}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{double-list-ind} \\  
\=\+{\rm{double-list-ind}}\,({\it{l\/}}, {\it{m\/}})\index{double-list-ind} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{l\/}}) $\wedge$ {\rm{listp}}\,({\it{m\/}}) \\ 
{\bf then }{\rm{double-list-ind}}\,({\rm{remove}}\,({\rm{car}}\,({\it{m\/}}), {\it{l\/}})\index{remove}, {\rm{cdr}}\,({\it{m\/}}))\index{double-list-ind} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remove-car-non-dups \\ \index{remove-car-non-dups}
({\rm{listp}}\,({\it{m\/}}) $\wedge$ ($\neg$ {\rm{dups}}\,({\it{m\/}})\index{dups})) $\rightarrow$ ({\rm{remove}}\,({\rm{car}}\,({\it{m\/}}), {\it{m\/}})\index{remove} $=$ {\rm{cdr}}\,({\it{m\/}}))
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{length} \\  
\=\+{\rm{length}}\,({\it{lst\/}})\index{length} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{lst\/}})$\;\;${\bf then }$1\;+$ {\rm{length}}\,({\rm{cdr}}\,({\it{lst\/}}))\index{length} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  length-remove-leq \\ \index{length-remove-leq}
({\rm{length}}\,({\it{l\/}})\index{length} $<$ {\rm{length}}\,({\rm{remove}}\,({\it{x\/}}, {\it{l\/}})\index{remove})\index{length}) $=$ {\bf{f}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  length-remove-lessp \\ \index{length-remove-lessp}
({\it{x\/}} $\in$ {\it{l\/}}) $\rightarrow$ (({\rm{length}}\,({\rm{remove}}\,({\it{x\/}}, {\it{l\/}})\index{remove})\index{length} $<$ {\rm{length}}\,({\it{l\/}})\index{length}) $=$ {\bf{t}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subsetp-dups \\ \index{subsetp-dups}
(({\rm{length}}\,({\it{l\/}})\index{length} $<$ {\rm{length}}\,({\it{m\/}})\index{length}) $\wedge$ {\rm{subsetp}}\,({\it{m\/}}, {\it{l\/}})\index{subsetp}) $\rightarrow$ {\rm{dups}}\,({\it{m\/}})\index{dups}
\end{tabbing}

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