\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}; Matt Kaufmann, ICSCA, Univ. of Texas, Austin, TX 78712
; 1/26/87

; Here is a mechanically-checked proof of the finite version
; of Ramsey's Theorem for exponent 2.  This proof was shown
; to me (with ordinary mathematical notation rather than in
; the Boyer-Moore logic) by Jim Schmerl, who claims that it's
; not a new proof.

; Theorem (RAMSEY-THM-2):

; (IMPLIES (LEQ (RAMSEY P Q)
;               (LENGTH DOMAIN))
;          (AND
;            (SUBSETP (HOM-SET PAIRS DOMAIN P Q)
;                     DOMAIN)
;            (OR
;              (AND (HOMOGENEOUS (HOM-SET PAIRS DOMAIN P Q)
;                                PAIRS
;                                1)
;                   (LEQ P (LENGTH (HOM-SET PAIRS DOMAIN P Q))))
;              (AND (HOMOGENEOUS (HOM-SET PAIRS DOMAIN P Q)
;                                PAIRS
;                                2)
;                   (LEQ Q (LENGTH (HOM-SET PAIRS DOMAIN P Q)))))))

; Here, HOM-SET can be thought of as a Skolem function which picks
; out the desired homogeneous subset of the given DOMAIN, i.e.
; homogeneous with respect to the relation PAIRS (presented as a
; list of ordered pairs).  Notice that if DOMAIN has no repetitions
; (which is a harmless assumption for the statement of Ramsey's
; Theorem), then LENGTH is just cardinality.  The function LEQ is
; just "less than or equal", at least on the natural numbers.
; (HOMOGENEOUS S PAIRS 1) is true, i.e. equals T, if the list
; S is homogeous with respect to PAIRS in the positive sense,
; i.e., in that each pair from S is related by PAIRS (i.e. either
; the pair or its reverse belongs to PAIRS).  Similary,
; (HOMOGENEOUS S PAIRS 2) is true if no pair from S belongs to
; PAIRS (in the same sense).  RAMSEY is a function which returns
; an integer which (according to the theorem above) is "large
; enough".  However, at the end of this note we prove that
; (RAMSEY P Q) = (CHOOSE (PLUS P Q) P), where (CHOOSE M N) is
; the binomial coefficient (defined though with integer division).

; The description above completes the discussion of the theorem,
; but to read on it helps to realize that we don't define HOM-SET
; until near the end of this note.  Instead, we define a function
; WIT which returns a pair, so that HOM-SET merely returns the CAR
; of this pair.  The CDR of the value of WIT is the "color", which
; is 1 or 2 (as is proved in a lemma below).  It's really best to
; think of WIT as a Skolem function, though in fact it is defined
; to make the theorem true.

\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{verbatim};this is a hint to get the
				;definition accepted

