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

;; Matt Kaufmann

;; Ramsey Theorem (infinite version) events supporting ``An Extension
;; of the Boyer-Moore Theorem Prover to Support First-Order
;; Quantification,'' to appear in JAR (1992?).  The DEFN-SK events
;; have been replaced by DCLs and ADD-AXIOMs, as shown.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Ramsey Theorem Events List
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

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

\addvspace{18pt}

\begin{tabbing}{\sc Conservative Axiom}:  p-num-intro \\ \index{p-num-intro}
\=\+(({\it{x\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{y\/}} $\in\;${\bf{N}}${}$)) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\tt{0}} $<$ {\rm{p-num}}\,({\it{x\/}}, {\it{y\/}})\index{p-num}) \\ 
$\wedge$$\;\;\;\;$({\sc{bound}}\index{bound} $\not<$ {\rm{p-num}}\,({\it{x\/}}, {\it{y\/}})\index{p-num}) \\ 
$\wedge$$\;\;\;\;$({\rm{p-num}}\,({\it{x\/}}, {\it{y\/}})\index{p-num} $=$ {\rm{p-num}}\,({\it{y\/}}, {\it{x\/}})\index{p-num}))\-\-
\end{tabbing}\noindent Simultaneously, we introduce the new function symbols {\it p-num\/} and {\it bound\/}.


\noindent{\sc Event}:   Disable p-num-intro.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{p}$\;\;$
{\rm{p}}\,({\it{x\/}}, {\it{y\/}})\index{p} $=$ {\rm{p-num}}\,({\rm{fix}}\,({\it{x\/}}), {\rm{fix}}\,({\it{y\/}}))\index{p-num}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  p-intro \\ \index{p-intro}
({\tt{0}} $<$ {\rm{p}}\,({\it{x\/}}, {\it{y\/}})\index{p}) $\wedge$ ({\sc{bound}}\index{bound} $\not<$ {\rm{p}}\,({\it{x\/}}, {\it{y\/}})\index{p}) $\wedge$ ({\rm{p}}\,({\it{x\/}}, {\it{y\/}})\index{p} $=$ {\rm{p}}\,({\it{y\/}}, {\it{x\/}})\index{p})
\end{tabbing}


\noindent{\sc Event}:   Disable p.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{prehom-seq-1} \\  
\=\+{\rm{prehom-seq-1}}\,({\it{a\/}}, {\it{x\/}})\index{prehom-seq-1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}}) \\ 
{\bf then }({\rm{p}}\,({\rm{caar}}\,({\it{x\/}}), {\it{a\/}})\index{p} $=$ {\rm{cdar}}\,({\it{x\/}})) $\wedge$ {\rm{prehom-seq-1}}\,({\it{a\/}}, {\rm{cdr}}\,({\it{x\/}}))\index{prehom-seq-1} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{prehom-seq} \\  
\=\+{\rm{prehom-seq}}\,({\it{x\/}})\index{prehom-seq} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{listp}}\,({\rm{cdr}}\,({\it{x\/}})) \\ 
{\bf then }\=\+({\rm{car}}\,({\rm{cadr}}\,({\it{x\/}})) $<$ {\rm{car}}\,({\rm{car}}\,({\it{x\/}}))) \\ 
$\wedge$$\;\;\;\;${\rm{prehom-seq-1}}\,({\rm{caar}}\,({\it{x\/}}), {\rm{cdr}}\,({\it{x\/}}))\index{prehom-seq-1} \\ 
$\wedge$$\;\;\;\;${\rm{prehom-seq}}\,({\rm{cdr}}\,({\it{x\/}}))\index{prehom-seq}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}#| The original DEFN-SK event here was processed as follows:

>(defn-sk extensible (s)
  ;; s is a list of pairs (i . c), and extensible means that there
  ;; are infinitely many a for which prehom-seq-1(a,s) holds.
  (forall above
          (exists next
                  (and (lessp above next)
                       (prehom-seq-1 next s)))))


Adding the Skolem axiom:
      (AND (IMPLIES (AND (LESSP (ABOVE S) NEXT)
                         (PREHOM-SEQ-1 NEXT S))
                    (EXTENSIBLE S))
           (IMPLIES (NOT (AND (LESSP ABOVE (NEXT ABOVE S))
                              (PREHOM-SEQ-1 (NEXT ABOVE S) S)))
                    (NOT (EXTENSIBLE S)))).


     As this is a DEFN-SK we can conclude that:
      (OR (TRUEP (EXTENSIBLE S))
          (FALSEP (EXTENSIBLE S)))
is a theorem.


