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

\addvspace{18pt}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                    ;;
;;                       SUBSIDIARY FUNCTIONS                         ;;
;;                                                                    ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; I suspect that many of these lemmas are not necessary but I'm keeping
;; them for now.  I'll eliminate many of them later as I see that they
;; are not needed.

;; I'm adopting the convention that all alist components are cons
;; pairs.  That is, of the form (x . y) not of the form (x y).

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{name}$\;\;$
{\rm{name}}\,({\it{exp\/}})\index{name} $=$ {\rm{car}}\,({\it{exp\/}})
\end{tabbing}


\noindent{\sc Event}:   Disable name.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  name-expansion \\ \index{name-expansion}
{\rm{name}}\,({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}))\index{name} $=$ {\it{x\/}}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{assoc} \\  
\=\+{\rm{assoc}}\,({\it{x\/}}, {\it{y\/}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{y\/}}) \\ 
{\bf then }\=\+{\bf if }{\it{x\/}} $=$ {\rm{caar}}\,({\it{y\/}})$\;\;${\bf then }{\rm{car}}\,({\it{y\/}}) \\ 
{\bf else }{\rm{assoc}}\,({\it{x\/}}, {\rm{cdr}}\,({\it{y\/}}))$\;${\bf  endif}\- \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  assoc-value1 \\ \index{assoc-value1}
{\rm{assoc}}\,({\it{x\/}}, {\rm{cons}}\,({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}), {\it{z\/}})) $=$ {\rm{cons}}\,({\it{x\/}}, {\it{y\/}})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{value}$\;\;$
{\rm{value}}\,({\it{name\/}}, {\it{alist\/}})\index{value} $=$ {\rm{cdr}}\,({\rm{assoc}}\,({\it{name\/}}, {\it{alist\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  value-expansion3 \\ \index{value-expansion3}
{\rm{value}}\,({\it{x\/}}, {\rm{cons}}\,({\rm{cons}}\,({\it{x\/}}, {\it{z\/}}), {\it{alist\/}}))\index{value} $=$ {\it{z\/}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  value-expansion2 \\ \index{value-expansion2}
({\it{x\/}} $\not=$ {\it{y\/}}) $\rightarrow$ ({\rm{value}}\,({\it{x\/}}, {\rm{cons}}\,({\rm{cons}}\,({\it{y\/}}, {\it{z\/}}), {\it{alist\/}}))\index{value} $=$ {\rm{value}}\,({\it{x\/}}, {\it{alist\/}})\index{value})
\end{tabbing}


\noindent{\sc Event}:   Disable value.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{max} \\  
\=\+{\rm{max}}\,({\it{x\/}}, {\it{y\/}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $<$ {\it{y\/}}$\;\;${\bf then }{\it{y\/}} \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\-\-
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  append-cons-rewrite \\ \index{append-cons-rewrite}
{\rm{append}}\,({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}), {\it{z\/}}) $=$ {\rm{cons}}\,({\it{x\/}}, {\rm{append}}\,({\it{y\/}}, {\it{z\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  append-nil-lemma \\ \index{append-nil-lemma}
{\rm{append}}\,({\bf{nil}}, {\it{x\/}}) $=$ {\it{x\/}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  assoc-not-affected-by-extra-element \\ \index{assoc-not-affected-by-extra-ele!ment}
\=\+({\it{y\/}} $\not=$ {\rm{car}}\,({\it{x\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{assoc}}\,({\it{y\/}}, {\rm{append}}\,({\it{lst1\/}}, {\rm{cons}}\,({\it{x\/}}, {\it{lst2\/}}))) $=$ {\rm{assoc}}\,({\it{y\/}}, {\rm{append}}\,({\it{lst1\/}}, {\it{lst2\/}})))\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{plistp} \\  
\=\+{\rm{plistp}}\,({\it{x\/}})\index{plistp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\it{x\/}} $=$ {\bf{nil}} \\ 
{\bf else }{\rm{plistp}}\,({\rm{cdr}}\,({\it{x\/}}))\index{plistp}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{length-plistp} \\  
{\rm{length-plistp}}\,({\it{lst\/}}, {\it{n\/}})\index{length-plistp} $=$ ({\rm{plistp}}\,({\it{lst\/}})\index{plistp} $\wedge$ ({\rm{length}}\,({\it{lst\/}})\index{length} $=$ {\it{n\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  associativity-of-append \\ \index{associativity-of-append}
{\rm{append}}\,({\rm{append}}\,({\it{x\/}}, {\it{y\/}}), {\it{z\/}}) $=$ {\rm{append}}\,({\it{x\/}}, {\rm{append}}\,({\it{y\/}}, {\it{z\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  length-distributes \\ \index{length-distributes}
{\rm{length}}\,({\rm{append}}\,({\it{lst1\/}}, {\it{lst2\/}}))\index{length} $=$ ({\rm{length}}\,({\it{lst1\/}})\index{length} $+$ {\rm{length}}\,({\it{lst2\/}})\index{length})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  not-zerop-length-listp \\ \index{not-zerop-length-listp}
({\rm{length}}\,({\it{x\/}})\index{length} $\not\simeq {\tt{0}}$) $\rightarrow$ {\rm{listp}}\,({\it{x\/}})
\end{tabbing}


\noindent{\sc Event}:   Disable not-zerop-length-listp.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  length-cons \\ \index{length-cons}
{\rm{length}}\,({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}))\index{length} $=$ ($1\;+$ {\rm{length}}\,({\it{y\/}})\index{length})
\end{tabbing}


\noindent{\sc Event}:   Disable length-cons.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  append-rewrite2 \\ \index{append-rewrite2}
({\rm{append}}\,({\it{x\/}}, {\it{y\/}}) $=$ {\rm{append}}\,({\it{x\/}}, {\it{z\/}})) $=$ ({\it{y\/}} $=$ {\it{z\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  append-cons-rewrite2 \\ \index{append-cons-rewrite2}
({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}) $=$ {\rm{cons}}\,({\it{x\/}}, {\it{z\/}})) $=$ ({\it{y\/}} $=$ {\it{z\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member-distributes \\ \index{member-distributes}
({\it{x\/}} $\in$ {\rm{append}}\,({\it{y\/}}, {\it{z\/}})) $=$ (({\it{x\/}} $\in$ {\it{y\/}}) $\vee$ ({\it{x\/}} $\in$ {\it{z\/}}))
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{reverse} \\  
\=\+{\rm{reverse}}\,({\it{x\/}})\index{reverse} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}})$\;\;${\bf then }{\rm{append}}\,({\rm{reverse}}\,({\rm{cdr}}\,({\it{x\/}}))\index{reverse}, {\rm{list}}\,({\rm{car}}\,({\it{x\/}}))) \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  reverse-preserves-length \\ \index{reverse-preserves-length}
{\rm{length}}\,({\rm{reverse}}\,({\it{lst\/}})\index{reverse})\index{length} $=$ {\rm{length}}\,({\it{lst\/}})\index{length}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  reverse-plistp \\ \index{reverse-plistp}
{\rm{plistp}}\,({\rm{reverse}}\,({\it{lst\/}})\index{reverse})\index{plistp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  reverse-reverse \\ \index{reverse-reverse}
{\rm{plistp}}\,({\it{lst\/}})\index{plistp} $\rightarrow$ ({\rm{reverse}}\,({\rm{reverse}}\,({\it{lst\/}})\index{reverse})\index{reverse} $=$ {\it{lst\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  listp-implies-non-zero-length \\ \index{listp-implies-non-zero-length}
{\rm{listp}}\,({\it{x\/}}) $\rightarrow$ ({\rm{length}}\,({\it{x\/}})\index{length} $\not=$ {\tt{0}})
\end{tabbing}

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

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


\noindent{\sc Event}:   Disable superset-preserves-membership.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  cons-preserves-subset \\ \index{cons-preserves-subset}
{\rm{subset}}\,({\it{x\/}}, {\it{y\/}})\index{subset} $\rightarrow$ {\rm{subset}}\,({\it{x\/}}, {\rm{cons}}\,({\it{z\/}}, {\it{y\/}}))\index{subset}
\end{tabbing}


\noindent{\sc Event}:   Disable cons-preserves-subset.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  subset-reflexive \\ \index{subset-reflexive}
{\rm{subset}}\,({\it{y\/}}, {\it{y\/}})\index{subset}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  cons-preserves-subset2 \\ \index{cons-preserves-subset2}
{\rm{subset}}\,({\it{y\/}}, {\rm{cons}}\,({\it{x\/}}, {\it{y\/}}))\index{subset}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subset-distributes \\ \index{subset-distributes}
{\rm{subset}}\,({\rm{append}}\,({\it{x\/}}, {\it{y\/}}), {\it{z\/}})\index{subset} $=$ ({\rm{subset}}\,({\it{x\/}}, {\it{z\/}})\index{subset} $\wedge$ {\rm{subset}}\,({\it{y\/}}, {\it{z\/}})\index{subset})
\end{tabbing}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                      ;;
;;                         ALIST FUNCTIONS                              ;;
;;                                                                      ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{listcars} \\  
\=\+{\rm{listcars}}\,({\it{lst\/}})\index{listcars} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{lst\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{cons}}\,({\rm{car}}\,({\rm{car}}\,({\it{lst\/}})), {\rm{listcars}}\,({\rm{cdr}}\,({\it{lst\/}}))\index{listcars})$\;${\bf  endif}\-\-
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  cons-distributes-over-listcars \\ \index{cons-distributes-over-listcars}
{\rm{listcars}}\,({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}))\index{listcars} $=$ {\rm{cons}}\,({\rm{car}}\,({\it{x\/}}), {\rm{listcars}}\,({\it{y\/}})\index{listcars})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  listcars-distributes \\ \index{listcars-distributes}
{\rm{listcars}}\,({\rm{append}}\,({\it{x\/}}, {\it{y\/}}))\index{listcars} $=$ {\rm{append}}\,({\rm{listcars}}\,({\it{x\/}})\index{listcars}, {\rm{listcars}}\,({\it{y\/}})\index{listcars})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  listcars-preserves-length \\ \index{listcars-preserves-length}
{\rm{length}}\,({\rm{listcars}}\,({\it{lst\/}})\index{listcars})\index{length} $=$ {\rm{length}}\,({\it{lst\/}})\index{length}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  not-member-listcars-not-assoc \\ \index{not-member-listcars-not-assoc}
({\it{x\/}} $\not\in$ {\rm{listcars}}\,({\it{lst\/}})\index{listcars}) $\rightarrow$ ({\rm{assoc}}\,({\it{x\/}}, {\it{lst\/}}) $=$ {\bf{f}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member-listcars-assoc \\ \index{member-listcars-assoc}
({\it{x\/}} $\not\in$ {\rm{listcars}}\,({\it{lst2\/}})\index{listcars}) $\rightarrow$ ({\rm{assoc}}\,({\it{x\/}}, {\rm{append}}\,({\it{lst2\/}}, {\it{lst3\/}})) $=$ {\rm{assoc}}\,({\it{x\/}}, {\it{lst3\/}}))
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  no-duplicates-append \\ \index{no-duplicates-append}
{\rm{no-duplicates}}\,({\rm{append}}\,({\it{x\/}}, {\it{y\/}}))\index{no-duplicates} $\rightarrow$ ({\rm{no-duplicates}}\,({\it{x\/}})\index{no-duplicates} $\wedge$ {\rm{no-duplicates}}\,({\it{y\/}})\index{no-duplicates})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  no-duplicates-append-append \\ \index{no-duplicates-append-append}
{\rm{no-duplicates}}\,({\rm{append}}\,({\it{x\/}}, {\rm{append}}\,({\it{y\/}}, {\it{z\/}})))\index{no-duplicates} $\rightarrow$ {\rm{no-duplicates}}\,({\rm{append}}\,({\it{x\/}}, {\it{z\/}}))\index{no-duplicates}
\end{tabbing}


\noindent{\sc Event}:   Disable no-duplicates-append-append.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  no-duplicates-member2 \\ \index{no-duplicates-member2}
\=\+({\rm{no-duplicates}}\,({\rm{append}}\,({\it{lst1\/}}, {\it{lst2\/}}))\index{no-duplicates} $\wedge$ ({\it{x\/}} $\in$ {\it{lst1\/}})) \\ 
$\rightarrow$$\;\;\;\;$(({\it{x\/}} $\in$ {\it{lst2\/}}) $=$ {\bf{f}})\-
\end{tabbing}


\noindent{\sc Event}:   Disable no-duplicates-member2.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  subset-preserves-no-duplicates \\ \index{subset-preserves-no-duplicates}
\=\+({\rm{no-duplicates}}\,({\rm{append}}\,({\it{x\/}}, {\it{y\/}}))\index{no-duplicates} $\wedge$ {\rm{no-duplicates}}\,({\it{z\/}})\index{no-duplicates} $\wedge$ {\rm{subset}}\,({\it{z\/}}, {\it{y\/}})\index{subset}) \\ 
$\rightarrow$$\;\;\;\;${\rm{no-duplicates}}\,({\rm{append}}\,({\it{x\/}}, {\it{z\/}}))\index{no-duplicates}\-
\end{tabbing}


\noindent{\sc Event}:   Disable subset-preserves-no-duplicates.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  no-duplicates-cons-append2 \\ \index{no-duplicates-cons-append2}
{\rm{no-duplicates}}\,({\rm{cons}}\,({\it{x\/}}, {\rm{append}}\,({\it{y\/}}, {\it{z\/}})))\index{no-duplicates} $\rightarrow$ {\rm{no-duplicates}}\,({\rm{cons}}\,({\it{x\/}}, {\it{z\/}}))\index{no-duplicates}
\end{tabbing}


\noindent{\sc Event}:   Disable no-duplicates-cons-append2.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  no-duplicates-member-append2 \\ \index{no-duplicates-member-append2}
{\rm{no-duplicates}}\,({\rm{append}}\,({\it{a\/}}, {\rm{cons}}\,({\it{x\/}}, {\it{b\/}})))\index{no-duplicates} $\rightarrow$ {\rm{no-duplicates}}\,({\rm{append}}\,({\it{a\/}}, {\it{b\/}}))\index{no-duplicates}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  no-duplicates-duplication \\ \index{no-duplicates-duplication}
\=\+(({\it{x\/}} $\in$ {\it{lst1\/}}) $\wedge$ ({\it{x\/}} $\in$ {\it{lst2\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{no-duplicates}}\,({\rm{append}}\,({\it{lst1\/}}, {\it{lst2\/}}))\index{no-duplicates} $=$ {\bf{f}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  no-duplicates-cons-append \\ \index{no-duplicates-cons-append}
\=\+(({\it{x\/}} $\not\in$ {\it{lst1\/}}) $\wedge$ ({\it{x\/}} $\not\in$ {\it{lst2\/}}) $\wedge$ {\rm{no-duplicates}}\,({\rm{append}}\,({\it{lst1\/}}, {\it{lst2\/}}))\index{no-duplicates}) \\ 
$\rightarrow$$\;\;\;\;${\rm{no-duplicates}}\,({\rm{append}}\,({\it{lst1\/}}, {\rm{cons}}\,({\it{x\/}}, {\it{lst2\/}})))\index{no-duplicates}\-
\end{tabbing}


\noindent{\sc Event}:   Disable no-duplicates-cons-append.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  append-plistp-nil-lemma \\ \index{append-plistp-nil-lemma}
{\rm{plistp}}\,({\it{x\/}})\index{plistp} $\rightarrow$ ({\rm{append}}\,({\it{x\/}}, {\bf{nil}}) $=$ {\it{x\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  no-duplicates-commutes-append \\ \index{no-duplicates-commutes-append}
\=\+({\rm{plistp}}\,({\it{x\/}})\index{plistp} $\wedge$ {\rm{plistp}}\,({\it{y\/}})\index{plistp} $\wedge$ {\rm{no-duplicates}}\,({\rm{append}}\,({\it{x\/}}, {\it{y\/}}))\index{no-duplicates}) \\ 
$\rightarrow$$\;\;\;\;${\rm{no-duplicates}}\,({\rm{append}}\,({\it{y\/}}, {\it{x\/}}))\index{no-duplicates}\-
\end{tabbing}


\noindent{\sc Event}:   Disable no-duplicates-commutes-append.

\addvspace{18pt}

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

\begin{tabbing}{\sc Definition}:\index{all-cars-unique}$\;\;$
{\rm{all-cars-unique}}\,({\it{lst\/}})\index{all-cars-unique} $=$ {\rm{no-duplicates}}\,({\rm{listcars}}\,({\it{lst\/}})\index{listcars})\index{no-duplicates}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  cars-unique-cars-unique \\ \index{cars-unique-cars-unique}
({\rm{all-cars-unique}}\,({\rm{cons}}\,({\it{y\/}}, {\it{lst\/}}))\index{all-cars-unique} $\wedge$ ({\it{x\/}} $\in$ {\it{lst\/}})) $\rightarrow$ ({\rm{car}}\,({\it{x\/}}) $\not=$ {\rm{car}}\,({\it{y\/}}))
\end{tabbing}


\noindent{\sc Event}:   Disable cars-unique-cars-unique.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  assoc-unique-member \\ \index{assoc-unique-member}
(({\it{x\/}} $\in$ {\it{lst\/}}) $\wedge$ {\rm{all-cars-unique}}\,({\it{lst\/}})\index{all-cars-unique}) $\rightarrow$ ({\rm{assoc}}\,({\rm{car}}\,({\it{x\/}}), {\it{lst\/}}) $=$ {\it{x\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  no-duplicates-member-cons \\ \index{no-duplicates-member-cons}
{\rm{no-duplicates}}\,({\rm{append}}\,({\it{x\/}}, {\rm{cons}}\,({\it{y\/}}, {\it{z\/}})))\index{no-duplicates} $\rightarrow$ ({\it{y\/}} $\not\in$ {\it{z\/}})
\end{tabbing}


\noindent{\sc Event}:   Disable no-duplicates-member-cons.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  all-cars-unique-commutes-append \\ \index{all-cars-unique-commutes-append}
\=\+({\rm{plistp}}\,({\it{x\/}})\index{plistp} $\wedge$ {\rm{plistp}}\,({\it{y\/}})\index{plistp} $\wedge$ {\rm{all-cars-unique}}\,({\rm{append}}\,({\it{x\/}}, {\it{y\/}}))\index{all-cars-unique}) \\ 
$\rightarrow$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{append}}\,({\it{y\/}}, {\it{x\/}}))\index{all-cars-unique}\-
\end{tabbing}


\noindent{\sc Event}:   Disable all-cars-unique-commutes-append.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  cars-unique-cons \\ \index{cars-unique-cons}
{\rm{all-cars-unique}}\,({\rm{cons}}\,({\it{x\/}}, {\rm{cons}}\,({\it{y\/}}, {\it{z\/}})))\index{all-cars-unique} $\rightarrow$ {\rm{all-cars-unique}}\,({\rm{cons}}\,({\it{x\/}}, {\it{z\/}}))\index{all-cars-unique}
\end{tabbing}


\noindent{\sc Event}:   Disable cars-unique-cons.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  cons-car-append-all-cars-unique \\ \index{cons-car-append-all-cars-unique}
\=\+({\rm{listp}}\,({\it{x\/}}) $\wedge$ {\rm{all-cars-unique}}\,({\rm{append}}\,({\it{x\/}}, {\it{y\/}}))\index{all-cars-unique}) \\ 
$\rightarrow$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{cons}}\,({\rm{car}}\,({\it{x\/}}), {\it{y\/}}))\index{all-cars-unique}\-
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  cars-unique-names-unique \\ \index{cars-unique-names-unique}
\=\+({\rm{all-cars-unique}}\,({\rm{append}}\,({\it{z\/}}, {\it{w\/}}))\index{all-cars-unique} $\wedge$ ({\it{x\/}} $\in$ {\it{z\/}}) $\wedge$ ({\it{y\/}} $\in$ {\it{w\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{car}}\,({\it{x\/}}) $\not=$ {\rm{car}}\,({\it{y\/}}))\-
\end{tabbing}


\noindent{\sc Event}:   Disable cars-unique-names-unique.

\addvspace{18pt}


\noindent{\sc Event}:   Disable all-cars-unique.

\addvspace{18pt}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                             ;;
;;                   ARITHMETIC FUNCTIONS                      ;;
;;                                                             ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{exp} \\  
\=\+{\rm{exp}}\,({\it{x\/}}, {\it{y\/}})\index{exp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{y\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\it{x\/}} $*$ {\rm{exp}}\,({\it{x\/}}, {\it{y\/}} $-\;1$)\index{exp}$\;${\bf  endif}\-\-
\end{tabbing}


\begin{tabbing}{\sc Definition}:\index{integerp} \\  
{\rm{integerp}}\,({\it{x\/}})\index{integerp} $=$ (({\rm{negativep}}\,({\it{x\/}}) $\wedge$ ({\rm{negative-guts}}\,({\it{x\/}}) $\not=$ {\tt{0}})) $\vee$ ({\it{x\/}} $\in\;${\bf{N}}${}$))
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{ilessp} \\  
\=\+{\rm{ilessp}}\,({\it{x\/}}, {\it{y\/}})\index{ilessp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{negativep}}\,({\it{x\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{negativep}}\,({\it{y\/}})$\;\;${\bf then }{\rm{negative-guts}}\,({\it{y\/}}) $<$ {\rm{negative-guts}}\,({\it{x\/}}) \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\- \\ 
{\bf elseif }{\rm{negativep}}\,({\it{y\/}})$\;\;${\bf then }{\bf{f}} \\ 
{\bf else }{\it{x\/}} $<$ {\it{y\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{iplus} \\  
\=\+{\rm{iplus}}\,({\it{i\/}}, {\it{j\/}})\index{iplus} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{negativep}}\,({\it{i\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{negativep}}\,({\it{j\/}})$\;\;${\bf then }$-$ ({\rm{negative-guts}}\,({\it{i\/}}) $+$ {\rm{negative-guts}}\,({\it{j\/}})) \\ 
{\bf elseif }{\it{j\/}} $<$ {\rm{negative-guts}}\,({\it{i\/}})$\;\;${\bf then }$-$ ({\rm{negative-guts}}\,({\it{i\/}}) $-$ {\it{j\/}}) \\ 
{\bf else }{\it{j\/}} $-$ {\rm{negative-guts}}\,({\it{i\/}})$\;${\bf  endif}\- \\ 
{\bf elseif }{\rm{negativep}}\,({\it{j\/}}) \\ 
{\bf then }\=\+{\bf if }{\it{i\/}} $<$ {\rm{negative-guts}}\,({\it{j\/}})$\;\;${\bf then }$-$ ({\rm{negative-guts}}\,({\it{j\/}}) $-$ {\it{i\/}}) \\ 
{\bf else }{\it{i\/}} $-$ {\rm{negative-guts}}\,({\it{j\/}})$\;${\bf  endif}\- \\ 
{\bf else }{\it{i\/}} $+$ {\it{j\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{inegate} \\  
\=\+{\rm{inegate}}\,({\it{i\/}})\index{inegate} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{negativep}}\,({\it{i\/}})$\;\;${\bf then }{\rm{negative-guts}}\,({\it{i\/}}) \\ 
{\bf elseif }{\it{i\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }$-$ {\it{i\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{idifference}$\;\;$
{\rm{idifference}}\,({\it{i\/}}, {\it{j\/}})\index{idifference} $=$ {\rm{iplus}}\,({\it{i\/}}, {\rm{inegate}}\,({\it{j\/}})\index{inegate})\index{iplus}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{ileq}$\;\;$
{\rm{ileq}}\,({\it{x\/}}, {\it{y\/}})\index{ileq} $=$ ($\neg$ {\rm{ilessp}}\,({\it{y\/}}, {\it{x\/}})\index{ilessp})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  zero-iplus-identity \\ \index{zero-iplus-identity}
{\rm{integerp}}\,({\it{n\/}})\index{integerp} $\rightarrow$ ({\rm{iplus}}\,({\tt{0}}, {\it{n\/}})\index{iplus} $=$ {\it{n\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  iplus-integerp \\ \index{iplus-integerp}
({\rm{integerp}}\,({\it{n\/}})\index{integerp} $\wedge$ {\rm{integerp}}\,({\it{m\/}})\index{integerp}) $\rightarrow$ {\rm{integerp}}\,({\rm{iplus}}\,({\it{n\/}}, {\it{m\/}})\index{iplus})\index{integerp}
\end{tabbing}


\noindent{\sc Event}:   Disable iplus-integerp.

\addvspace{18pt}

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


\noindent{\sc Event}:   Disable plus-commutes.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  plus-0-rewrite \\ \index{plus-0-rewrite}
({\it{x\/}} $+$ {\tt{0}}) $=$ {\rm{fix}}\,({\it{x\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  plus-add1 \\ \index{plus-add1}
({\it{x\/}} $+$ {\tt{1}}) $=$ ($1\;+$ {\it{x\/}})
\end{tabbing}


\noindent{\sc Event}:   Disable plus-add1.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  times-m-rewrite \\ \index{times-m-rewrite}
({\it{m\/}} $*$ ($1\;+$ {\it{n\/}})) $=$ ({\it{m\/}} $+$ ({\it{m\/}} $*$ {\it{n\/}}))
\end{tabbing}


\noindent{\sc Event}:   Disable times-m-rewrite.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  plus-add1-commute \\ \index{plus-add1-commute}
({\it{x\/}} $+$ ($1\;+$ {\it{n\/}})) $=$ ($1\;+$ ({\it{x\/}} $+$ {\it{n\/}}))
\end{tabbing}


\noindent{\sc Event}:   Disable plus-add1-commute.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  add1-preserves-lessp \\ \index{add1-preserves-lessp}
({\it{n\/}} $<$ {\it{m\/}}) $\rightarrow$ (({\it{n\/}} $<$ ($1\;+$ {\it{m\/}})) $=$ {\bf{t}})
\end{tabbing}


\noindent{\sc Event}:   Disable add1-preserves-lessp.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  difference-x-x \\ \index{difference-x-x}
({\it{x\/}} $-$ {\it{x\/}}) $=$ {\tt{0}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  plus-equality-lemma1 \\ \index{plus-equality-lemma1}
({\it{m\/}} $=$ {\it{k\/}}) $\rightarrow$ ((({\it{n\/}} $+$ {\it{m\/}}) $=$ ({\it{n\/}} $+$ {\it{k\/}})) $=$ {\bf{t}})
\end{tabbing}


\noindent{\sc Event}:   Disable plus-equality-lemma1.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  difference-rewrite \\ \index{difference-rewrite}
({\it{y\/}} $<$ {\it{x\/}}) $\rightarrow$ (({\it{x\/}} $-$ {\it{y\/}}) $=$ ($1\;+$ ({\it{x\/}} $-$ ($1\;+$ {\it{y\/}}))))
\end{tabbing}


\noindent{\sc Event}:   Disable difference-rewrite.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  sub1-preserves-lessp \\ \index{sub1-preserves-lessp}
({\it{x\/}} $<$ {\it{y\/}}) $\rightarrow$ ((({\it{x\/}} $-\;1$) $<$ {\it{y\/}}) $=$ {\bf{t}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  add1-difference \\ \index{add1-difference}
({\it{j\/}} $\leq$ {\it{k\/}}) $\rightarrow$ ((($1\;+$ {\it{k\/}}) $-$ {\it{j\/}}) $=$ ($1\;+$ ({\it{k\/}} $-$ {\it{j\/}})))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  add1-sub1-difference \\ \index{add1-sub1-difference}
((($1\;+$ {\it{x\/}}) $-$ {\it{y\/}}) $-\;1$) $=$ ({\it{x\/}} $-$ {\it{y\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  difference-add1 \\ \index{difference-add1}
(($1\;+$ {\it{n\/}}) $-$ {\it{n\/}}) $=$ {\tt{1}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  difference-plus-rewrite \\ \index{difference-plus-rewrite}
(({\it{x\/}} $+$ {\it{y\/}}) $-$ {\it{x\/}}) $=$ {\rm{fix}}\,({\it{y\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  plus-0-rewrite2 \\ \index{plus-0-rewrite2}
({\it{n\/}} $\simeq {\tt{0}}$) $\rightarrow$ (({\it{m\/}} $+$ {\it{n\/}}) $=$ {\rm{fix}}\,({\it{m\/}}))
\end{tabbing}
           
\begin{tabbing}{\sc Theorem}:  plus-add1-sub1 \\ \index{plus-add1-sub1}
({\it{m\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ ((($1\;+$ {\it{n\/}}) $+$ ({\it{m\/}} $-\;1$)) $=$ ({\it{n\/}} $+$ {\it{m\/}}))
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  difference-n-leq \\ \index{difference-n-leq}
({\it{n\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ (((({\it{n\/}} $-$ {\it{m\/}}) $-\;1$) $<$ {\it{n\/}}) $=$ {\bf{t}})
\end{tabbing}


\noindent{\sc Event}:   Disable difference-n-leq.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  plus-preserves-lessp \\ \index{plus-preserves-lessp}
(({\it{x\/}} $+$ {\it{y\/}}) $<$ {\it{z\/}}) $\rightarrow$ (({\it{x\/}} $<$ {\it{z\/}}) $=$ {\bf{t}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  plus-preserves-lessp2 \\ \index{plus-preserves-lessp2}
({\it{x\/}} $<$ {\it{y\/}}) $\rightarrow$ (({\it{x\/}} $<$ ({\it{n\/}} $+$ {\it{y\/}})) $=$ {\bf{t}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-transitive \\ \index{lessp-transitive}
(({\it{x\/}} $<$ {\it{y1\/}}) $\wedge$ ({\it{y2\/}} $\not<$ {\it{y1\/}})) $\rightarrow$ (({\it{x\/}} $<$ {\it{y2\/}}) $=$ {\bf{t}})
\end{tabbing}


\noindent{\sc Event}:   Disable lessp-transitive.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  difference-lessp \\ \index{difference-lessp}
({\it{x\/}} $<$ ({\it{y\/}} $-$ {\it{z\/}})) $\rightarrow$ (({\it{z\/}} $<$ {\it{y\/}}) $=$ {\bf{t}})
\end{tabbing}


\noindent{\sc Event}:   Disable difference-lessp.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  plus-preserves-lessp3 \\ \index{plus-preserves-lessp3}
({\it{n\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ (({\it{k\/}} $<$ ({\it{n\/}} $+$ {\it{k\/}})) $=$ {\bf{t}})
\end{tabbing}


\noindent{\sc Event}:   Disable plus-preserves-lessp3.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  difference-difference-plus \\ \index{difference-difference-plus}
(({\it{n\/}} $\not<$ {\it{l\/}}) $\wedge$ ({\it{k\/}} $\not<$ {\it{n\/}})) $\rightarrow$ (({\it{k\/}} $-$ ({\it{n\/}} $-$ {\it{l\/}})) $=$ ({\it{l\/}} $+$ ({\it{k\/}} $-$ {\it{n\/}})))
\end{tabbing}


\noindent{\sc Event}:   Disable difference-difference-plus.

\addvspace{18pt}		

\begin{tabbing}{\sc Theorem}:  zerop-difference-lessp \\ \index{zerop-difference-lessp}
({\it{m\/}} $<$ {\it{n\/}}) $\rightarrow$ ((({\it{n\/}} $-$ {\it{m\/}}) $=$ {\tt{0}}) $=$ {\bf{f}})
\end{tabbing}


\noindent{\sc Event}:   Disable zerop-difference-lessp.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  add1-difference2 \\ \index{add1-difference2}
({\it{y\/}} $<$ {\it{x\/}}) $\rightarrow$ (({\it{x\/}} $-$ ($1\;+$ {\it{y\/}})) $=$ (({\it{x\/}} $-$ {\it{y\/}}) $-\;1$))
\end{tabbing}


\noindent{\sc Event}:   Disable add1-difference2.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  sub1-plus5 \\ \index{sub1-plus5}
({\it{y\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ (({\it{x\/}} $+$ ({\it{y\/}} $-\;1$)) $=$ (({\it{x\/}} $+$ {\it{y\/}}) $-\;1$))
\end{tabbing}


\noindent{\sc Event}:   Disable sub1-plus5.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  sub1-plus4 \\ \index{sub1-plus4}
(({\it{x\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{y\/}} $\not\simeq {\tt{0}}$)) $\rightarrow$ ((({\it{x\/}} $-\;1$) $+$ {\it{y\/}}) $=$ ({\it{x\/}} $+$ ({\it{y\/}} $-\;1$)))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  difference-lessp2 \\ \index{difference-lessp2}
(({\it{x\/}} $+$ {\it{y\/}} $+$ {\it{z\/}}) $<$ ({\it{m\/}} $-$ {\it{n\/}})) $\rightarrow$ (({\it{m\/}} $<$ ({\it{x\/}} $+$ {\it{y\/}} $+$ {\it{z\/}} $+$ {\it{n\/}})) $=$ {\bf{f}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  plus-times-3 \\ \index{plus-times-3}
\=\+({\it{k\/}} $\not\simeq {\tt{0}}$) \\ 
$\rightarrow$$\;\;\;\;$((({\it{k\/}} $*$ {\tt{3}}) $+$ {\it{n\/}}) $=$ ($1\;+$ ($1\;+$ ($1\;+$ ((({\it{k\/}} $-\;1$) $*$ {\tt{3}}) $+$ {\it{n\/}})))))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  zero-iplus-right-identity \\ \index{zero-iplus-right-identity}
{\rm{integerp}}\,({\it{x\/}})\index{integerp} $\rightarrow$ ({\rm{iplus}}\,({\it{x\/}}, {\tt{0}})\index{iplus} $=$ {\it{x\/}})
\end{tabbing}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                             ;;
;;                    MISCELLANEOUS STUFF                      ;;
;;                                                             ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

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

\begin{verbatim};; Index is used for converting the current condition to a numeric
;; value for the lower level state.  

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{index} \\  
\=\+{\rm{index}}\,({\it{y\/}}, {\it{lst\/}})\index{index} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{lst\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{y\/}} $=$ {\rm{car}}\,({\it{lst\/}})$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }$1\;+$ {\rm{index}}\,({\it{y\/}}, {\rm{cdr}}\,({\it{lst\/}}))\index{index}$\;${\bf  endif}\-\-
\end{tabbing} 

\begin{tabbing}{\sc Theorem}:  member-implies-nonzero-index \\ \index{member-implies-nonzero-index}
({\it{c\/}} $\in$ {\it{cond-list\/}}) $\rightarrow$ ({\rm{index}}\,({\it{c\/}}, {\it{cond-list\/}})\index{index} $\not=$ {\tt{0}})
\end{tabbing}


\noindent{\sc Event}:   Disable member-implies-nonzero-index.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  member-index-lessp-length \\ \index{member-index-lessp-length}
{\rm{index}}\,({\it{c\/}}, {\it{cond-list\/}})\index{index} $<$ ($1\;+$ {\rm{length}}\,({\it{cond-list\/}})\index{length})
\end{tabbing}


\noindent{\sc Event}:   Disable member-index-lessp-length.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  lessp-member-index-length \\ \index{lessp-member-index-length}
({\it{x\/}} $\in$ {\it{lst\/}}) $\rightarrow$ (({\rm{index}}\,({\it{x\/}}, {\it{lst\/}})\index{index} $<$ ($1\;+$ {\rm{length}}\,({\it{lst\/}})\index{length})) $=$ {\bf{t}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  index-length \\ \index{index-length}
({\rm{length}}\,({\it{lst\/}})\index{length} $<$ ({\it{n\/}} $-\;1$)) $\rightarrow$ (({\rm{index}}\,({\it{x\/}}, {\it{lst\/}})\index{index} $<$ {\it{n\/}}) $=$ {\bf{t}})
\end{tabbing}


\noindent{\sc Event}:   Disable index-length.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  nth-index-elimination \\ \index{nth-index-elimination}
({\it{x\/}} $\in$ {\it{lst\/}}) $\rightarrow$ ({\rm{car}}\,({\rm{nth}}\,({\it{lst\/}}, {\rm{index}}\,({\it{x\/}}, {\it{lst\/}})\index{index} $-\;1$)\index{nth}) $=$ {\it{x\/}})
\end{tabbing}


\noindent{\sc Event}:   Disable nth-index-elimination.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  subset-append1 \\ \index{subset-append1}
{\rm{subset}}\,({\it{x\/}}, {\it{y\/}})\index{subset} $\rightarrow$ ({\rm{subset}}\,({\it{x\/}}, {\rm{append}}\,({\it{y\/}}, {\it{z\/}}))\index{subset} $\wedge$ {\rm{subset}}\,({\it{x\/}}, {\rm{append}}\,({\it{z\/}}, {\it{y\/}}))\index{subset})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  reorder-subset \\ \index{reorder-subset}
{\rm{subset}}\,({\rm{cons}}\,({\it{x\/}}, {\rm{append}}\,({\it{y\/}}, {\it{z\/}})), {\rm{append}}\,({\it{y\/}}, {\rm{cons}}\,({\it{x\/}}, {\it{z\/}})))\index{subset}
\end{tabbing}


\noindent{\sc Event}:   Disable reorder-subset.

\addvspace{18pt}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                             ;;
;;                       PLISTP LEMMAS                         ;;
;;                                                             ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

\end{verbatim}\begin{tabbing}{\sc Theorem}:  plistp-cons \\ \index{plistp-cons}
{\rm{plistp}}\,({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}))\index{plistp} $=$ {\rm{plistp}}\,({\it{y\/}})\index{plistp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  plistp-append \\ \index{plistp-append}
{\rm{plistp}}\,({\rm{append}}\,({\it{x\/}}, {\it{y\/}}))\index{plistp} $=$ {\rm{plistp}}\,({\it{y\/}})\index{plistp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  plistp-atom \\ \index{plistp-atom}
({\it{x\/}} $\simeq\;${{\bf{nil}}}${}$) $\rightarrow$ ({\rm{plistp}}\,({\it{x\/}})\index{plistp} $=$ ({\it{x\/}} $=$ {\bf{nil}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  zero-length-plistp-nil \\ \index{zero-length-plistp-nil}
({\rm{plistp}}\,({\it{x\/}})\index{plistp} $\wedge$ ({\rm{length}}\,({\it{x\/}})\index{length} $=$ {\tt{0}})) $\rightarrow$ (({\it{x\/}} $=$ {\bf{nil}}) $=$ {\bf{t}})
\end{tabbing}


\noindent{\sc Event}:   Disable zero-length-plistp-nil.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  cddr-length-plistp-2 \\ \index{cddr-length-plistp-2}
{\rm{length-plistp}}\,({\it{x\/}}, {\tt{2}})\index{length-plistp} $\rightarrow$ ({\rm{cddr}}\,({\it{x\/}}) $=$ {\bf{nil}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  reverse-append-reverse1 \\ \index{reverse-append-reverse1}
\=\+({\rm{plistp}}\,({\it{x\/}})\index{plistp} $\wedge$ {\rm{plistp}}\,({\it{y\/}})\index{plistp}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{reverse}}\,({\rm{append}}\,({\it{x\/}}, {\it{y\/}}))\index{reverse} $=$ {\rm{append}}\,({\rm{reverse}}\,({\it{y\/}})\index{reverse}, {\rm{reverse}}\,({\it{x\/}})\index{reverse}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  reverse-append-reverse \\ \index{reverse-append-reverse}
\=\+({\rm{plistp}}\,({\it{lst1\/}})\index{plistp} $\wedge$ {\rm{plistp}}\,({\it{lst2\/}})\index{plistp}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{reverse}}\,({\rm{append}}\,({\rm{reverse}}\,({\it{lst1\/}})\index{reverse}, {\rm{reverse}}\,({\it{lst2\/}})\index{reverse}))\index{reverse} $=$ {\rm{append}}\,({\it{lst2\/}}, {\it{lst1\/}}))\-
\end{tabbing}


\noindent{\sc Event}:   Disable reverse-append-reverse.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  append-doesnt-affect-value4 \\ \index{append-doesnt-affect-value4}
({\it{x\/}} $\not\in$ {\rm{listcars}}\,({\it{z\/}})\index{listcars}) $\rightarrow$ ({\rm{assoc}}\,({\it{x\/}}, {\rm{append}}\,({\it{y\/}}, {\it{z\/}})) $=$ {\rm{assoc}}\,({\it{x\/}}, {\it{y\/}}))
\end{tabbing}


\noindent{\sc Event}:   Disable append-doesnt-affect-value4.

\addvspace{18pt}


\noindent{\sc Event}:   Disable length-plistp.

\addvspace{18pt}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                             ;;
;;                     GET and PUT LEMMAS                      ;;
;;                                                             ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

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

\begin{tabbing}{\sc Theorem}:  get-0 \\ \index{get-0}
{\rm{get}}\,({\tt{0}}, {\rm{cons}}\,({\it{x\/}}, {\it{y\/}}))\index{get} $=$ {\it{x\/}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  get-add1 \\ \index{get-add1}
{\rm{get}}\,($1\;+$ {\it{n\/}}, {\rm{cons}}\,({\it{x\/}}, {\it{y\/}}))\index{get} $=$ {\rm{get}}\,({\it{n\/}}, {\it{y\/}})\index{get}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  get-length-cons \\ \index{get-length-cons}
({\it{n\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ ({\rm{get}}\,({\it{n\/}}, {\rm{cons}}\,({\it{x\/}}, {\it{lst\/}}))\index{get} $=$ {\rm{get}}\,({\it{n\/}} $-\;1$, {\it{lst\/}})\index{get})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  get-length-car1 \\ \index{get-length-car1}
{\rm{get}}\,({\rm{length}}\,({\it{lst\/}})\index{length}, {\rm{append}}\,({\it{lst\/}}, {\it{lst2\/}}))\index{get} $=$ {\rm{car}}\,({\it{lst2\/}})
\end{tabbing}


\noindent{\sc Event}:   Disable get-length-car1.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  get-length-car \\ \index{get-length-car}
({\it{n\/}} $=$ {\rm{length}}\,({\it{lst\/}})\index{length}) $\rightarrow$ ({\rm{get}}\,({\it{n\/}}, {\rm{append}}\,({\it{lst\/}}, {\it{lst2\/}}))\index{get} $=$ {\rm{car}}\,({\it{lst2\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  get-length-plus \\ \index{get-length-plus}
({\it{n\/}} $=$ {\rm{length}}\,({\it{lst1\/}})\index{length}) $\rightarrow$ ({\rm{get}}\,({\it{n\/}} $+$ {\it{m\/}}, {\rm{append}}\,({\it{lst1\/}}, {\it{lst2\/}}))\index{get} $=$ {\rm{get}}\,({\it{m\/}}, {\it{lst2\/}})\index{get})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  get-car \\ \index{get-car}
({\it{n\/}} $\simeq {\tt{0}}$) $\rightarrow$ ({\rm{get}}\,({\it{n\/}}, {\it{lst\/}})\index{get} $=$ {\rm{car}}\,({\it{lst\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  get-sub1 \\ \index{get-sub1}
({\it{n\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ ({\rm{get}}\,({\it{n\/}}, {\it{lst\/}})\index{get} $=$ {\rm{get}}\,({\it{n\/}} $-\;1$, {\rm{cdr}}\,({\it{lst\/}}))\index{get})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  get-append \\ \index{get-append}
({\it{k\/}} $<$ {\rm{length}}\,({\it{lst1\/}})\index{length}) $\rightarrow$ ({\rm{get}}\,({\it{k\/}}, {\rm{append}}\,({\it{lst1\/}}, {\it{lst2\/}}))\index{get} $=$ {\rm{get}}\,({\it{k\/}}, {\it{lst1\/}})\index{get})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  get-add1-add1-append \\ \index{get-add1-add1-append}
{\rm{get}}\,({\it{n\/}} $+$ ($1\;+$ ($1\;+$ {\it{m\/}})), {\rm{cons}}\,({\it{x\/}}, {\rm{cons}}\,({\it{y\/}}, {\it{lst\/}})))\index{get} $=$ {\rm{get}}\,({\it{n\/}} $+$ {\it{m\/}}, {\it{lst\/}})\index{get}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  get-add1-length-plus \\ \index{get-add1-length-plus}
\=\+(({\rm{length}}\,({\it{lst1\/}})\index{length} $=$ ($1\;+$ {\it{n\/}})) $\wedge$ ({\it{m\/}} $\not\simeq {\tt{0}}$)) \\ 
$\rightarrow$$\;\;\;\;$({\rm{get}}\,({\it{n\/}} $+$ {\it{m\/}}, {\rm{append}}\,({\it{lst1\/}}, {\it{lst2\/}}))\index{get} $=$ {\rm{get}}\,({\it{m\/}} $-\;1$, {\it{lst2\/}})\index{get})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  get-add1-plus \\ \index{get-add1-plus}
{\rm{get}}\,(($1\;+$ {\it{n\/}}) $+$ {\it{m\/}}, {\rm{cons}}\,({\it{x\/}}, {\it{y\/}}))\index{get} $=$ {\rm{get}}\,({\it{n\/}} $+$ {\it{m\/}}, {\it{y\/}})\index{get}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  get-0-plus \\ \index{get-0-plus}
{\rm{get}}\,({\tt{0}} $+$ {\it{n\/}}, {\it{y\/}})\index{get} $=$ {\rm{get}}\,({\it{n\/}}, {\it{y\/}})\index{get}
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  put-car-nlistp \\ \index{put-car-nlistp}
(({\it{n\/}} $\simeq {\tt{0}}$) $\wedge$ ({\it{lst\/}} $\simeq\;${{\bf{nil}}}${}$)) $\rightarrow$ ({\rm{put}}\,({\it{val\/}}, {\it{n\/}}, {\it{lst\/}})\index{put} $=$ {\rm{list}}\,({\it{val\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  put-car-listp \\ \index{put-car-listp}
(({\it{n\/}} $\simeq {\tt{0}}$) $\wedge$ {\rm{listp}}\,({\it{lst\/}})) $\rightarrow$ ({\rm{put}}\,({\it{val\/}}, {\it{n\/}}, {\it{lst\/}})\index{put} $=$ {\rm{cons}}\,({\it{val\/}}, {\rm{cdr}}\,({\it{lst\/}})))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  put-preserves-plistp \\ \index{put-preserves-plistp}
{\rm{plistp}}\,({\it{lst\/}})\index{plistp} $\rightarrow$ {\rm{plistp}}\,({\rm{put}}\,({\it{val\/}}, {\it{n\/}}, {\it{lst\/}})\index{put})\index{plistp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  get-inverts-put \\ \index{get-inverts-put}
{\rm{get}}\,({\it{y\/}}, {\rm{put}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{put})\index{get} $=$ {\it{x\/}}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{put-assoc} \\  
\=\+{\rm{put-assoc}}\,({\it{val\/}}, {\it{name\/}}, {\it{alist\/}})\index{put-assoc} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{alist\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\it{alist\/}} \\ 
{\bf elseif }{\it{name\/}} $=$ {\rm{caar}}\,({\it{alist\/}})$\;\;${\bf then }{\rm{cons}}\,({\rm{cons}}\,({\it{name\/}}, {\it{val\/}}), {\rm{cdr}}\,({\it{alist\/}})) \\ 
{\bf else }{\rm{cons}}\,({\rm{car}}\,({\it{alist\/}}), {\rm{put-assoc}}\,({\it{val\/}}, {\it{name\/}}, {\rm{cdr}}\,({\it{alist\/}}))\index{put-assoc})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  put-assoc-expansion \\ \index{put-assoc-expansion}
{\rm{put-assoc}}\,({\it{x\/}}, {\it{y\/}}, {\rm{cons}}\,({\rm{cons}}\,({\it{y\/}}, {\it{z\/}}), {\it{w\/}}))\index{put-assoc} $=$ {\rm{cons}}\,({\rm{cons}}\,({\it{y\/}}, {\it{x\/}}), {\it{w\/}})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{definedp} \\  
\=\+{\rm{definedp}}\,({\it{name\/}}, {\it{alist\/}})\index{definedp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{alist\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{f}} \\ 
{\bf elseif }{\it{name\/}} $=$ {\rm{caar}}\,({\it{alist\/}})$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{definedp}}\,({\it{name\/}}, {\rm{cdr}}\,({\it{alist\/}}))\index{definedp}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member-defined-name \\ \index{member-defined-name}
({\it{x\/}} $\in$ {\it{y\/}}) $\rightarrow$ {\rm{definedp}}\,({\rm{car}}\,({\it{x\/}}), {\it{y\/}})\index{definedp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  definedp-car-assoc \\ \index{definedp-car-assoc}
{\rm{definedp}}\,({\it{x\/}}, {\it{lst\/}})\index{definedp} $\rightarrow$ ({\rm{car}}\,({\rm{assoc}}\,({\it{x\/}}, {\it{lst\/}})) $=$ {\it{x\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  definedp-car-cons \\ \index{definedp-car-cons}
{\rm{definedp}}\,({\it{x\/}}, {\rm{cons}}\,({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}), {\it{z\/}}))\index{definedp}
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  definedp-implies-member \\ \index{definedp-implies-member}
({\it{x\/}} $\in$ {\rm{listcars}}\,({\it{y\/}})\index{listcars}) $=$ {\rm{definedp}}\,({\it{x\/}}, {\it{y\/}})\index{definedp}
\end{tabbing}


\noindent{\sc Event}:   Disable definedp-implies-member.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  definedp-member-assoc \\ \index{definedp-member-assoc}
{\rm{definedp}}\,({\it{x\/}}, {\it{lst\/}})\index{definedp} $\rightarrow$ ({\rm{assoc}}\,({\it{x\/}}, {\it{lst\/}}) $\in$ {\it{lst\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  definedp-rewrites-to-member \\ \index{definedp-rewrites-to-member}
{\rm{definedp}}\,({\it{x\/}}, {\it{lst\/}})\index{definedp} $=$ ({\it{x\/}} $\in$ {\rm{listcars}}\,({\it{lst\/}})\index{listcars})
\end{tabbing}


\noindent{\sc Event}:   Disable definedp-rewrites-to-member.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  definedp-distributes \\ \index{definedp-distributes}
{\rm{definedp}}\,({\it{x\/}}, {\rm{append}}\,({\it{y\/}}, {\it{z\/}}))\index{definedp} $=$ ({\rm{definedp}}\,({\it{x\/}}, {\it{y\/}})\index{definedp} $\vee$ {\rm{definedp}}\,({\it{x\/}}, {\it{z\/}})\index{definedp})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  definedp-append-preserves-assoc \\ \index{definedp-append-preserves-assoc}
{\rm{definedp}}\,({\it{x\/}}, {\it{y\/}})\index{definedp} $\rightarrow$ ({\rm{assoc}}\,({\it{x\/}}, {\rm{append}}\,({\it{y\/}}, {\it{z\/}})) $=$ {\rm{assoc}}\,({\it{x\/}}, {\it{y\/}}))
\end{tabbing}


\noindent{\sc Event}:   Disable definedp-append-preserves-assoc.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  definedp-once \\ \index{definedp-once}
({\rm{all-cars-unique}}\,({\rm{append}}\,({\it{y\/}}, {\it{z\/}}))\index{all-cars-unique} $\wedge$ {\rm{definedp}}\,({\it{x\/}}, {\it{z\/}})\index{definedp}) $\rightarrow$ ($\neg$ {\rm{definedp}}\,({\it{x\/}}, {\it{y\/}})\index{definedp})
\end{tabbing}


\noindent{\sc Event}:   Disable definedp-once.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  not-definedp-assoc-append \\ \index{not-definedp-assoc-append}
($\neg$ {\rm{definedp}}\,({\it{x\/}}, {\it{y\/}})\index{definedp}) $\rightarrow$ ({\rm{assoc}}\,({\it{x\/}}, {\rm{append}}\,({\it{y\/}}, {\it{z\/}})) $=$ {\rm{assoc}}\,({\it{x\/}}, {\it{z\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  put-preserves-length \\ \index{put-preserves-length}
({\it{y\/}} $<$ {\rm{length}}\,({\it{z\/}})\index{length}) $\rightarrow$ ({\rm{length}}\,({\rm{put}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{put})\index{length} $=$ {\rm{length}}\,({\it{z\/}})\index{length})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  multiple-puts-cancel \\ \index{multiple-puts-cancel}
{\rm{put}}\,({\it{x\/}}, {\it{y\/}}, {\rm{put}}\,({\it{z\/}}, {\it{y\/}}, {\it{w\/}})\index{put})\index{put} $=$ {\rm{put}}\,({\it{x\/}}, {\it{y\/}}, {\it{w\/}})\index{put}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  puts-commute \\ \index{puts-commute}
\=\+(\=\+({\it{y\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{v\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{y\/}} $<$ {\rm{length}}\,({\it{z\/}})\index{length}) \\ 
$\wedge$$\;\;\;\;$({\it{v\/}} $<$ {\rm{length}}\,({\it{z\/}})\index{length}) \\ 
$\wedge$$\;\;\;\;$({\it{v\/}} $\not=$ {\it{y\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{put}}\,({\it{x\/}}, {\it{y\/}}, {\rm{put}}\,({\it{u\/}}, {\it{v\/}}, {\it{z\/}})\index{put})\index{put} $=$ {\rm{put}}\,({\it{u\/}}, {\it{v\/}}, {\rm{put}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{put})\index{put})\-
\end{tabbing}


\noindent{\sc Event}:   Disable puts-commute.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  put-never-shrinks \\ \index{put-never-shrinks}
({\rm{length}}\,({\rm{put}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{put})\index{length} $<$ {\rm{length}}\,({\it{z\/}})\index{length}) $=$ {\bf{f}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  put-value-length-rewrite \\ \index{put-value-length-rewrite}
\=\+({\it{n\/}} $=$ {\rm{length}}\,({\it{lst1\/}})\index{length}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{put}}\,({\it{value\/}}, {\it{n\/}}, {\rm{append}}\,({\it{lst1\/}}, {\rm{cons}}\,({\it{value2\/}}, {\it{lst2\/}})))\index{put} \\ 
$=$$\;\;\;\;${\rm{append}}\,({\it{lst1\/}}, {\rm{cons}}\,({\it{value\/}}, {\it{lst2\/}})))\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable put-value-length-rewrite.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  put-length \\ \index{put-length}
\=\+({\it{n\/}} $=$ {\rm{length}}\,({\it{lst\/}})\index{length}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{put}}\,({\it{x\/}}, {\it{n\/}}, {\rm{append}}\,({\it{lst\/}}, {\rm{cons}}\,({\it{y\/}}, {\it{lst2\/}})))\index{put} $=$ {\rm{append}}\,({\it{lst\/}}, {\rm{cons}}\,({\it{x\/}}, {\it{lst2\/}})))\-
\end{tabbing}


\noindent{\sc Event}:   Disable put-length.

\addvspace{18pt}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                             ;;
;;                         RESTRICT                            ;;
;;                                                             ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Given an alist, select the sub-alist with names in a given list.
;; This will allow me to select out, for example, the sub-alist relating to 
;; the locals or formals.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{restrict} \\  
\=\+{\rm{restrict}}\,({\it{alist\/}}, {\it{names\/}})\index{restrict} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{alist\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf elseif }{\rm{caar}}\,({\it{alist\/}}) $\in$ {\it{names\/}} \\ 
{\bf then }{\rm{cons}}\,({\rm{car}}\,({\it{alist\/}}), {\rm{restrict}}\,({\rm{cdr}}\,({\it{alist\/}}), {\it{names\/}})\index{restrict}) \\ 
{\bf else }{\rm{restrict}}\,({\rm{cdr}}\,({\it{alist\/}}), {\it{names\/}})\index{restrict}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  restriction-nil-names \\ \index{restriction-nil-names}
({\it{names\/}} $\simeq\;${{\bf{nil}}}${}$) $\rightarrow$ ({\rm{restrict}}\,({\it{alist\/}}, {\it{names\/}})\index{restrict} $=$ {\bf{nil}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  no-duplicates-restriction \\ \index{no-duplicates-restriction}
\=\+{\rm{no-duplicates}}\,({\rm{cons}}\,({\it{x\/}}, {\rm{listcars}}\,({\it{alist\/}})\index{listcars}))\index{no-duplicates} \\ 
$\rightarrow$$\;\;\;\;$({\rm{restrict}}\,({\it{alist\/}}, {\rm{cons}}\,({\it{x\/}}, {\it{names\/}}))\index{restrict} $=$ {\rm{restrict}}\,({\it{alist\/}}, {\it{names\/}})\index{restrict})\-
\end{tabbing}


\noindent{\sc Event}:   Disable no-duplicates-restriction.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  restriction-names-cdr \\ \index{restriction-names-cdr}
\=\+(\=\+{\rm{no-duplicates}}\,({\it{names\/}})\index{no-duplicates} \\ 
$\wedge$$\;\;\;\;${\rm{no-duplicates}}\,({\rm{listcars}}\,({\it{alist\/}})\index{listcars})\index{no-duplicates} \\ 
$\wedge$$\;\;\;\;$({\rm{caar}}\,({\it{alist\/}}) $=$ {\rm{car}}\,({\it{names\/}})))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{restrict}}\,({\rm{cdr}}\,({\it{alist\/}}), {\it{names\/}})\index{restrict} $=$ {\rm{restrict}}\,({\rm{cdr}}\,({\it{alist\/}}), {\rm{cdr}}\,({\it{names\/}}))\index{restrict})\-
\end{tabbing}


\noindent{\sc Event}:   Disable restriction-names-cdr.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  restrict-alist-listcars \\ \index{restrict-alist-listcars}
\=\+({\rm{plistp}}\,({\it{alist\/}})\index{plistp} $\wedge$ {\rm{no-duplicates}}\,({\rm{listcars}}\,({\it{alist\/}})\index{listcars})\index{no-duplicates}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{restrict}}\,({\it{alist\/}}, {\rm{listcars}}\,({\it{alist\/}})\index{listcars})\index{restrict} $=$ {\it{alist\/}})\-
\end{tabbing}


\noindent{\sc Event}:   Disable restrict-alist-listcars.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  restrict-listcars-member \\ \index{restrict-listcars-member}
({\it{x\/}} $\not\in$ {\it{y\/}}) $\rightarrow$ ({\it{x\/}} $\not\in$ {\rm{listcars}}\,({\rm{restrict}}\,({\it{lst\/}}, {\it{y\/}})\index{restrict})\index{listcars})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{restriction-induction-hint} \\  
\=\+{\rm{restriction-induction-hint}}\,({\it{alist\/}}, {\it{names1\/}}, {\it{names2\/}})\index{restriction-induction-hint} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{alist\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\rm{caar}}\,({\it{alist\/}}) $\in$ {\it{names1\/}} \\ 
{\bf then }{\rm{restriction-induction-hint}}\,({\rm{cdr}}\,({\it{alist\/}}), {\rm{cdr}}\,({\it{names1\/}}), {\it{names2\/}})\index{restriction-induction-hint} \\ 
{\bf else }{\rm{restriction-induction-hint}}\,({\rm{cdr}}\,({\it{alist\/}}), {\it{names1\/}}, {\rm{cdr}}\,({\it{names2\/}}))\index{restriction-induction-hint}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  listcars-restriction-append \\ \index{listcars-restriction-append}
\=\+(\=\+({\rm{listcars}}\,({\it{alist\/}})\index{listcars} $=$ {\rm{append}}\,({\it{names1\/}}, {\it{names2\/}})) \\ 
$\wedge$$\;\;\;\;${\rm{no-duplicates}}\,({\rm{listcars}}\,({\it{alist\/}})\index{listcars})\index{no-duplicates} \\ 
$\wedge$$\;\;\;\;${\rm{plistp}}\,({\it{alist\/}})\index{plistp})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{append}}\,({\rm{restrict}}\,({\it{alist\/}}, {\it{names1\/}})\index{restrict}, {\rm{restrict}}\,({\it{alist\/}}, {\it{names2\/}})\index{restrict}) $=$ {\it{alist\/}})\-
\end{tabbing}


\noindent{\sc Event}:   Disable listcars-restriction-append.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  restriction-plistp \\ \index{restriction-plistp}
{\rm{plistp}}\,({\rm{restrict}}\,({\it{x\/}}, {\it{y\/}})\index{restrict})\index{plistp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  assoc-restriction \\ \index{assoc-restriction}
({\it{x\/}} $\in$ {\it{y\/}}) $\rightarrow$ ({\rm{assoc}}\,({\it{x\/}}, {\rm{restrict}}\,({\it{z\/}}, {\it{y\/}})\index{restrict}) $=$ {\rm{assoc}}\,({\it{x\/}}, {\it{z\/}}))
\end{tabbing}


\noindent{\sc Event}:   Disable assoc-restriction.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  no-duplicates-append-restrict \\ \index{no-duplicates-append-restrict}
\=\+{\rm{no-duplicates}}\,({\rm{append}}\,({\it{names\/}}, {\rm{listcars}}\,({\it{lst\/}})\index{listcars}))\index{no-duplicates} \\ 
$\rightarrow$$\;\;\;\;$({\rm{restrict}}\,({\rm{append}}\,({\it{x\/}}, {\it{lst\/}}), {\it{names\/}})\index{restrict} $=$ {\rm{restrict}}\,({\it{x\/}}, {\it{names\/}})\index{restrict})\-
\end{tabbing}


\noindent{\sc Event}:   Disable no-duplicates-append-restrict.

\addvspace{18pt}

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

\begin{tabbing}{\sc Theorem}:  restrict-matching-listcars \\ \index{restrict-matching-listcars}
\=\+({\rm{plistp}}\,({\it{lst\/}})\index{plistp} $\wedge$ ({\it{names\/}} $=$ {\rm{listcars}}\,({\it{lst\/}})\index{listcars}) $\wedge$ {\rm{no-duplicates}}\,({\rm{listcars}}\,({\it{lst\/}})\index{listcars})\index{no-duplicates}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{restrict}}\,({\it{lst\/}}, {\it{names\/}})\index{restrict} $=$ {\it{lst\/}})\-
\end{tabbing}


\noindent{\sc Event}:   Disable restrict-matching-listcars.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  restrict-append2 \\ \index{restrict-append2}
\=\+{\rm{no-duplicates}}\,({\rm{append}}\,({\rm{listcars}}\,({\it{lst1\/}})\index{listcars}, {\it{names\/}}))\index{no-duplicates} \\ 
$\rightarrow$$\;\;\;\;$({\rm{restrict}}\,({\rm{append}}\,({\it{lst1\/}}, {\it{lst2\/}}), {\it{names\/}})\index{restrict} $=$ {\rm{restrict}}\,({\it{lst2\/}}, {\it{names\/}})\index{restrict})\-
\end{tabbing}


\noindent{\sc Event}:   Disable restrict-append2.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  restrict-restricts-listcars \\ \index{restrict-restricts-listcars}
({\it{x\/}} $\not\in$ {\rm{listcars}}\,({\it{y\/}})\index{listcars}) $\rightarrow$ ({\it{x\/}} $\not\in$ {\rm{listcars}}\,({\rm{restrict}}\,({\it{y\/}}, {\it{z\/}})\index{restrict})\index{listcars})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  restriction-cdr \\ \index{restriction-cdr}
\=\+({\rm{listp}}\,({\it{y\/}}) $\wedge$ ({\rm{car}}\,({\it{y\/}}) $\not\in$ {\rm{listcars}}\,({\it{x\/}})\index{listcars})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{restrict}}\,({\it{x\/}}, {\it{y\/}})\index{restrict} $=$ {\rm{restrict}}\,({\it{x\/}}, {\rm{cdr}}\,({\it{y\/}}))\index{restrict})\-
\end{tabbing}


\noindent{\sc Event}:   Disable restriction-cdr.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  restrict-append \\ \index{restrict-append}
\=\+({\rm{listp}}\,({\it{y\/}}) $\wedge$ ({\rm{listcars}}\,({\it{x\/}})\index{listcars} $=$ {\rm{append}}\,({\it{y\/}}, {\it{z\/}})) $\wedge$ {\rm{all-cars-unique}}\,({\it{x\/}})\index{all-cars-unique}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{restrict}}\,({\it{x\/}}, {\it{y\/}})\index{restrict} $=$ {\rm{cons}}\,({\rm{car}}\,({\it{x\/}}), {\rm{restrict}}\,({\rm{cdr}}\,({\it{x\/}}), {\rm{cdr}}\,({\it{y\/}}))\index{restrict}))\-
\end{tabbing}


\noindent{\sc Event}:   Disable restrict-append.

\addvspace{18pt}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                             ;;
;;                       SIGNATURES                            ;;
;;                                                             ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{signatures-match} \\  
\=\+{\rm{signatures-match}}\,({\it{alist1\/}}, {\it{alist2\/}})\index{signatures-match} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{alist1\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\it{alist2\/}} $=$ {\bf{nil}} \\ 
{\bf else }\=\+({\rm{caar}}\,({\it{alist1\/}}) $=$ {\rm{caar}}\,({\it{alist2\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{cadr}}\,({\rm{car}}\,({\it{alist1\/}})) $=$ {\rm{cadr}}\,({\rm{car}}\,({\it{alist2\/}}))) \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{cdr}}\,({\it{alist1\/}}), {\rm{cdr}}\,({\it{alist2\/}}))\index{signatures-match}\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  signatures-match-reflexive \\ \index{signatures-match-reflexive}
{\rm{plistp}}\,({\it{lst\/}})\index{plistp} $\rightarrow$ {\rm{signatures-match}}\,({\it{lst\/}}, {\it{lst\/}})\index{signatures-match}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  signatures-match-reflexive1 \\ \index{signatures-match-reflexive1}
{\rm{signatures-match}}\,({\it{lst\/}}, {\it{lst\/}})\index{signatures-match} $=$ {\rm{plistp}}\,({\it{lst\/}})\index{plistp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  signatures-match-symmetric \\ \index{signatures-match-symmetric}
\=\+({\rm{plistp}}\,({\it{lst1\/}})\index{plistp} $\wedge$ {\rm{signatures-match}}\,({\it{lst1\/}}, {\it{lst2\/}})\index{signatures-match}) \\ 
$\rightarrow$$\;\;\;\;${\rm{signatures-match}}\,({\it{lst2\/}}, {\it{lst1\/}})\index{signatures-match}\-
\end{tabbing}


\noindent{\sc Event}:   Disable signatures-match-symmetric.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  signatures-match-transitive \\ \index{signatures-match-transitive}
\=\+(\=\+{\rm{plistp}}\,({\it{lst1\/}})\index{plistp} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\it{lst1\/}}, {\it{lst2\/}})\index{signatures-match} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\it{lst2\/}}, {\it{lst3\/}})\index{signatures-match})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{signatures-match}}\,({\it{lst1\/}}, {\it{lst3\/}})\index{signatures-match}\-
\end{tabbing}


\noindent{\sc Event}:   Disable signatures-match-transitive.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  signatures-match-listp \\ \index{signatures-match-listp}
({\rm{signatures-match}}\,({\it{x\/}}, {\it{y\/}})\index{signatures-match} $\wedge$ {\rm{listp}}\,({\it{x\/}})) $\rightarrow$ {\rm{listp}}\,({\it{y\/}})
\end{tabbing}


\noindent{\sc Event}:   Disable signatures-match-listp.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  signatures-match-listcars \\ \index{signatures-match-listcars}
{\rm{signatures-match}}\,({\it{x\/}}, {\it{y\/}})\index{signatures-match} $\rightarrow$ ({\rm{listcars}}\,({\it{y\/}})\index{listcars} $=$ {\rm{listcars}}\,({\it{x\/}})\index{listcars})
\end{tabbing}


\noindent{\sc Event}:   Disable signatures-match-listcars.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  signatures-match-append1 \\ \index{signatures-match-append1}
\=\+({\rm{signatures-match}}\,({\it{lst1\/}}, {\it{lst3\/}})\index{signatures-match} $\wedge$ {\rm{signatures-match}}\,({\it{lst2\/}}, {\it{lst4\/}})\index{signatures-match}) \\ 
$\rightarrow$$\;\;\;\;${\rm{signatures-match}}\,({\rm{append}}\,({\it{lst1\/}}, {\it{lst2\/}}), {\rm{append}}\,({\it{lst3\/}}, {\it{lst4\/}}))\index{signatures-match}\-
\end{tabbing}


\noindent{\sc Event}:   Disable signatures-match-append1.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  signatures-match-reorder \\ \index{signatures-match-reorder}
\=\+(\=\+{\rm{plistp}}\,({\it{alist1\/}})\index{plistp} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\it{alist1\/}}, {\it{alist3\/}})\index{signatures-match} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\it{alist1\/}}, {\it{alist2\/}})\index{signatures-match})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{signatures-match}}\,({\it{alist2\/}}, {\it{alist3\/}})\index{signatures-match}\-
\end{tabbing}


\noindent{\sc Event}:   Disable signatures-match-reorder.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{signature} \\  
\=\+{\rm{signature}}\,({\it{mg-vars-list\/}})\index{signature} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{mg-vars-list\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{cons}}\,(\=\+{\rm{list}}\,({\rm{caar}}\,({\it{mg-vars-list\/}}), {\rm{cadar}}\,({\it{mg-vars-list\/}})), \\ 
{\rm{signature}}\,({\rm{cdr}}\,({\it{mg-vars-list\/}}))\index{signature})\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  signatures-match-listcars-equal \\ \index{signatures-match-listcars-equal}
{\rm{signatures-match}}\,({\it{x\/}}, {\it{y\/}})\index{signatures-match} $\rightarrow$ ({\rm{listcars}}\,({\it{y\/}})\index{listcars} $=$ {\rm{listcars}}\,({\it{x\/}})\index{listcars})
\end{tabbing}


\noindent{\sc Event}:   Disable signatures-match-listcars-equal.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  signatures-match-preserves-uniqueness-of-cars \\ \index{signatures-match-preserves-uniq!ueness-of-cars}
({\rm{signatures-match}}\,({\it{x\/}}, {\it{y\/}})\index{signatures-match} $\wedge$ {\rm{all-cars-unique}}\,({\it{x\/}})\index{all-cars-unique}) $\rightarrow$ {\rm{all-cars-unique}}\,({\it{y\/}})\index{all-cars-unique}
\end{tabbing}


\noindent{\sc Event}:   Disable signatures-match-preserves-uniqueness-of-cars.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  signature-restrict-commute \\ \index{signature-restrict-commute}
{\rm{signature}}\,({\rm{restrict}}\,({\it{alist\/}}, {\it{names\/}})\index{restrict})\index{signature} $=$ {\rm{restrict}}\,({\rm{signature}}\,({\it{alist\/}})\index{signature}, {\it{names\/}})\index{restrict}
\end{tabbing}


\noindent{\sc Event}:   Disable signature-restrict-commute.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  signatures-match-restrict \\ \index{signatures-match-restrict}
{\rm{signatures-match}}\,({\it{x\/}}, {\it{y\/}})\index{signatures-match} $\rightarrow$ {\rm{signatures-match}}\,({\rm{restrict}}\,({\it{x\/}}, {\it{z\/}})\index{restrict}, {\rm{restrict}}\,({\it{y\/}}, {\it{z\/}})\index{restrict})\index{signatures-match}
\end{tabbing}


\noindent{\sc Event}:   Disable signatures-match-restrict.

\addvspace{18pt}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                             ;;
;;                         DISJOINT                            ;;
;;                                                             ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{one-way-disjoint} \\  
\=\+{\rm{one-way-disjoint}}\,({\it{lst1\/}}, {\it{lst2\/}})\index{one-way-disjoint} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{lst1\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }({\rm{car}}\,({\it{lst1\/}}) $\not\in$ {\it{lst2\/}}) $\wedge$ {\rm{one-way-disjoint}}\,({\rm{cdr}}\,({\it{lst1\/}}), {\it{lst2\/}})\index{one-way-disjoint}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{disjoint} \\  
\=\+{\rm{disjoint}}\,({\it{lst1\/}}, {\it{lst2\/}})\index{disjoint} \\ 
$=$$\;\;\;\;$({\rm{one-way-disjoint}}\,({\it{lst1\/}}, {\it{lst2\/}})\index{one-way-disjoint} $\wedge$ {\rm{one-way-disjoint}}\,({\it{lst2\/}}, {\it{lst1\/}})\index{one-way-disjoint})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  disjoint-nil \\ \index{disjoint-nil}
{\rm{disjoint}}\,({\it{x\/}}, {\bf{nil}})\index{disjoint} $\wedge$ {\rm{disjoint}}\,({\bf{nil}}, {\it{x\/}})\index{disjoint}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  cons-preserves-one-way-disjoint2 \\ \index{cons-preserves-one-way-disjoint!2}
{\rm{one-way-disjoint}}\,({\it{lst2\/}}, {\rm{cons}}\,({\it{x\/}}, {\it{lst\/}}))\index{one-way-disjoint} $\rightarrow$ {\rm{one-way-disjoint}}\,({\it{lst2\/}}, {\it{lst\/}})\index{one-way-disjoint}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  cdr-preserves-disjoint \\ \index{cdr-preserves-disjoint}
{\rm{disjoint}}\,({\rm{cons}}\,({\it{x\/}}, {\it{lst\/}}), {\it{lst2\/}})\index{disjoint} $\rightarrow$ {\rm{disjoint}}\,({\it{lst\/}}, {\it{lst2\/}})\index{disjoint}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  no-duplicates-append-implies-one-way-disjoint \\ \index{no-duplicates-append-implies-one!-way-disjoint}
{\rm{no-duplicates}}\,({\rm{append}}\,({\it{x\/}}, {\it{y\/}}))\index{no-duplicates} $\rightarrow$ {\rm{one-way-disjoint}}\,({\it{x\/}}, {\it{y\/}})\index{one-way-disjoint}
\end{tabbing}


\noindent{\sc Event}:   Disable no-duplicates-append-implies-one-way-disjoint.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  right-cdr-preserves-one-way-disjoint \\ \index{right-cdr-preserves-one-way-dis!joint}
({\rm{one-way-disjoint}}\,({\it{x\/}}, {\it{y\/}})\index{one-way-disjoint} $\wedge$ {\rm{listp}}\,({\it{y\/}})) $\rightarrow$ {\rm{one-way-disjoint}}\,({\it{x\/}}, {\rm{cdr}}\,({\it{y\/}}))\index{one-way-disjoint}
\end{tabbing}


\noindent{\sc Event}:   Disable right-cdr-preserves-one-way-disjoint.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  disjoint-preserves-no-duplicates \\ \index{disjoint-preserves-no-duplicate!s}
\=\+({\rm{no-duplicates}}\,({\it{lst1\/}})\index{no-duplicates} $\wedge$ {\rm{no-duplicates}}\,({\it{lst2\/}})\index{no-duplicates} $\wedge$ {\rm{disjoint}}\,({\it{lst1\/}}, {\it{lst2\/}})\index{disjoint}) \\ 
$\rightarrow$$\;\;\;\;${\rm{no-duplicates}}\,({\rm{append}}\,({\it{lst1\/}}, {\it{lst2\/}}))\index{no-duplicates}\-
\end{tabbing}


\noindent{\sc Event}:   Disable disjoint-preserves-no-duplicates.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  one-way-disjoint-right-cons \\ \index{one-way-disjoint-right-cons}
\=\+({\rm{one-way-disjoint}}\,({\it{lst1\/}}, {\it{lst2\/}})\index{one-way-disjoint} $\wedge$ ({\it{x\/}} $\not\in$ {\it{lst1\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{one-way-disjoint}}\,({\it{lst1\/}}, {\rm{cons}}\,({\it{x\/}}, {\it{lst2\/}}))\index{one-way-disjoint}\-
\end{tabbing}


\noindent{\sc Event}:   Disable one-way-disjoint-right-cons.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  disjoint-right-cons \\ \index{disjoint-right-cons}
({\rm{disjoint}}\,({\it{lst1\/}}, {\it{lst2\/}})\index{disjoint} $\wedge$ ({\it{x\/}} $\not\in$ {\it{lst1\/}})) $\rightarrow$ {\rm{disjoint}}\,({\it{lst1\/}}, {\rm{cons}}\,({\it{x\/}}, {\it{lst2\/}}))\index{disjoint}
\end{tabbing}       


\noindent{\sc Event}:   Disable disjoint-right-cons.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  one-way-disjoint-right-cdr \\ \index{one-way-disjoint-right-cdr}
\=\+({\rm{listp}}\,({\it{lst2\/}}) $\wedge$ {\rm{one-way-disjoint}}\,({\it{lst1\/}}, {\it{lst2\/}})\index{one-way-disjoint}) \\ 
$\rightarrow$$\;\;\;\;${\rm{one-way-disjoint}}\,({\it{lst1\/}}, {\rm{cdr}}\,({\it{lst2\/}}))\index{one-way-disjoint}\-
\end{tabbing}


\noindent{\sc Event}:   Disable one-way-disjoint-right-cdr.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  disjoint-right-cdr \\ \index{disjoint-right-cdr}
({\rm{listp}}\,({\it{lst2\/}}) $\wedge$ {\rm{disjoint}}\,({\it{lst1\/}}, {\it{lst2\/}})\index{disjoint}) $\rightarrow$ {\rm{disjoint}}\,({\it{lst1\/}}, {\rm{cdr}}\,({\it{lst2\/}}))\index{disjoint}
\end{tabbing}


\noindent{\sc Event}:   Disable disjoint-right-cdr.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  disjoint-right-append \\ \index{disjoint-right-append}
\=\+({\rm{disjoint}}\,({\it{lst1\/}}, {\it{lst2\/}})\index{disjoint} $\wedge$ {\rm{disjoint}}\,({\it{lst1\/}}, {\it{lst3\/}})\index{disjoint}) \\ 
$\rightarrow$$\;\;\;\;${\rm{disjoint}}\,({\it{lst1\/}}, {\rm{append}}\,({\it{lst2\/}}, {\it{lst3\/}}))\index{disjoint}\-
\end{tabbing}


\noindent{\sc Event}:   Disable disjoint-right-append.

\addvspace{18pt}


\noindent{\sc Event}:   Disable disjoint.

\addvspace{18pt}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                             ;;
;;                       COND-SUBSETP                          ;;
;;                                                             ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{cond-subsetp} \\  
\=\+{\rm{cond-subsetp}}\,({\it{lst1\/}}, {\it{lst2\/}})\index{cond-subsetp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{lst1\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }\=\+({\rm{car}}\,({\it{lst1\/}}) $\in$ {\rm{cons}}\,({\tt{'}}{\tt{leave}}, {\rm{cons}}\,({\tt{'}}{\tt{routineerror}}, {\it{lst2\/}}))) \\ 
$\wedge$$\;\;\;\;${\rm{cond-subsetp}}\,({\rm{cdr}}\,({\it{lst1\/}}), {\it{lst2\/}})\index{cond-subsetp}\-$\;${\bf  endif}\-\-
\end{tabbing}

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


\noindent{\sc Event}:   Disable cond-subsetp-append.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  subsetp-implies-cond-subsetp \\ \index{subsetp-implies-cond-subsetp}
{\rm{subset}}\,({\it{x\/}}, {\it{y\/}})\index{subset} $\rightarrow$ {\rm{cond-subsetp}}\,({\it{x\/}}, {\it{y\/}})\index{cond-subsetp}
\end{tabbing}


\noindent{\sc Event}:   Disable subsetp-implies-cond-subsetp.

\addvspace{18pt}


\noindent{\sc Event}:   Make the library {\tt{"c1"}}.

\addvspace{18pt}

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