\end{verbatim}\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 }{\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}\-\-
\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 Theorem}:  length-of-partitions \\ \index{length-of-partitions}
\=\+{\rm{length}}\,({\rm{cons}}\,({\it{n\/}}, {\it{domain\/}}))\index{length} \\ 
$=$$\;\;\;\;$($1\;+$ (\=\+{\rm{length}}\,({\rm{car}}\,({\rm{partition}}\,({\it{n\/}}, {\it{domain\/}}, {\it{pairs\/}})\index{partition}))\index{length} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\rm{cdr}}\,({\rm{partition}}\,({\it{n\/}}, {\it{domain\/}}, {\it{pairs\/}})\index{partition}))\index{length})\-)\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-length-ramsey-2 \\ \index{lessp-length-ramsey-2}
\=\+(\=\+{\rm{listp}}\,({\it{domain\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$(({\it{i\/}} $+$ {\it{j\/}}) $\leq$ {\rm{length}}\,({\it{domain\/}})\index{length}) \\ 
$\wedge$$\;\;\;\;$({\rm{length}}\,({\rm{car}}\,({\rm{partition}}\,({\rm{car}}\,({\it{domain\/}}), {\rm{cdr}}\,({\it{domain\/}}), {\it{pairs\/}})\index{partition}))\index{length} $<$ {\it{i\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$(({\rm{length}}\,({\rm{cdr}}\,({\rm{partition}}\,({\rm{car}}\,({\it{domain\/}}), {\rm{cdr}}\,({\it{domain\/}}), {\it{pairs\/}})\index{partition}))\index{length} $<$ {\it{j\/}}) $=$ {\bf{f}})\-
\end{tabbing}

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


\noindent{\sc Event}:   Disable lessp-length-ramsey-2.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  lessp-length-ramsey \\ \index{lessp-length-ramsey}
\=\+(\=\+({\it{p\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\it{q\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\rm{ramsey}}\,({\it{p\/}}, {\it{q\/}})\index{ramsey} $\leq$ {\rm{length}}\,({\it{domain\/}})\index{length}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\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})\-)\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+{\rm{length}}\,({\rm{cdr}}\,({\rm{partition}}\,({\rm{car}}\,({\it{domain\/}}), {\rm{cdr}}\,({\it{domain\/}}), {\it{pairs\/}})\index{partition}))\index{length} \\ 
$<$$\;\;\;\;${\rm{ramsey}}\,({\it{p\/}}, {\it{q\/}} $-\;1$)\index{ramsey})\- \\ 
$=$$\;\;\;\;${\bf{f}})\-\-
\end{tabbing}

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

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

\begin{tabbing}{\sc Theorem}:  homogeneous1-partition-car \\ \index{homogeneous1-partition-car}
{\rm{homogeneous1}}\,({\it{a\/}}, {\rm{car}}\,({\rm{partition}}\,({\it{a\/}}, {\it{domain\/}}, {\it{pairs\/}})\index{partition}), {\it{pairs\/}}, {\tt{1}})\index{homogeneous1}
\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}:  subsetp-preserves-homogeneous1 \\ \index{subsetp-preserves-homogeneous1}
\=\+({\rm{subsetp}}\,({\it{l\/}}, {\it{m\/}})\index{subsetp} $\wedge$ {\rm{homogeneous1}}\,({\it{a\/}}, {\it{m\/}}, {\it{pairs\/}}, {\it{flg\/}})\index{homogeneous1}) \\ 
$\rightarrow$$\;\;\;\;${\rm{homogeneous1}}\,({\it{a\/}}, {\it{l\/}}, {\it{pairs\/}}, {\it{flg\/}})\index{homogeneous1}\-
\end{tabbing}

\begin{verbatim}; The following lemmas, till further notice, are simply
; lemmas about sets, some of which may be needed below.

\end{verbatim}\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{verbatim}; end of silly subset lemmas

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

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

\begin{tabbing}{\sc Theorem}:  witness-subsetp \\ \index{witness-subsetp}
\=\+({\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}\-
\end{tabbing}

\begin{verbatim}; Here are the commands to generate proofs of four of
; the six induction steps in the theorem.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  ramsey-thm-2-goals-1-2-3-5 \\ \index{ramsey-thm-2-goals-1-2-3-5}
{\bf{t}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-but-goal-4 \\ \index{all-but-goal-4}
{\bf{t}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ramsey-thm-2-except-length \\ \index{ramsey-thm-2-except-length}
\=\+({\rm{ramsey}}\,({\it{p\/}}, {\it{q\/}})\index{ramsey} $\leq$ {\rm{length}}\,({\it{domain\/}})\index{length}) \\ 
$\rightarrow$$\;\;\;\;${\rm{homogeneous}}\,(\=\+{\rm{car}}\,({\rm{wit}}\,({\it{pairs\/}}, {\it{domain\/}}, {\it{p\/}}, {\it{q\/}})\index{wit}), \\ 
{\it{pairs\/}}, \\ 
{\rm{cdr}}\,({\rm{wit}}\,({\it{pairs\/}}, {\it{domain\/}}, {\it{p\/}}, {\it{q\/}})\index{wit}))\-\index{homogeneous}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ramsey-thm-2-length \\ \index{ramsey-thm-2-length}
\=\+({\rm{ramsey}}\,({\it{p\/}}, {\it{q\/}})\index{ramsey} $\leq$ {\rm{length}}\,({\it{domain\/}})\index{length}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+{\rm{length}}\,({\rm{car}}\,({\rm{wit}}\,({\it{pairs\/}}, {\it{domain\/}}, {\it{p\/}}, {\it{q\/}})\index{wit}))\index{length} \\ 
$<$$\;\;\;\;$\=\+{\bf if }{\rm{cdr}}\,({\rm{wit}}\,({\it{pairs\/}}, {\it{domain\/}}, {\it{p\/}}, {\it{q\/}})\index{wit}) $=$ {\tt{1}}$\;\;${\bf then }{\it{p\/}} \\ 
{\bf else }{\it{q\/}}$\;${\bf  endif}\-)\- \\ 
$=$$\;\;\;\;${\bf{f}})\-\-
\end{tabbing}

\begin{verbatim}; Finally, the main theorem's proof is concluded:

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

\begin{tabbing}{\sc Theorem}:  ramsey-thm-2 \\ \index{ramsey-thm-2}
\=\+({\rm{ramsey}}\,({\it{p\/}}, {\it{q\/}})\index{ramsey} $\leq$ {\rm{length}}\,({\it{domain\/}})\index{length}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{subsetp}}\,({\rm{hom-set}}\,({\it{pairs\/}}, {\it{domain\/}}, {\it{p\/}}, {\it{q\/}})\index{hom-set}, {\it{domain\/}})\index{subsetp} \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+{\rm{homogeneous}}\,({\rm{hom-set}}\,({\it{pairs\/}}, {\it{domain\/}}, {\it{p\/}}, {\it{q\/}})\index{hom-set}, {\it{pairs\/}}, {\tt{1}})\index{homogeneous} \\ 
$\wedge$$\;\;\;\;$({\it{p\/}} $\leq$ {\rm{length}}\,({\rm{hom-set}}\,({\it{pairs\/}}, {\it{domain\/}}, {\it{p\/}}, {\it{q\/}})\index{hom-set})\index{length}))\- \\ 
$\vee$$\;\;\;\;$(\=\+{\rm{homogeneous}}\,({\rm{hom-set}}\,({\it{pairs\/}}, {\it{domain\/}}, {\it{p\/}}, {\it{q\/}})\index{hom-set}, {\it{pairs\/}}, {\tt{2}})\index{homogeneous} \\ 
$\wedge$$\;\;\;\;$({\it{q\/}} $\leq$ {\rm{length}}\,({\rm{hom-set}}\,({\it{pairs\/}}, {\it{domain\/}}, {\it{p\/}}, {\it{q\/}})\index{hom-set})\index{length}))\-)\-)\-\-
\end{tabbing}

\begin{verbatim};;; The following were aded 4/22/88 to show that in fact, under the
;;; hypotheses of the theorem above, the HOM-SET has no duplicates
;;; (and hence LENGTH really does measure cardinality, though I don't
;;; formalize or prove this parenthetical remark).

\end{verbatim}\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}:  set-partition \\ \index{set-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}:  member-partition \\ \index{member-partition}
\=\+({\it{a\/}} $\not\in$ {\it{x\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\it{a\/}} $\not\in$ {\rm{car}}\,({\rm{partition}}\,({\it{b\/}}, {\it{x\/}}, {\it{pairs\/}})\index{partition})) \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $\not\in$ {\rm{cdr}}\,({\rm{partition}}\,({\it{b\/}}, {\it{x\/}}, {\it{pairs\/}})\index{partition})))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member-cons-expand \\ \index{member-cons-expand}
\=\+({\it{a\/}} $\in$ {\rm{cons}}\,({\it{b\/}}, {\it{y\/}})) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{a\/}} $=$ {\it{b\/}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\it{a\/}} $\in$ {\it{y\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  setp-cons-expand \\ \index{setp-cons-expand}
\=\+{\rm{setp}}\,({\rm{cons}}\,({\it{b\/}}, {\it{y\/}}))\index{setp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{b\/}} $\in$ {\it{y\/}}$\;\;${\bf then }{\bf{f}} \\ 
{\bf else }{\rm{setp}}\,({\it{y\/}})\index{setp}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member-hom-set-implies-member-domain \\ \index{member-hom-set-implies-member-d!omain}
\=\+(({\rm{length}}\,({\it{domain\/}})\index{length} $\not<$ {\rm{ramsey}}\,({\it{p\/}}, {\it{q\/}})\index{ramsey}) $\wedge$ ({\it{a\/}} $\not\in$ {\it{domain\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\it{a\/}} $\not\in$ {\rm{car}}\,({\rm{wit}}\,({\it{pairs\/}}, {\it{domain\/}}, {\it{p\/}}, {\it{q\/}})\index{wit}))\-
\end{tabbing}

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

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