[ 0.3 0.0 0.0 ]
EXTENSIBLE

>

|#

\end{verbatim}
\noindent{\sc Event}:   Introduce the function symbol {\it above\index{above}\/} of one argument.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it next\index{next}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it extensible\index{extensible}\/} of one argument.

\addvspace{18pt}

\begin{tabbing}{\sc Axiom}:  extensible-intro \\ \index{extensible-intro}
\=\+((({\rm{above}}\,({\it{s\/}})\index{above} $<$ {\it{next\/}}) $\wedge$ {\rm{prehom-seq-1}}\,({\it{next\/}}, {\it{s\/}})\index{prehom-seq-1}) $\rightarrow$ {\rm{extensible}}\,({\it{s\/}})\index{extensible}) \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ (({\it{above\/}} $<$ {\rm{next}}\,({\it{above\/}}, {\it{s\/}})\index{next}) $\wedge$ {\rm{prehom-seq-1}}\,({\rm{next}}\,({\it{above\/}}, {\it{s\/}})\index{next}, {\it{s\/}})\index{prehom-seq-1})) \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{extensible}}\,({\it{s\/}})\index{extensible}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Axiom}:  extensible-boolean \\ \index{extensible-boolean}
{\rm{truep}}\,({\rm{extensible}}\,({\it{s\/}})\index{extensible}) $\vee$ {\rm{falsep}}\,({\rm{extensible}}\,({\it{s\/}})\index{extensible})
\end{tabbing}

