\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}#|

 Copyright (C) 1994 by Computational Logic, Inc.  All Rights Reserved.

 This script is hereby placed in the public domain, and therefore unlimited
 editing and redistribution is permitted.

 NO WARRANTY

 Computational Logic, Inc. PROVIDES ABSOLUTELY NO WARRANTY.  THE EVENT SCRIPT
 IS PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS OR IMPLIED,
 INCLUDING, BUT NOT LIMITED TO, ANY IMPLIED WARRANTIES OF MERCHANTABILITY AND
 FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND
 PERFORMANCE OF THE SCRIPT IS WITH YOU.  SHOULD THE SCRIPT PROVE DEFECTIVE, YOU
 ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION.

 IN NO EVENT WILL Computational Logic, Inc. BE LIABLE TO YOU FOR ANY DAMAGES,
 ANY LOST PROFITS, LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR CONSEQUENTIAL
 DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THIS SCRIPT (INCLUDING BUT
 NOT LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES
 SUSTAINED BY THIRD PARTIES), EVEN IF YOU HAVE ADVISED US OF THE POSSIBILITY OF
 SUCH DAMAGES, OR FOR ANY CLAIM BY ANY OTHER PARTY.
|#

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

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{ramsey} \\  
\=\+{\rm{ramsey}}\,({\it{p\/}}, {\it{q\/}})\index{ramsey} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{p\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{q\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\rm{ramsey}}\,({\it{p\/}} $-\;1$, {\it{q\/}})\index{ramsey} $+$ {\rm{ramsey}}\,({\it{p\/}}, {\it{q\/}} $-\;1$)\index{ramsey}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{related} \\  
{\rm{related}}\,({\it{i\/}}, {\it{j\/}}, {\it{pairs\/}})\index{related} $=$ (({\rm{cons}}\,({\it{i\/}}, {\it{j\/}}) $\in$ {\it{pairs\/}}) $\vee$ ({\rm{cons}}\,({\it{j\/}}, {\it{i\/}}) $\in$ {\it{pairs\/}}))
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{partition} \\  
\=\+{\rm{partition}}\,({\it{n\/}}, {\it{rest\/}}, {\it{pairs\/}})\index{partition} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{rest\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{related}}\,({\it{n\/}}, {\rm{car}}\,({\it{rest\/}}), {\it{pairs\/}})\index{related} \\ 
{\bf then }{\rm{cons}}\,(\=\+{\rm{cons}}\,({\rm{car}}\,({\it{rest\/}}), {\rm{car}}\,({\rm{partition}}\,({\it{n\/}}, {\rm{cdr}}\,({\it{rest\/}}), {\it{pairs\/}})\index{partition})), \\ 
{\rm{cdr}}\,({\rm{partition}}\,({\it{n\/}}, {\rm{cdr}}\,({\it{rest\/}}), {\it{pairs\/}})\index{partition}))\- \\ 
{\bf else }{\rm{cons}}\,(\=\+{\rm{car}}\,({\rm{partition}}\,({\it{n\/}}, {\rm{cdr}}\,({\it{rest\/}}), {\it{pairs\/}})\index{partition}), \\ 
{\rm{cons}}\,({\rm{car}}\,({\it{rest\/}}), {\rm{cdr}}\,({\rm{partition}}\,({\it{n\/}}, {\rm{cdr}}\,({\it{rest\/}}), {\it{pairs\/}})\index{partition})))\-$\;${\bf  endif}\- \\ 
{\bf else }{\rm{cons}}\,({\bf{nil}}, {\bf{nil}})$\;${\bf  endif}\-\-
\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 Definition}:\index{wit} \\  
\=\+{\rm{wit}}\,({\it{pairs\/}}, {\it{domain\/}}, {\it{p\/}}, {\it{q\/}})\index{wit} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{domain\/}}) \\ 
{\bf then }\=\+{\bf if }{\it{p\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{cons}}\,({\bf{nil}}, {\tt{1}}) \\ 
{\bf elseif }{\it{q\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{cons}}\,({\bf{nil}}, {\tt{2}}) \\ 
{\bf elseif }\=\+{\rm{length}}\,({\rm{car}}\,({\rm{partition}}\,({\rm{car}}\,({\it{domain\/}}), {\rm{cdr}}\,({\it{domain\/}}), {\it{pairs\/}})\index{partition}))\index{length} \\ 
$<$$\;\;\;\;${\rm{ramsey}}\,({\it{p\/}} $-\;1$, {\it{q\/}})\index{ramsey}\- \\ 
{\bf then }\=\+{\bf if }\=\+{\rm{cdr}}\,({\rm{wit}}\,(\=\+{\it{pairs\/}}, \\ 
{\rm{cdr}}\,({\rm{partition}}\,({\rm{car}}\,({\it{domain\/}}), {\rm{cdr}}\,({\it{domain\/}}), {\it{pairs\/}})\index{partition}), \\ 
{\it{p\/}}, \\ 
{\it{q\/}} $-\;1$)\-\index{wit}) \\ 
$=$$\;\;\;\;${\tt{1}}\- \\ 
{\bf then }{\rm{wit}}\,(\=\+{\it{pairs\/}}, \\ 
{\rm{cdr}}\,({\rm{partition}}\,({\rm{car}}\,({\it{domain\/}}), {\rm{cdr}}\,({\it{domain\/}}), {\it{pairs\/}})\index{partition}), \\ 
{\it{p\/}}, \\ 
{\it{q\/}} $-\;1$)\-\index{wit} \\ 
{\bf else }{\rm{cons}}\,(\=\+{\rm{cons}}\,(\=\+{\rm{car}}\,({\it{domain\/}}), \\ 
{\rm{car}}\,({\rm{wit}}\,(\=\+{\it{pairs\/}}, \\ 
{\rm{cdr}}\,({\rm{partition}}\,(\=\+{\rm{car}}\,({\it{domain\/}}), \\ 
{\rm{cdr}}\,({\it{domain\/}}), \\ 
{\it{pairs\/}})\-\index{partition}), \\ 
{\it{p\/}}, \\ 
{\it{q\/}} $-\;1$)\-\index{wit}))\-, \\ 
{\tt{2}})\-$\;${\bf  endif}\- \\ 
{\bf elseif }\=\+{\rm{cdr}}\,({\rm{wit}}\,(\=\+{\it{pairs\/}}, \\ 
{\rm{car}}\,({\rm{partition}}\,({\rm{car}}\,({\it{domain\/}}), {\rm{cdr}}\,({\it{domain\/}}), {\it{pairs\/}})\index{partition}), \\ 
{\it{p\/}} $-\;1$, \\ 
{\it{q\/}})\-\index{wit}) \\ 
$=$$\;\;\;\;${\tt{2}}\- \\ 
{\bf then }{\rm{wit}}\,(\=\+{\it{pairs\/}}, \\ 
{\rm{car}}\,({\rm{partition}}\,({\rm{car}}\,({\it{domain\/}}), {\rm{cdr}}\,({\it{domain\/}}), {\it{pairs\/}})\index{partition}), \\ 
{\it{p\/}} $-\;1$, \\ 
{\it{q\/}})\-\index{wit} \\ 
{\bf else }{\rm{cons}}\,(\=\+{\rm{cons}}\,(\=\+{\rm{car}}\,({\it{domain\/}}), \\ 
{\rm{car}}\,({\rm{wit}}\,(\=\+{\it{pairs\/}}, \\ 
{\rm{car}}\,({\rm{partition}}\,(\=\+{\rm{car}}\,({\it{domain\/}}), \\ 
{\rm{cdr}}\,({\it{domain\/}}), \\ 
{\it{pairs\/}})\-\index{partition}), \\ 
{\it{p\/}} $-\;1$, \\ 
{\it{q\/}})\-\index{wit}))\-, \\ 
{\tt{1}})\-$\;${\bf  endif}\- \\ 
{\bf else }{\rm{cons}}\,({\bf{nil}}, {\tt{1}})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{homogeneous1} \\  
\=\+{\rm{homogeneous1}}\,({\it{n\/}}, {\it{domain\/}}, {\it{pairs\/}}, {\it{flg\/}})\index{homogeneous1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{domain\/}}) \\ 
{\bf then }\=\+\=\+{\bf if }{\it{flg\/}} $=$ {\tt{1}}$\;\;${\bf then }{\rm{related}}\,({\it{n\/}}, {\rm{car}}\,({\it{domain\/}}), {\it{pairs\/}})\index{related} \\ 
{\bf else }$\neg$ {\rm{related}}\,({\it{n\/}}, {\rm{car}}\,({\it{domain\/}}), {\it{pairs\/}})\index{related}$\;${\bf  endif}\- \\ 
$\wedge$$\;\;\;\;${\rm{homogeneous1}}\,({\it{n\/}}, {\rm{cdr}}\,({\it{domain\/}}), {\it{pairs\/}}, {\it{flg\/}})\index{homogeneous1}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{homogeneous} \\  
\=\+{\rm{homogeneous}}\,({\it{domain\/}}, {\it{pairs\/}}, {\it{flg\/}})\index{homogeneous} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{domain\/}}) \\ 
{\bf then }\=\+{\rm{homogeneous1}}\,({\rm{car}}\,({\it{domain\/}}), {\rm{cdr}}\,({\it{domain\/}}), {\it{pairs\/}}, {\it{flg\/}})\index{homogeneous1} \\ 
$\wedge$$\;\;\;\;${\rm{homogeneous}}\,({\rm{cdr}}\,({\it{domain\/}}), {\it{pairs\/}}, {\it{flg\/}})\index{homogeneous}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\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 Theorem}:  member-cons \\ \index{member-cons}
({\it{a\/}} $\in$ {\it{l\/}}) $\rightarrow$ ({\it{a\/}} $\in$ {\rm{cons}}\,({\it{x\/}}, {\it{l\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subsetp-cons \\ \index{subsetp-cons}
{\rm{subsetp}}\,({\it{l\/}}, {\it{m\/}})\index{subsetp} $\rightarrow$ {\rm{subsetp}}\,({\it{l\/}}, {\rm{cons}}\,({\it{a\/}}, {\it{m\/}}))\index{subsetp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subsetp-reflexivity \\ \index{subsetp-reflexivity}
{\rm{subsetp}}\,({\it{x\/}}, {\it{x\/}})\index{subsetp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  cdr-subsetp \\ \index{cdr-subsetp}
{\rm{subsetp}}\,({\rm{cdr}}\,({\it{x\/}}), {\it{x\/}})\index{subsetp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member-subsetp \\ \index{member-subsetp}
(({\it{x\/}} $\in$ {\it{y\/}}) $\wedge$ {\rm{subsetp}}\,({\it{y\/}}, {\it{z\/}})\index{subsetp}) $\rightarrow$ ({\it{x\/}} $\in$ {\it{z\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subsetp-is-transitive \\ \index{subsetp-is-transitive}
({\rm{subsetp}}\,({\it{x\/}}, {\it{y\/}})\index{subsetp} $\wedge$ {\rm{subsetp}}\,({\it{y\/}}, {\it{z\/}})\index{subsetp}) $\rightarrow$ {\rm{subsetp}}\,({\it{x\/}}, {\it{z\/}})\index{subsetp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subsetp-cdr-partition \\ \index{subsetp-cdr-partition}
{\rm{subsetp}}\,({\rm{cdr}}\,({\rm{partition}}\,({\it{x\/}}, {\it{z\/}}, {\it{pairs\/}})\index{partition}), {\it{z\/}})\index{subsetp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subsetp-hom-set-domain-1 \\ \index{subsetp-hom-set-domain-1}
\=\+{\rm{subsetp}}\,(\=\+{\rm{car}}\,({\rm{wit}}\,({\it{pairs\/}}, {\rm{cdr}}\,({\rm{partition}}\,({\it{x\/}}, {\it{z\/}}, {\it{pairs\/}})\index{partition}), {\it{p\/}}, {\it{q\/}})\index{wit}), \\ 
{\rm{cdr}}\,({\rm{partition}}\,({\it{x\/}}, {\it{z\/}}, {\it{pairs\/}})\index{partition}))\-\index{subsetp} \\ 
$\rightarrow$$\;\;\;\;${\rm{subsetp}}\,({\rm{car}}\,({\rm{wit}}\,({\it{pairs\/}}, {\rm{cdr}}\,({\rm{partition}}\,({\it{x\/}}, {\it{z\/}}, {\it{pairs\/}})\index{partition}), {\it{p\/}}, {\it{q\/}})\index{wit}), {\rm{cons}}\,({\it{x\/}}, {\it{z\/}}))\index{subsetp}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subsetp-car-partition \\ \index{subsetp-car-partition}
{\rm{subsetp}}\,({\rm{car}}\,({\rm{partition}}\,({\it{x\/}}, {\it{z\/}}, {\it{pairs\/}})\index{partition}), {\it{z\/}})\index{subsetp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subsetp-hom-set-domain-2 \\ \index{subsetp-hom-set-domain-2}
\=\+{\rm{subsetp}}\,(\=\+{\rm{car}}\,({\rm{wit}}\,({\it{pairs\/}}, {\rm{car}}\,({\rm{partition}}\,({\it{x\/}}, {\it{z\/}}, {\it{pairs\/}})\index{partition}), {\it{p\/}}, {\it{q\/}})\index{wit}), \\ 
{\rm{car}}\,({\rm{partition}}\,({\it{x\/}}, {\it{z\/}}, {\it{pairs\/}})\index{partition}))\-\index{subsetp} \\ 
$\rightarrow$$\;\;\;\;${\rm{subsetp}}\,({\rm{car}}\,({\rm{wit}}\,({\it{pairs\/}}, {\rm{car}}\,({\rm{partition}}\,({\it{x\/}}, {\it{z\/}}, {\it{pairs\/}})\index{partition}), {\it{p\/}}, {\it{q\/}})\index{wit}), {\rm{cons}}\,({\it{x\/}}, {\it{z\/}}))\index{subsetp}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subsetp-hom-set-domain \\ \index{subsetp-hom-set-domain}
{\rm{subsetp}}\,({\rm{car}}\,({\rm{wit}}\,({\it{pairs\/}}, {\it{domain\/}}, {\it{p\/}}, {\it{q\/}})\index{wit}), {\it{domain\/}})\index{subsetp}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{good-hom-set} \\  
\=\+{\rm{good-hom-set}}\,({\it{pairs\/}}, {\it{domain\/}}, {\it{p\/}}, {\it{q\/}}, {\it{flg\/}})\index{good-hom-set} \\ 
$=$$\;\;\;\;$(\=\+{\rm{homogeneous}}\,({\rm{car}}\,({\rm{wit}}\,({\it{pairs\/}}, {\it{domain\/}}, {\it{p\/}}, {\it{q\/}})\index{wit}), {\it{pairs\/}}, {\it{flg\/}})\index{homogeneous} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{length}}\,({\rm{car}}\,({\rm{wit}}\,({\it{pairs\/}}, {\it{domain\/}}, {\it{p\/}}, {\it{q\/}})\index{wit}))\index{length} \\ 
$\not<$$\;\;\;\;$\=\+{\bf if }{\it{flg\/}} $=$ {\tt{1}}$\;\;${\bf then }{\it{p\/}} \\ 
{\bf else }{\it{q\/}}$\;${\bf  endif}\-)\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  homogeneous1-subset \\ \index{homogeneous1-subset}
\=\+({\rm{subsetp}}\,({\it{x\/}}, {\it{domain\/}})\index{subsetp} $\wedge$ {\rm{homogeneous1}}\,({\it{elt\/}}, {\it{domain\/}}, {\it{pairs\/}}, {\it{flg\/}})\index{homogeneous1}) \\ 
$\rightarrow$$\;\;\;\;${\rm{homogeneous1}}\,({\it{elt\/}}, {\it{x\/}}, {\it{pairs\/}}, {\it{flg\/}})\index{homogeneous1}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  homogeneous1-cdr-partition \\ \index{homogeneous1-cdr-partition}
{\rm{homogeneous1}}\,({\it{elt\/}}, {\rm{cdr}}\,({\rm{partition}}\,({\it{elt\/}}, {\it{dom\/}}, {\it{pairs\/}})\index{partition}), {\it{pairs\/}}, {\tt{2}})\index{homogeneous1}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  length-partition-1 \\ \index{length-partition-1}
\=\+{\rm{length}}\,({\it{z\/}})\index{length} \\ 
$=$$\;\;\;\;$(\=\+{\rm{length}}\,({\rm{car}}\,({\rm{partition}}\,({\it{x\/}}, {\it{z\/}}, {\it{pairs\/}})\index{partition}))\index{length} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\rm{cdr}}\,({\rm{partition}}\,({\it{x\/}}, {\it{z\/}}, {\it{pairs\/}})\index{partition}))\index{length})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  length-partition \\ \index{length-partition}
\=\+{\rm{length}}\,({\rm{car}}\,({\rm{partition}}\,({\it{x\/}}, {\it{z\/}}, {\it{pairs\/}})\index{partition}))\index{length} \\ 
$=$$\;\;\;\;$({\rm{length}}\,({\it{z\/}})\index{length} $-$ {\rm{length}}\,({\rm{cdr}}\,({\rm{partition}}\,({\it{x\/}}, {\it{z\/}}, {\it{pairs\/}})\index{partition}))\index{length})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ramsey-not-zero \\ \index{ramsey-not-zero}
{\tt{0}} $<$ {\rm{ramsey}}\,({\it{p\/}}, {\it{q\/}})\index{ramsey}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  homogeneous1-car-wit-cdr-partition \\ \index{homogeneous1-car-wit-cdr-partiti!on}
{\rm{homogeneous1}}\,({\it{elt\/}}, {\rm{car}}\,({\rm{wit}}\,({\it{pairs\/}}, {\rm{cdr}}\,({\rm{partition}}\,({\it{elt\/}}, {\it{dom\/}}, {\it{pairs\/}})\index{partition}), {\it{p\/}}, {\it{q\/}})\index{wit}), {\it{pairs\/}}, {\tt{2}})\index{homogeneous1}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  homogeneous1-car-partition \\ \index{homogeneous1-car-partition}
{\rm{homogeneous1}}\,({\it{elt\/}}, {\rm{car}}\,({\rm{partition}}\,({\it{elt\/}}, {\it{dom\/}}, {\it{pairs\/}})\index{partition}), {\it{pairs\/}}, {\tt{1}})\index{homogeneous1}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  homogeneous1-car-wit-car-partition \\ \index{homogeneous1-car-wit-car-partiti!on}
{\rm{homogeneous1}}\,({\it{elt\/}}, {\rm{car}}\,({\rm{wit}}\,({\it{pairs\/}}, {\rm{car}}\,({\rm{partition}}\,({\it{elt\/}}, {\it{dom\/}}, {\it{pairs\/}})\index{partition}), {\it{p\/}}, {\it{q\/}})\index{wit}), {\it{pairs\/}}, {\tt{1}})\index{homogeneous1}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  cdr-wit-is-1-or-2 \\ \index{cdr-wit-is-1-or-2}
({\rm{cdr}}\,({\rm{wit}}\,({\it{pairs\/}}, {\it{dom\/}}, {\it{p\/}}, {\it{q\/}})\index{wit}) $\not=$ {\tt{1}}) $\rightarrow$ ({\rm{cdr}}\,({\rm{wit}}\,({\it{pairs\/}}, {\it{dom\/}}, {\it{p\/}}, {\it{q\/}})\index{wit}) $=$ {\tt{2}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  wit-yields-good-hom-set \\ \index{wit-yields-good-hom-set}
\=\+({\rm{length}}\,({\it{domain\/}})\index{length} $\not<$ {\rm{ramsey}}\,({\it{p\/}}, {\it{q\/}})\index{ramsey}) \\ 
$\rightarrow$$\;\;\;\;${\rm{good-hom-set}}\,({\it{pairs\/}}, {\it{domain\/}}, {\it{p\/}}, {\it{q\/}}, {\rm{cdr}}\,({\rm{wit}}\,({\it{pairs\/}}, {\it{domain\/}}, {\it{p\/}}, {\it{q\/}})\index{wit}))\index{good-hom-set}\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{setp} \\  
\=\+{\rm{setp}}\,({\it{x\/}})\index{setp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}})$\;\;${\bf then }({\rm{car}}\,({\it{x\/}}) $\not\in$ {\rm{cdr}}\,({\it{x\/}})) $\wedge$ {\rm{setp}}\,({\rm{cdr}}\,({\it{x\/}}))\index{setp} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  setp-partition \\ \index{setp-partition}
\=\+{\rm{setp}}\,({\it{x\/}})\index{setp} \\ 
$\rightarrow$$\;\;\;\;$({\rm{setp}}\,({\rm{car}}\,({\rm{partition}}\,({\it{a\/}}, {\it{x\/}}, {\it{pairs\/}})\index{partition}))\index{setp} $\wedge$ {\rm{setp}}\,({\rm{cdr}}\,({\rm{partition}}\,({\it{a\/}}, {\it{x\/}}, {\it{pairs\/}})\index{partition}))\index{setp})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  not-member-car-wit-cdr-partition \\ \index{not-member-car-wit-cdr-partitio!n}
({\it{z\/}} $\not\in$ {\it{x\/}}) $\rightarrow$ ({\it{z\/}} $\not\in$ {\rm{car}}\,({\rm{wit}}\,({\it{pairs\/}}, {\rm{cdr}}\,({\rm{partition}}\,({\it{z\/}}, {\it{x\/}}, {\it{pairs\/}})\index{partition}), {\it{p\/}}, {\it{q\/}})\index{wit}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  not-member-car-wit-car-partition \\ \index{not-member-car-wit-car-partitio!n}
({\it{z\/}} $\not\in$ {\it{x\/}}) $\rightarrow$ ({\it{z\/}} $\not\in$ {\rm{car}}\,({\rm{wit}}\,({\it{pairs\/}}, {\rm{car}}\,({\rm{partition}}\,({\it{z\/}}, {\it{x\/}}, {\it{pairs\/}})\index{partition}), {\it{p\/}}, {\it{q\/}})\index{wit}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  setp-hom-set \\ \index{setp-hom-set}
{\rm{setp}}\,({\it{domain\/}})\index{setp} $\rightarrow$ {\rm{setp}}\,({\rm{car}}\,({\rm{wit}}\,({\it{pairs\/}}, {\it{domain\/}}, {\it{p\/}}, {\it{q\/}})\index{wit}))\index{setp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ramsey-theorem-2 \\ \index{ramsey-theorem-2}
\=\+({\rm{ramsey}}\,({\it{p\/}}, {\it{q\/}})\index{ramsey} $\leq$ {\rm{length}}\,({\it{domain\/}})\index{length}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{subsetp}}\,({\rm{car}}\,({\rm{wit}}\,({\it{pairs\/}}, {\it{domain\/}}, {\it{p\/}}, {\it{q\/}})\index{wit}), {\it{domain\/}})\index{subsetp} \\ 
$\wedge$$\;\;\;\;${\rm{good-hom-set}}\,({\it{pairs\/}}, {\it{domain\/}}, {\it{p\/}}, {\it{q\/}}, {\rm{cdr}}\,({\rm{wit}}\,({\it{pairs\/}}, {\it{domain\/}}, {\it{p\/}}, {\it{q\/}})\index{wit}))\index{good-hom-set} \\ 
$\wedge$$\;\;\;\;$({\rm{setp}}\,({\it{domain\/}})\index{setp} $\rightarrow$ {\rm{setp}}\,({\rm{car}}\,({\rm{wit}}\,({\it{pairs\/}}, {\it{domain\/}}, {\it{p\/}}, {\it{q\/}})\index{wit}))\index{setp}))\-\-
\end{tabbing}


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