\begin{verbatim};; The following two lemmas are for the benefit of the proof-checker
;; macro-command SK*.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  extensible-suff \\ \index{extensible-suff}
(({\rm{above}}\,({\it{s\/}})\index{above} $<$ {\it{next\/}}) $\wedge$ {\rm{prehom-seq-1}}\,({\it{next\/}}, {\it{s\/}})\index{prehom-seq-1}) $\rightarrow$ {\rm{extensible}}\,({\it{s\/}})\index{extensible}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  extensible-necc \\ \index{extensible-necc}
\=\+($\neg$ (({\it{above\/}} $<$ {\rm{next}}\,({\it{above\/}}, {\it{s\/}})\index{next}) $\wedge$ {\rm{prehom-seq-1}}\,({\rm{next}}\,({\it{above\/}}, {\it{s\/}})\index{next}, {\it{s\/}})\index{prehom-seq-1})) \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{extensible}}\,({\it{s\/}})\index{extensible})\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{above-all-aux} \\  
\=\+{\rm{above-all-aux}}\,({\it{a\/}}, {\it{s\/}}, {\it{n\/}})\index{above-all-aux} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\rm{above}}\,({\rm{cons}}\,({\rm{cons}}\,({\it{a\/}}, {\it{n\/}}), {\it{s\/}}))\index{above} $+$ {\rm{above-all-aux}}\,({\it{a\/}}, {\it{s\/}}, {\it{n\/}} $-\;1$)\index{above-all-aux}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{above-all}$\;\;$
{\rm{above-all}}\,({\it{a\/}}, {\it{s\/}})\index{above-all} $=$ {\rm{above-all-aux}}\,({\it{a\/}}, {\it{s\/}}, {\sc{bound}}\index{bound})\index{above-all-aux}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-above-all-aux \\ \index{lessp-above-all-aux}
({\tt{0}} $<$ {\it{n\/}}) $\rightarrow$ ({\rm{above-all-aux}}\,({\it{a\/}}, {\it{s\/}}, {\it{n\/}})\index{above-all-aux} $\not<$ {\rm{above}}\,({\rm{cons}}\,({\rm{cons}}\,({\it{a\/}}, {\it{n\/}}), {\it{s\/}}))\index{above})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  above-all-aux-monotone \\ \index{above-all-aux-monotone}
({\it{bound\/}} $\not<$ {\it{n\/}}) $\rightarrow$ ({\rm{above-all-aux}}\,({\it{a\/}}, {\it{s\/}}, {\it{bound\/}})\index{above-all-aux} $\not<$ {\rm{above-all-aux}}\,({\it{a\/}}, {\it{s\/}}, {\it{n\/}})\index{above-all-aux})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-above-all-bound \\ \index{lessp-above-all-bound}
\=\+(({\tt{0}} $<$ {\it{n\/}}) $\wedge$ ({\sc{bound}}\index{bound} $\not<$ {\it{n\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{above-all}}\,({\it{a\/}}, {\it{s\/}})\index{above-all} $\not<$ {\rm{above}}\,({\rm{cons}}\,({\rm{cons}}\,({\it{a\/}}, {\it{n\/}}), {\it{s\/}}))\index{above})\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{next-element}$\;\;$
{\rm{next-element}}\,({\it{a\/}}, {\it{s\/}})\index{next-element} $=$ {\rm{next}}\,({\rm{above-all}}\,({\it{a\/}}, {\it{s\/}})\index{above-all}, {\it{s\/}})\index{next}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{next-color}$\;\;$
{\rm{next-color}}\,({\it{a\/}}, {\it{s\/}})\index{next-color} $=$ {\rm{p}}\,({\it{a\/}}, {\rm{next-element}}\,({\it{a\/}}, {\it{s\/}})\index{next-element})\index{p}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  numberp-p \\ \index{numberp-p}
{\rm{p}}\,({\it{x\/}}, {\it{y\/}})\index{p} $\in\;${\bf{N}}${}$
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  next-color-bound \\ \index{next-color-bound}
({\tt{0}} $<$ {\rm{next-color}}\,({\it{a\/}}, {\it{s\/}})\index{next-color}) $\wedge$ ({\sc{bound}}\index{bound} $\not<$ {\rm{next-color}}\,({\it{a\/}}, {\it{s\/}})\index{next-color})
\end{tabbing}


\noindent{\sc Event}:   Disable above-all.

\addvspace{18pt}

\begin{verbatim};; first of two goals for extensible-cons
\end{verbatim}\begin{tabbing}{\sc Theorem}:  lessp-next-element \\ \index{lessp-next-element}
\=\+{\rm{extensible}}\,({\it{s\/}})\index{extensible} \\ 
$\rightarrow$$\;\;\;\;$({\rm{above}}\,({\rm{cons}}\,({\rm{cons}}\,({\it{a\/}}, {\rm{next-color}}\,({\it{a\/}}, {\it{s\/}})\index{next-color}), {\it{s\/}}))\index{above} $<$ {\rm{next-element}}\,({\it{a\/}}, {\it{s\/}})\index{next-element})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  prehom-seq-1-next-element \\ \index{prehom-seq-1-next-element}
{\rm{extensible}}\,({\it{s\/}})\index{extensible} $\rightarrow$ {\rm{prehom-seq-1}}\,({\rm{next-element}}\,({\it{a\/}}, {\it{s\/}})\index{next-element}, {\it{s\/}})\index{prehom-seq-1}
\end{tabbing}


\noindent{\sc Event}:   Disable next-element.

\addvspace{18pt}

\begin{verbatim};; second of two goals for extensible-cons
\end{verbatim}\begin{tabbing}{\sc Theorem}:  prehom-seq-1-next-element-cons \\ \index{prehom-seq-1-next-element-cons}
\=\+{\rm{extensible}}\,({\it{s\/}})\index{extensible} \\ 
$\rightarrow$$\;\;\;\;${\rm{prehom-seq-1}}\,({\rm{next-element}}\,({\it{a\/}}, {\it{s\/}})\index{next-element}, {\rm{cons}}\,({\rm{cons}}\,({\it{a\/}}, {\rm{next-color}}\,({\it{a\/}}, {\it{s\/}})\index{next-color}), {\it{s\/}}))\index{prehom-seq-1}\-
\end{tabbing}


\noindent{\sc Event}:   Disable next-color.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  extensible-cons \\ \index{extensible-cons}
{\rm{extensible}}\,({\it{s\/}})\index{extensible} $\rightarrow$ {\rm{extensible}}\,({\rm{cons}}\,({\rm{cons}}\,({\it{a\/}}, {\rm{next-color}}\,({\it{a\/}}, {\it{s\/}})\index{next-color}), {\it{s\/}}))\index{extensible}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{next-pair} \\  
{\rm{next-pair}}\,({\it{s\/}})\index{next-pair} $=$ {\rm{cons}}\,({\rm{next}}\,({\rm{caar}}\,({\it{s\/}}), {\it{s\/}})\index{next}, {\rm{next-color}}\,({\rm{next}}\,({\rm{caar}}\,({\it{s\/}}), {\it{s\/}})\index{next}, {\it{s\/}})\index{next-color})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  next-pair-extends \\ \index{next-pair-extends}
{\rm{extensible}}\,({\it{s\/}})\index{extensible} $\rightarrow$ {\rm{extensible}}\,({\rm{cons}}\,({\rm{next-pair}}\,({\it{s\/}})\index{next-pair}, {\it{s\/}}))\index{extensible}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{ramsey-seq-p}$\;\;$
{\rm{ramsey-seq-p}}\,({\it{s\/}})\index{ramsey-seq-p} $=$ ({\rm{extensible}}\,({\it{s\/}})\index{extensible} $\wedge$ {\rm{prehom-seq}}\,({\it{s\/}})\index{prehom-seq})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  extensible-next-property \\ \index{extensible-next-property}
{\rm{extensible}}\,({\it{s\/}})\index{extensible} $\rightarrow$ (({\it{a\/}} $<$ {\rm{next}}\,({\it{a\/}}, {\it{s\/}})\index{next}) $\wedge$ {\rm{prehom-seq-1}}\,({\rm{next}}\,({\it{a\/}}, {\it{s\/}})\index{next}, {\it{s\/}})\index{prehom-seq-1})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ramsey-seq-p-extends \\ \index{ramsey-seq-p-extends}
{\rm{ramsey-seq-p}}\,({\it{s\/}})\index{ramsey-seq-p} $\rightarrow$ {\rm{ramsey-seq-p}}\,({\rm{cons}}\,({\rm{next-pair}}\,({\it{s\/}})\index{next-pair}, {\it{s\/}}))\index{ramsey-seq-p}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  extensible-nlistp \\ \index{extensible-nlistp}
($\neg$ {\rm{listp}}\,({\it{s\/}})) $\rightarrow$ {\rm{extensible}}\,({\it{s\/}})\index{extensible}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ramsey-seq-p-nlistp \\ \index{ramsey-seq-p-nlistp}
({\it{s\/}} $\simeq\;${{\bf{nil}}}${}$) $\rightarrow$ {\rm{ramsey-seq-p}}\,({\it{s\/}})\index{ramsey-seq-p}
\end{tabbing}


\noindent{\sc Event}:   Disable ramsey-seq-p.

\addvspace{18pt}


\noindent{\sc Event}:   Disable next-pair.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{ramsey-seq} \\  
\=\+{\rm{ramsey-seq}}\,({\it{n\/}})\index{ramsey-seq} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{cons}}\,({\rm{next-pair}}\,({\rm{ramsey-seq}}\,({\it{n\/}} $-\;1$)\index{ramsey-seq})\index{next-pair}, {\rm{ramsey-seq}}\,({\it{n\/}} $-\;1$)\index{ramsey-seq})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ramsey-seq-has-ramsey-seq-p \\ \index{ramsey-seq-has-ramsey-seq-p}
{\rm{ramsey-seq-p}}\,({\rm{ramsey-seq}}\,({\it{n\/}})\index{ramsey-seq})\index{ramsey-seq-p}
\end{tabbing}

\begin{verbatim};; Now we want to cut down this prehomogenous sequence to one that's
;; homogeneous.  First let's define the flag.

#| The original DEFN-SK event here was processed as follows:

>(defn-sk good-color-p (c)
  ;; says that arbitrarily large elements of ramsey-seq agree with c
  (forall big
          (exists good-c-index
                  (and (lessp big good-c-index)
                       (equal c (cdr (car (ramsey-seq good-c-index))))))))


Adding the Skolem axiom:
      (AND
          (IMPLIES (AND (LESSP (BIG C) GOOD-C-INDEX)
                        (EQUAL C
                               (CDAR (RAMSEY-SEQ GOOD-C-INDEX))))
                   (GOOD-COLOR-P C))
          (IMPLIES (NOT (AND (LESSP BIG (GOOD-C-INDEX BIG C))
                             (EQUAL C
                                    (CDAR (RAMSEY-SEQ (GOOD-C-INDEX BIG C))))))
                   (NOT (GOOD-COLOR-P C)))).


     As this is a DEFN-SK we can conclude that:
      (OR (TRUEP (GOOD-COLOR-P C))
          (FALSEP (GOOD-COLOR-P C)))
is a theorem.


[ 0.2 0.0 0.0 ]
GOOD-COLOR-P

>

|#

\end{verbatim}
\noindent{\sc Event}:   Introduce the function symbol {\it big\index{big}\/} of one argument.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it good-c-index\index{good-c-index}\/} of 2 arguments.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it good-color-p\index{good-color-p}\/} of one argument.

\addvspace{18pt}

\begin{tabbing}{\sc Axiom}:  good-color-p-intro \\ \index{good-color-p-intro}
\=\+(\=\+(({\rm{big}}\,({\it{c\/}})\index{big} $<$ {\it{good-c-index\/}}) $\wedge$ ({\it{c\/}} $=$ {\rm{cdar}}\,({\rm{ramsey-seq}}\,({\it{good-c-index\/}})\index{ramsey-seq}))) \\ 
$\rightarrow$$\;\;\;\;${\rm{good-color-p}}\,({\it{c\/}})\index{good-color-p})\- \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ (\=\+({\it{big\/}} $<$ {\rm{good-c-index}}\,({\it{big\/}}, {\it{c\/}})\index{good-c-index}) \\ 
$\wedge$$\;\;\;\;$({\it{c\/}} $=$ {\rm{cdar}}\,({\rm{ramsey-seq}}\,({\rm{good-c-index}}\,({\it{big\/}}, {\it{c\/}})\index{good-c-index})\index{ramsey-seq})))\-) \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{good-color-p}}\,({\it{c\/}})\index{good-color-p}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Axiom}:  good-color-p-boolean \\ \index{good-color-p-boolean}
{\rm{truep}}\,({\rm{good-color-p}}\,({\it{c\/}})\index{good-color-p}) $\vee$ {\rm{falsep}}\,({\rm{good-color-p}}\,({\it{c\/}})\index{good-color-p})
\end{tabbing}

\begin{verbatim};; The following two lemmas are for the benefit of the proof-checker
;; macro-command SK*.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  good-color-p-suff \\ \index{good-color-p-suff}
\=\+(({\rm{big}}\,({\it{c\/}})\index{big} $<$ {\it{good-c-index\/}}) $\wedge$ ({\it{c\/}} $=$ {\rm{cdar}}\,({\rm{ramsey-seq}}\,({\it{good-c-index\/}})\index{ramsey-seq}))) \\ 
$\rightarrow$$\;\;\;\;${\rm{good-color-p}}\,({\it{c\/}})\index{good-color-p}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  good-color-p-necc \\ \index{good-color-p-necc}
\=\+($\neg$ (\=\+({\it{big\/}} $<$ {\rm{good-c-index}}\,({\it{big\/}}, {\it{c\/}})\index{good-c-index}) \\ 
$\wedge$$\;\;\;\;$({\it{c\/}} $=$ {\rm{cdar}}\,({\rm{ramsey-seq}}\,({\rm{good-c-index}}\,({\it{big\/}}, {\it{c\/}})\index{good-c-index})\index{ramsey-seq})))\-) \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{good-color-p}}\,({\it{c\/}})\index{good-color-p})\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{good-c-index-wit} \\  
\=\+{\rm{good-c-index-wit}}\,({\it{bound\/}})\index{good-c-index-wit} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{bound\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\rm{big}}\,({\it{bound\/}})\index{big} $+$ {\rm{good-c-index-wit}}\,({\it{bound\/}} $-\;1$)\index{good-c-index-wit}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  good-c-index-wit-positive \\ \index{good-c-index-wit-positive}
{\tt{0}} $<$ {\rm{good-c-index-wit}}\,({\it{bound\/}})\index{good-c-index-wit}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-big-good-c-index \\ \index{lessp-big-good-c-index}
\=\+(({\tt{0}} $<$ {\it{c\/}}) $\wedge$ ({\it{bound\/}} $\not<$ {\it{c\/}})) \\ 
$\rightarrow$$\;\;\;\;$(({\rm{big}}\,({\it{c\/}})\index{big} $<$ {\rm{good-c-index-wit}}\,({\it{bound\/}})\index{good-c-index-wit}) $=$ {\bf{t}})\-
\end{tabbing}


\noindent{\sc Event}:   Disable good-c-index-wit.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{color}$\;\;$
{\sc{color}}\index{color} $=$ {\rm{cdar}}\,({\rm{ramsey-seq}}\,({\rm{good-c-index-wit}}\,({\sc{bound}}\index{bound})\index{good-c-index-wit})\index{ramsey-seq})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ramsey-seq-has-colors-in-bounds \\ \index{ramsey-seq-has-colors-in-bounds}
\=\+({\tt{0}} $<$ {\it{n\/}}) \\ 
$\rightarrow$$\;\;\;\;$(({\tt{0}} $<$ {\rm{cdar}}\,({\rm{ramsey-seq}}\,({\it{n\/}})\index{ramsey-seq})) $\wedge$ ({\sc{bound}}\index{bound} $\not<$ {\rm{cdar}}\,({\rm{ramsey-seq}}\,({\it{n\/}})\index{ramsey-seq})))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  color-in-bounds \\ \index{color-in-bounds}
({\tt{0}} $<$ {\sc{color}}\index{color}) $\wedge$ ({\sc{bound}}\index{bound} $\not<$ {\sc{color}}\index{color})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  color-is-good \\ \index{color-is-good}
{\rm{good-color-p}}\,({\sc{color}}\index{color})\index{good-color-p}
\end{tabbing}


\noindent{\sc Event}:   Disable color.

\addvspace{18pt}

\noindent{\sc Event}:   Disable *1*color.

\addvspace{18pt}

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

\begin{tabbing}{\sc Theorem}:  color-properties \\ \index{color-properties}
\=\+({\it{big\/}} $<$ {\rm{good-c-index}}\,({\it{big\/}}, {\sc{color}}\index{color})\index{good-c-index}) \\ 
$\wedge$$\;\;\;\;$({\rm{cdr}}\,({\rm{car}}\,({\rm{ramsey-seq}}\,({\rm{good-c-index}}\,({\it{big\/}}, {\sc{color}}\index{color})\index{good-c-index})\index{ramsey-seq})) $=$ {\sc{color}}\index{color})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ramsey-index-increasing \\ \index{ramsey-index-increasing}
({\it{i\/}} $<$ {\it{j\/}}) $\rightarrow$ ({\rm{ramsey-index}}\,({\it{i\/}})\index{ramsey-index} $<$ {\rm{ramsey-index}}\,({\it{j\/}})\index{ramsey-index})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{ramsey}$\;\;$
{\rm{ramsey}}\,({\it{n\/}})\index{ramsey} $=$ {\rm{car}}\,({\rm{car}}\,({\rm{ramsey-seq}}\,({\rm{ramsey-index}}\,({\it{n\/}})\index{ramsey-index})\index{ramsey-seq}))
\end{tabbing}

\begin{verbatim}; Next goal:
;(prove-lemma ramsey-increasing (rewrite)
;  (implies (lessp i j)
;           (lessp (ramsey i) (ramsey j))))

\end{verbatim}\begin{tabbing}{\sc Theorem}:  good-c-index-numberp \\ \index{good-c-index-numberp}
{\rm{good-c-index}}\,({\it{big\/}}, {\sc{color}}\index{color})\index{good-c-index} $\in\;${\bf{N}}${}$
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ramsey-index-numberp \\ \index{ramsey-index-numberp}
{\rm{ramsey-index}}\,({\it{n\/}})\index{ramsey-index} $\in\;${\bf{N}}${}$
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  car-next-pair \\ \index{car-next-pair}
{\rm{car}}\,({\rm{next-pair}}\,({\it{s\/}})\index{next-pair}) $=$ {\rm{next}}\,({\rm{caar}}\,({\it{s\/}}), {\it{s\/}})\index{next}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ramsey-seq-extensible \\ \index{ramsey-seq-extensible}
{\rm{extensible}}\,({\rm{ramsey-seq}}\,({\it{n\/}})\index{ramsey-seq})\index{extensible}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  next-not-zerop \\ \index{next-not-zerop}
{\rm{extensible}}\,({\it{s\/}})\index{extensible} $\rightarrow$ (({\rm{next}}\,({\it{a\/}}, {\it{s\/}})\index{next} $\in\;${\bf{N}}${}$) $\wedge$ ({\rm{next}}\,({\it{a\/}}, {\it{s\/}})\index{next} $\not=$ {\tt{0}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ramsey-seq-increasing \\ \index{ramsey-seq-increasing}
({\it{i\/}} $<$ {\it{j\/}}) $\rightarrow$ (({\rm{caar}}\,({\rm{ramsey-seq}}\,({\it{i\/}})\index{ramsey-seq}) $<$ {\rm{caar}}\,({\rm{ramsey-seq}}\,({\it{j\/}})\index{ramsey-seq})) $=$ {\bf{t}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ramsey-index-increasing-rewrite \\ \index{ramsey-index-increasing-rewrite}
({\it{i\/}} $<$ {\it{j\/}}) $\rightarrow$ (({\rm{ramsey-index}}\,({\it{i\/}})\index{ramsey-index} $<$ {\rm{ramsey-index}}\,({\it{j\/}})\index{ramsey-index}) $=$ {\bf{t}})
\end{tabbing}


\noindent{\sc Event}:   Disable ramsey-index-increasing.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  ramsey-increasing \\ \index{ramsey-increasing}
({\it{i\/}} $<$ {\it{j\/}}) $\rightarrow$ ({\rm{ramsey}}\,({\it{i\/}})\index{ramsey} $<$ {\rm{ramsey}}\,({\it{j\/}})\index{ramsey})
\end{tabbing}

\begin{verbatim};; Now we want to show that ramsey is homogeneous for (color):

;(prove-lemma ramsey-homogeneous (rewrite)
;  (implies (lessp i j)
;           (iff (p (ramsey i) (ramsey j))
;                (color))))

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

\begin{verbatim};; We've already proved (ramsey-seq-p (ramseq-seq i)).  So, in order
;; to prove the key lemma ramsey-seq-prehom below, we'll use this
;; together with an appropriate fact about restn and prehom seqs.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  ramsey-seq-restn-length \\ \index{ramsey-seq-restn-length}
{\rm{restn}}\,({\it{n\/}}, {\rm{ramsey-seq}}\,({\it{n\/}})\index{ramsey-seq})\index{restn} $=$ {\bf{nil}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  prehom-seq-ramsey \\ \index{prehom-seq-ramsey}
{\rm{prehom-seq}}\,({\rm{ramsey-seq}}\,({\it{n\/}})\index{ramsey-seq})\index{prehom-seq}
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  prehom-seq-1-restn \\ \index{prehom-seq-1-restn}
\=\+({\rm{prehom-seq-1}}\,({\it{a\/}}, {\it{s\/}})\index{prehom-seq-1} $\wedge$ ({\it{x\/}} $<$ {\rm{length}}\,({\it{s\/}})\index{length})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{p}}\,({\rm{caar}}\,({\rm{restn}}\,({\it{x\/}}, {\it{s\/}})\index{restn}), {\it{a\/}})\index{p} $=$ {\rm{cdar}}\,({\rm{restn}}\,({\it{x\/}}, {\it{s\/}})\index{restn}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  prehom-seq-restn \\ \index{prehom-seq-restn}
\=\+({\rm{prehom-seq}}\,({\it{s\/}})\index{prehom-seq} $\wedge$ ({\tt{0}} $<$ {\it{x\/}}) $\wedge$ ({\it{x\/}} $<$ {\rm{length}}\,({\it{s\/}})\index{length})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{p}}\,({\rm{caar}}\,({\rm{restn}}\,({\it{x\/}}, {\it{s\/}})\index{restn}), {\rm{caar}}\,({\it{s\/}}))\index{p} $=$ {\rm{cdar}}\,({\rm{restn}}\,({\it{x\/}}, {\it{s\/}})\index{restn}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ramsey-seq-plus \\ \index{ramsey-seq-plus}
{\rm{restn}}\,({\it{x\/}}, {\rm{ramsey-seq}}\,({\it{x\/}} $+$ {\it{y\/}})\index{ramsey-seq})\index{restn} $=$ {\rm{ramsey-seq}}\,({\it{y\/}})\index{ramsey-seq}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  plus-comm \\ \index{plus-comm}
({\it{x\/}} $+$ {\it{y\/}}) $=$ ({\it{y\/}} $+$ {\it{x\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ramsey-seq-plus-commuted \\ \index{ramsey-seq-plus-commuted}
{\rm{restn}}\,({\it{x\/}}, {\rm{ramsey-seq}}\,({\it{y\/}} $+$ {\it{x\/}})\index{ramsey-seq})\index{restn} $=$ {\rm{ramsey-seq}}\,({\it{y\/}})\index{ramsey-seq}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  length-ramsey-seq \\ \index{length-ramsey-seq}
{\rm{length}}\,({\rm{ramsey-seq}}\,({\it{n\/}})\index{ramsey-seq})\index{length} $=$ {\rm{fix}}\,({\it{n\/}})
\end{tabbing}

\begin{verbatim};; The lemmas from here to RAMSEY-SEQ-PREHOM were to eliminate the
;; proof-checker hints from that lemma.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  plus-difference-elim \\ \index{plus-difference-elim}
(({\it{j\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{j\/}} $\not<$ {\it{i\/}})) $\rightarrow$ (({\it{i\/}} $+$ ({\it{j\/}} $-$ {\it{i\/}})) $=$ {\it{j\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  restn-difference-ramsey-seq \\ \index{restn-difference-ramsey-seq}
\=\+(({\tt{0}} $<$ {\it{i\/}}) $\wedge$ ({\it{i\/}} $<$ {\it{j\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{restn}}\,({\it{j\/}} $-$ {\it{i\/}}, {\rm{ramsey-seq}}\,({\it{j\/}})\index{ramsey-seq})\index{restn} $=$ {\rm{ramsey-seq}}\,({\it{i\/}})\index{ramsey-seq})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  prehom-seq-restn-commuted \\ \index{prehom-seq-restn-commuted}
\=\+({\rm{prehom-seq}}\,({\it{s\/}})\index{prehom-seq} $\wedge$ ({\tt{0}} $<$ {\it{x\/}}) $\wedge$ ({\it{x\/}} $<$ {\rm{length}}\,({\it{s\/}})\index{length})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{p}}\,({\rm{caar}}\,({\it{s\/}}), {\rm{caar}}\,({\rm{restn}}\,({\it{x\/}}, {\it{s\/}})\index{restn}))\index{p} $=$ {\rm{cdar}}\,({\rm{restn}}\,({\it{x\/}}, {\it{s\/}})\index{restn}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ramsey-seq-prehom-lemma \\ \index{ramsey-seq-prehom-lemma}
\=\+(({\tt{0}} $<$ {\it{i\/}}) $\wedge$ ({\it{i\/}} $<$ {\it{j\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{p}}\,({\rm{caar}}\,({\rm{restn}}\,({\it{j\/}} $-$ {\it{i\/}}, {\rm{ramsey-seq}}\,({\it{j\/}})\index{ramsey-seq})\index{restn}), {\rm{caar}}\,({\rm{ramsey-seq}}\,({\it{j\/}})\index{ramsey-seq}))\index{p} \\ 
$=$$\;\;\;\;${\rm{cdar}}\,({\rm{restn}}\,({\it{j\/}} $-$ {\it{i\/}}, {\rm{ramsey-seq}}\,({\it{j\/}})\index{ramsey-seq})\index{restn}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ramsey-seq-prehom \\ \index{ramsey-seq-prehom}
\=\+(({\tt{0}} $<$ {\it{i\/}}) $\wedge$ ({\it{i\/}} $<$ {\it{j\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{p}}\,({\rm{caar}}\,({\rm{ramsey-seq}}\,({\it{i\/}})\index{ramsey-seq}), {\rm{caar}}\,({\rm{ramsey-seq}}\,({\it{j\/}})\index{ramsey-seq}))\index{p} $=$ {\rm{cdar}}\,({\rm{ramsey-seq}}\,({\it{i\/}})\index{ramsey-seq}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  cdar-ramseq-seq-ramsey-index \\ \index{cdar-ramseq-seq-ramsey-index}
{\rm{cdar}}\,({\rm{ramsey-seq}}\,({\rm{ramsey-index}}\,({\it{n\/}})\index{ramsey-index})\index{ramsey-seq}) $=$ {\sc{color}}\index{color}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-good-c-index \\ \index{lessp-good-c-index}
({\it{big\/}} $<$ {\rm{good-c-index}}\,({\it{big\/}}, {\sc{color}}\index{color})\index{good-c-index}) $=$ {\bf{t}}
\end{tabbing}


\noindent{\sc Event}:   Disable color-properties.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  good-c-index-non-zero \\ \index{good-c-index-non-zero}
({\tt{0}} $<$ {\rm{good-c-index}}\,({\it{big\/}}, {\sc{color}}\index{color})\index{good-c-index}) $=$ {\bf{t}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ramsey-index-positive \\ \index{ramsey-index-positive}
{\tt{0}} $<$ {\rm{ramsey-index}}\,({\it{n\/}})\index{ramsey-index}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ramsey-seq-hom-lessp \\ \index{ramsey-seq-hom-lessp}
({\it{i\/}} $<$ {\it{j\/}}) $\rightarrow$ ({\rm{p}}\,({\rm{ramsey}}\,({\it{i\/}})\index{ramsey}, {\rm{ramsey}}\,({\it{j\/}})\index{ramsey})\index{p} $=$ {\sc{color}}\index{color})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  p-num-is-p \\ \index{p-num-is-p}
(({\it{x\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{y\/}} $\in\;${\bf{N}}${}$)) $\rightarrow$ ({\rm{p-num}}\,({\it{x\/}}, {\it{y\/}})\index{p-num} $=$ {\rm{p}}\,({\it{x\/}}, {\it{y\/}})\index{p})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  numberp-ramsey \\ \index{numberp-ramsey}
{\rm{caar}}\,({\rm{ramsey-seq}}\,({\rm{ramsey-index}}\,({\it{n\/}})\index{ramsey-index})\index{ramsey-seq}) $\in\;${\bf{N}}${}$
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ramsey-seq-hom \\ \index{ramsey-seq-hom}
\=\+(({\it{i\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{j\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{i\/}} $\not=$ {\it{j\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{p-num}}\,({\rm{ramsey}}\,({\it{i\/}})\index{ramsey}, {\rm{ramsey}}\,({\it{j\/}})\index{ramsey})\index{p-num} $=$ {\sc{color}}\index{color})\-
\end{tabbing}

\begin{verbatim};; The above, together with what was already proved, i.e.

;; (prove-lemma ramsey-increasing (rewrite)
;;  (implies (lessp i j)
;;           (lessp (ramsey i) (ramsey j))))

;; and the fact that p-num was arbitrary (and there are no add-axioms)
;; finishes the job.

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