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

\addvspace{18pt}

\begin{verbatim};; Sets; Matt Kaufmann, Dec. 1989, revised March 1990.  The first few events
;; are some basic events about lists.  I'll take the approach that all these
;; basic functions will be disabled once enough algebraic properties have
;; been proved.

;; Theories:

;; (deftheory set-defns
;;  (length properp fix-properp member append subsetp delete
;;          disjoint intersection set-diff setp))

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

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

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

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


\noindent{\sc Event}:   Disable length.

\addvspace{18pt}

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

\begin{tabbing}{\sc Theorem}:  member-nlistp \\ \index{member-nlistp}
({\it{l\/}} $\simeq\;${{\bf{nil}}}${}$) $\rightarrow$ ({\it{a\/}} $\not\in$ {\it{l\/}})
\end{tabbing}


\noindent{\sc Event}:   Disable member.

\addvspace{18pt}

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

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

\begin{tabbing}{\sc Theorem}:  subsetp-wit-witnesses \\ \index{subsetp-wit-witnesses}
\=\+{\rm{subsetp}}\,({\it{x\/}}, {\it{y\/}})\index{subsetp} \\ 
$=$$\;\;\;\;$($\neg$ (({\rm{subsetp-wit}}\,({\it{x\/}}, {\it{y\/}})\index{subsetp-wit} $\in$ {\it{x\/}}) $\wedge$ ({\rm{subsetp-wit}}\,({\it{x\/}}, {\it{y\/}})\index{subsetp-wit} $\not\in$ {\it{y\/}})))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subsetp-wit-witnesses-general-1 \\ \index{subsetp-wit-witnesses-general-1}
(({\rm{subsetp-wit}}\,({\it{x\/}}, {\it{y\/}})\index{subsetp-wit} $\not\in$ {\it{x\/}}) $\wedge$ ({\it{a\/}} $\in$ {\it{x\/}})) $\rightarrow$ ({\it{a\/}} $\in$ {\it{y\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subsetp-wit-witnesses-general-2 \\ \index{subsetp-wit-witnesses-general-2}
(({\rm{subsetp-wit}}\,({\it{x\/}}, {\it{y\/}})\index{subsetp-wit} $\in$ {\it{y\/}}) $\wedge$ ({\it{a\/}} $\in$ {\it{x\/}})) $\rightarrow$ ({\it{a\/}} $\in$ {\it{y\/}})
\end{tabbing}


\noindent{\sc Event}:   Disable subsetp-wit-witnesses.

\addvspace{18pt}

\noindent{\sc Event}:   Disable subsetp-wit-witnesses-general-1.

\addvspace{18pt}

\noindent{\sc Event}:   Disable subsetp-wit-witnesses-general-2.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  subsetp-cons-1 \\ \index{subsetp-cons-1}
{\rm{subsetp}}\,({\rm{cons}}\,({\it{a\/}}, {\it{x\/}}), {\it{y\/}})\index{subsetp} $=$ (({\it{a\/}} $\in$ {\it{y\/}}) $\wedge$ {\rm{subsetp}}\,({\it{x\/}}, {\it{y\/}})\index{subsetp})
\end{tabbing}

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

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

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

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

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

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

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

\begin{tabbing}{\sc Theorem}:  subsetp-of-append-sufficiency \\ \index{subsetp-of-append-sufficiency}
({\rm{subsetp}}\,({\it{a\/}}, {\it{b\/}})\index{subsetp} $\vee$ {\rm{subsetp}}\,({\it{a\/}}, {\it{c\/}})\index{subsetp}) $\rightarrow$ {\rm{subsetp}}\,({\it{a\/}}, {\rm{append}}\,({\it{b\/}}, {\it{c\/}}))\index{subsetp}
\end{tabbing}

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

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


\noindent{\sc Event}:   Disable subsetp.

\addvspace{18pt}

\begin{verbatim};;;;; Other set-theoretic and list-theoretic definitions, and properp observations.

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

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

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

\begin{tabbing}{\sc Theorem}:  fix-properp-properp \\ \index{fix-properp-properp}
{\rm{properp}}\,({\it{x\/}})\index{properp} $\rightarrow$ ({\rm{fix-properp}}\,({\it{x\/}})\index{fix-properp} $=$ {\it{x\/}})
\end{tabbing}

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

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

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

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

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

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

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

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

\begin{tabbing}{\sc Theorem}:  properp-delete \\ \index{properp-delete}
{\rm{properp}}\,({\rm{delete}}\,({\it{x\/}}, {\it{l\/}})\index{delete})\index{properp} $=$ {\rm{properp}}\,({\it{l\/}})\index{properp}
\end{tabbing}

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

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

\begin{tabbing}{\sc Theorem}:  disjoint-wit-witnesses \\ \index{disjoint-wit-witnesses}
\=\+{\rm{disjoint}}\,({\it{x\/}}, {\it{y\/}})\index{disjoint} \\ 
$=$$\;\;\;\;$($\neg$ (({\rm{disjoint-wit}}\,({\it{x\/}}, {\it{y\/}})\index{disjoint-wit} $\in$ {\it{x\/}}) $\wedge$ ({\rm{disjoint-wit}}\,({\it{x\/}}, {\it{y\/}})\index{disjoint-wit} $\in$ {\it{y\/}})))\-
\end{tabbing}


\noindent{\sc Event}:   Disable disjoint-wit.

\addvspace{18pt}


\noindent{\sc Event}:   Disable disjoint-wit-witnesses.

\addvspace{18pt}

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

\begin{tabbing}{\sc Theorem}:  properp-intersection \\ \index{properp-intersection}
{\rm{properp}}\,({\rm{intersection}}\,({\it{x\/}}, {\it{y\/}})\index{intersection})\index{properp}
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  properp-set-diff \\ \index{properp-set-diff}
{\rm{properp}}\,({\rm{set-diff}}\,({\it{x\/}}, {\it{y\/}})\index{set-diff})\index{properp}
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  setp-implies-properp \\ \index{setp-implies-properp}
{\rm{setp}}\,({\it{x\/}})\index{setp} $\rightarrow$ {\rm{properp}}\,({\it{x\/}})\index{properp}
\end{tabbing}


\noindent{\sc Event}:   Disable properp.

\addvspace{18pt}


\noindent{\sc Event}:   Let us define the theory {\it{set-defns}} to consist of the following events: length,
properp,
fix-properp,
member,
append,
subsetp,
delete,
disjoint,
intersection,
set-diff,
setp,
properp.\index{set-defns}

\addvspace{18pt}

\begin{verbatim};; Set theory lemmas

\end{verbatim}\begin{tabbing}{\sc Theorem}:  delete-cons \\ \index{delete-cons}
\=\+{\rm{delete}}\,({\it{a\/}}, {\rm{cons}}\,({\it{b\/}}, {\it{x\/}}))\index{delete} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{a\/}} $=$ {\it{b\/}}$\;\;${\bf then }{\it{x\/}} \\ 
{\bf else }{\rm{cons}}\,({\it{b\/}}, {\rm{delete}}\,({\it{a\/}}, {\it{x\/}})\index{delete})$\;${\bf  endif}\-\-
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  listp-delete \\ \index{listp-delete}
\=\+{\rm{listp}}\,({\rm{delete}}\,({\it{x\/}}, {\it{l\/}})\index{delete}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{l\/}})$\;\;${\bf then }({\it{x\/}} $\not=$ {\rm{car}}\,({\it{l\/}})) $\vee$ {\rm{listp}}\,({\rm{cdr}}\,({\it{l\/}})) \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}

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

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

\begin{tabbing}{\sc Theorem}:  member-delete \\ \index{member-delete}
{\rm{setp}}\,({\it{x\/}})\index{setp} $\rightarrow$ (({\it{a\/}} $\in$ {\rm{delete}}\,({\it{b\/}}, {\it{x\/}})\index{delete}) $=$ (({\it{a\/}} $\not=$ {\it{b\/}}) $\wedge$ ({\it{a\/}} $\in$ {\it{x\/}})))
\end{tabbing}		       

\begin{tabbing}{\sc Theorem}:  setp-delete \\ \index{setp-delete}
{\rm{setp}}\,({\it{x\/}})\index{setp} $\rightarrow$ {\rm{setp}}\,({\rm{delete}}\,({\it{a\/}}, {\it{x\/}})\index{delete})\index{setp}
\end{tabbing}


\noindent{\sc Event}:   Disable delete.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  disjoint-cons-1 \\ \index{disjoint-cons-1}
{\rm{disjoint}}\,({\rm{cons}}\,({\it{a\/}}, {\it{x\/}}), {\it{y\/}})\index{disjoint} $=$ (({\it{a\/}} $\not\in$ {\it{y\/}}) $\wedge$ {\rm{disjoint}}\,({\it{x\/}}, {\it{y\/}})\index{disjoint})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  disjoint-cons-2 \\ \index{disjoint-cons-2}
{\rm{disjoint}}\,({\it{x\/}}, {\rm{cons}}\,({\it{a\/}}, {\it{y\/}}))\index{disjoint} $=$ (({\it{a\/}} $\not\in$ {\it{x\/}}) $\wedge$ {\rm{disjoint}}\,({\it{x\/}}, {\it{y\/}})\index{disjoint})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  disjoint-nlistp \\ \index{disjoint-nlistp}
(({\it{x\/}} $\simeq\;${{\bf{nil}}}${}$) $\vee$ ({\it{y\/}} $\simeq\;${{\bf{nil}}}${}$)) $\rightarrow$ {\rm{disjoint}}\,({\it{x\/}}, {\it{y\/}})\index{disjoint}
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  disjoint-append-right \\ \index{disjoint-append-right}
{\rm{disjoint}}\,({\it{u\/}}, {\rm{append}}\,({\it{y\/}}, {\it{z\/}}))\index{disjoint} $=$ ({\rm{disjoint}}\,({\it{u\/}}, {\it{y\/}})\index{disjoint} $\wedge$ {\rm{disjoint}}\,({\it{u\/}}, {\it{z\/}})\index{disjoint})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  disjoint-append-left \\ \index{disjoint-append-left}
{\rm{disjoint}}\,({\rm{append}}\,({\it{y\/}}, {\it{z\/}}), {\it{u\/}})\index{disjoint} $=$ ({\rm{disjoint}}\,({\it{y\/}}, {\it{u\/}})\index{disjoint} $\wedge$ {\rm{disjoint}}\,({\it{z\/}}, {\it{u\/}})\index{disjoint})
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  disjoint-subsetp-monotone-second \\ \index{disjoint-subsetp-monotone-secon!d}
({\rm{subsetp}}\,({\it{y\/}}, {\it{z\/}})\index{subsetp} $\wedge$ {\rm{disjoint}}\,({\it{x\/}}, {\it{z\/}})\index{disjoint}) $\rightarrow$ {\rm{disjoint}}\,({\it{x\/}}, {\it{y\/}})\index{disjoint}
\end{tabbing}

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

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

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


\noindent{\sc Event}:   Disable disjoint.

\addvspace{18pt}

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

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

\begin{tabbing}{\sc Theorem}:  member-intersection \\ \index{member-intersection}
({\it{a\/}} $\in$ {\rm{intersection}}\,({\it{x\/}}, {\it{y\/}})\index{intersection}) $=$ (({\it{a\/}} $\in$ {\it{x\/}}) $\wedge$ ({\it{a\/}} $\in$ {\it{y\/}}))
\end{tabbing}

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

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

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

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

\begin{verbatim};; The following is needed because DISJOINT-INTERSECTION-COMMUTER,
;; added during polishing, caused the proof of
;; DISJOINT-DOMAIN-CO-RESTRICT (in "alists.events") to fail.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  intersection-cons-3 \\ \index{intersection-cons-3}
\=\+({\it{w\/}} $\in$ {\it{x\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{subsetp}}\,({\rm{intersection}}\,({\it{y\/}}, {\rm{cons}}\,({\it{w\/}}, {\it{z\/}}))\index{intersection}, {\it{x\/}})\index{subsetp} \\ 
$=$$\;\;\;\;${\rm{subsetp}}\,({\rm{intersection}}\,({\it{y\/}}, {\it{z\/}})\index{intersection}, {\it{x\/}})\index{subsetp})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  intersection-cons-subsetp \\ \index{intersection-cons-subsetp}
{\rm{subsetp}}\,({\rm{intersection}}\,({\it{x\/}}, {\it{y\/}})\index{intersection}, {\rm{intersection}}\,({\it{x\/}}, {\rm{cons}}\,({\it{a\/}}, {\it{y\/}}))\index{intersection})\index{subsetp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subsetp-intersection-left-1 \\ \index{subsetp-intersection-left-1}
{\rm{subsetp}}\,({\rm{intersection}}\,({\it{x\/}}, {\it{y\/}})\index{intersection}, {\it{x\/}})\index{subsetp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subsetp-intersection-left-2 \\ \index{subsetp-intersection-left-2}
{\rm{subsetp}}\,({\rm{intersection}}\,({\it{x\/}}, {\it{y\/}})\index{intersection}, {\it{y\/}})\index{subsetp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subsetp-intersection-sufficiency-1 \\ \index{subsetp-intersection-sufficienc!y-1}
{\rm{subsetp}}\,({\it{y\/}}, {\it{z\/}})\index{subsetp} $\rightarrow$ {\rm{subsetp}}\,({\rm{intersection}}\,({\it{x\/}}, {\it{y\/}})\index{intersection}, {\it{z\/}})\index{subsetp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subsetp-intersection-sufficiency-2 \\ \index{subsetp-intersection-sufficienc!y-2}
{\rm{subsetp}}\,({\it{y\/}}, {\it{z\/}})\index{subsetp} $\rightarrow$ {\rm{subsetp}}\,({\rm{intersection}}\,({\it{y\/}}, {\it{x\/}})\index{intersection}, {\it{z\/}})\index{subsetp}
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  intersection-elimination \\ \index{intersection-elimination}
{\rm{subsetp}}\,({\it{x\/}}, {\it{y\/}})\index{subsetp} $\rightarrow$ ({\rm{intersection}}\,({\it{x\/}}, {\it{y\/}})\index{intersection} $=$ {\rm{fix-properp}}\,({\it{x\/}})\index{fix-properp})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  length-intersection \\ \index{length-intersection}
{\rm{length}}\,({\it{x\/}})\index{length} $\not<$ {\rm{length}}\,({\rm{intersection}}\,({\it{x\/}}, {\it{y\/}})\index{intersection})\index{length}
\end{tabbing}

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

\begin{verbatim};; The following wasn't needed in the proof about generalization, but it's a nice rule.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  intersection-append \\ \index{intersection-append}
{\rm{intersection}}\,({\rm{append}}\,({\it{x\/}}, {\it{y\/}}), {\it{z\/}})\index{intersection} $=$ {\rm{append}}\,({\rm{intersection}}\,({\it{x\/}}, {\it{z\/}})\index{intersection}, {\rm{intersection}}\,({\it{y\/}}, {\it{z\/}})\index{intersection})
\end{tabbing}

\begin{verbatim};; I'd rather just prove that intersection distributes over append on
;; the right but that isn't true.  Congruence relations would probably
;; help a lot with that problem.  In the meantime, I content myself
;; with the following.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  disjoint-intersection-append \\ \index{disjoint-intersection-append}
\=\+{\rm{disjoint}}\,({\it{x\/}}, {\rm{intersection}}\,({\it{y\/}}, {\rm{append}}\,({\it{z1\/}}, {\it{z2\/}}))\index{intersection})\index{disjoint} \\ 
$=$$\;\;\;\;$({\rm{disjoint}}\,({\it{x\/}}, {\rm{intersection}}\,({\it{y\/}}, {\it{z1\/}})\index{intersection})\index{disjoint} $\wedge$ {\rm{disjoint}}\,({\it{x\/}}, {\rm{intersection}}\,({\it{y\/}}, {\it{z2\/}})\index{intersection})\index{disjoint})\-
\end{tabbing}

\begin{verbatim};; See comment just above DISJOINT-INTERSECTION-APPEND
\end{verbatim}\begin{tabbing}{\sc Theorem}:  subsetp-intersection-append \\ \index{subsetp-intersection-append}
\=\+{\rm{subsetp}}\,({\rm{intersection}}\,({\it{u\/}}, {\rm{append}}\,({\it{x\/}}, {\it{y\/}}))\index{intersection}, {\it{z\/}})\index{subsetp} \\ 
$=$$\;\;\;\;$({\rm{subsetp}}\,({\rm{intersection}}\,({\it{u\/}}, {\it{x\/}})\index{intersection}, {\it{z\/}})\index{subsetp} $\wedge$ {\rm{subsetp}}\,({\rm{intersection}}\,({\it{u\/}}, {\it{y\/}})\index{intersection}, {\it{z\/}})\index{subsetp})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subsetp-intersection-elimination-lemma \\ \index{subsetp-intersection-eliminatio!n-lemma}
\=\+({\rm{subsetp}}\,({\it{y\/}}, {\it{x\/}})\index{subsetp} $\wedge$ ($\neg$ {\rm{subsetp}}\,({\it{y\/}}, {\it{z\/}})\index{subsetp})) \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{subsetp}}\,({\rm{intersection}}\,({\it{x\/}}, {\it{y\/}})\index{intersection}, {\it{z\/}})\index{subsetp})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subsetp-intersection-elimination \\ \index{subsetp-intersection-eliminatio!n}
{\rm{subsetp}}\,({\it{y\/}}, {\it{x\/}})\index{subsetp} $\rightarrow$ ({\rm{subsetp}}\,({\rm{intersection}}\,({\it{x\/}}, {\it{y\/}})\index{intersection}, {\it{z\/}})\index{subsetp} $\leftrightarrow$ {\rm{subsetp}}\,({\it{y\/}}, {\it{z\/}})\index{subsetp})
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  subsetp-intersection-monotone-1 \\ \index{subsetp-intersection-monotone-1}
\=\+({\rm{subsetp}}\,({\rm{intersection}}\,({\it{x\/}}, {\it{y\/}})\index{intersection}, {\it{z\/}})\index{subsetp} $\wedge$ {\rm{subsetp}}\,({\it{x1\/}}, {\it{x\/}})\index{subsetp}) \\ 
$\rightarrow$$\;\;\;\;${\rm{subsetp}}\,({\rm{intersection}}\,({\it{x1\/}}, {\it{y\/}})\index{intersection}, {\it{z\/}})\index{subsetp}\-
\end{tabbing}

\begin{verbatim};; The lemma SUBSETP-INTERSECTION-MONOTONE-2 below was added during
;; polishing of the final proof in "generalize.events", since the
;; lemma immediately above wasn't enough at that point.  Actually
;; I realized at this point that intersection commutes from the point
;; of view of subsetp:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  subsetp-intersection-commuter \\ \index{subsetp-intersection-commuter}
{\rm{subsetp}}\,({\rm{intersection}}\,({\it{x\/}}, {\it{y\/}})\index{intersection}, {\it{z\/}})\index{subsetp} $=$ {\rm{subsetp}}\,({\rm{intersection}}\,({\it{y\/}}, {\it{x\/}})\index{intersection}, {\it{z\/}})\index{subsetp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subsetp-intersection-monotone-2 \\ \index{subsetp-intersection-monotone-2}
\=\+({\rm{subsetp}}\,({\rm{intersection}}\,({\it{y\/}}, {\it{x\/}})\index{intersection}, {\it{z\/}})\index{subsetp} $\wedge$ {\rm{subsetp}}\,({\it{x1\/}}, {\it{x\/}})\index{subsetp}) \\ 
$\rightarrow$$\;\;\;\;${\rm{subsetp}}\,({\rm{intersection}}\,({\it{x1\/}}, {\it{y\/}})\index{intersection}, {\it{z\/}})\index{subsetp}\-
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  disjoint-intersection3 \\ \index{disjoint-intersection3}
\=\+{\rm{disjoint}}\,({\it{free\/}}, {\rm{intersection}}\,({\it{vars\/}}, {\it{x\/}})\index{intersection})\index{disjoint} \\ 
$\rightarrow$$\;\;\;\;$({\rm{intersection}}\,({\it{x\/}}, {\rm{intersection}}\,({\it{vars\/}}, {\it{free\/}})\index{intersection})\index{intersection} $=$ {\bf{nil}})\-
\end{tabbing}


\noindent{\sc Event}:   Disable intersection.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  member-set-diff \\ \index{member-set-diff}
({\it{a\/}} $\in$ {\rm{set-diff}}\,({\it{y\/}}, {\it{z\/}})\index{set-diff}) $=$ (({\it{a\/}} $\in$ {\it{y\/}}) $\wedge$ ({\it{a\/}} $\not\in$ {\it{z\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subsetp-set-diff-1 \\ \index{subsetp-set-diff-1}
{\rm{subsetp}}\,({\rm{set-diff}}\,({\it{x\/}}, {\it{y\/}})\index{set-diff}, {\it{x\/}})\index{subsetp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  disjointp-set-diff \\ \index{disjointp-set-diff}
{\rm{disjoint}}\,({\rm{set-diff}}\,({\it{x\/}}, {\it{y\/}})\index{set-diff}, {\it{y\/}})\index{disjoint}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subsetp-set-diff-2 \\ \index{subsetp-set-diff-2}
{\rm{subsetp}}\,({\it{x\/}}, {\rm{set-diff}}\,({\it{y\/}}, {\it{z\/}})\index{set-diff})\index{subsetp} $=$ ({\rm{subsetp}}\,({\it{x\/}}, {\it{y\/}})\index{subsetp} $\wedge$ {\rm{disjoint}}\,({\it{x\/}}, {\it{z\/}})\index{disjoint})
\end{tabbing}

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

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

\begin{verbatim};; The following was discovered during final polishing, for the
;; proof of MAIN-HYPS-RELIEVED-6-FIRST.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  disjoint-set-diff-general \\ \index{disjoint-set-diff-general}
{\rm{disjoint}}\,({\it{x\/}}, {\rm{set-diff}}\,({\it{y\/}}, {\it{z\/}})\index{set-diff})\index{disjoint} $=$ {\rm{subsetp}}\,({\rm{intersection}}\,({\it{x\/}}, {\it{y\/}})\index{intersection}, {\it{z\/}})\index{subsetp}
\end{tabbing}

\begin{verbatim};; No longer relevant:
;(prove-lemma disjoint-set-diff-subsetp (rewrite)
;  (implies (and (disjoint x (set-diff y z))
;		(subsetp z z1))
;	   (disjoint x (set-diff y z1)))
;  ((use (disjoint-wit-witnesses (y (set-diff y z1))))
;   (disable member-set-diff set-diff)))

;; Instead of the following I'll prove the corresponding (in light of
;; DISJOINT-SET-DIFF-GENERAL) fact INTERSECTION-X-X about intersection.
;(prove-lemma disjoint-set-diff (rewrite)
;  (disjoint x (set-diff y x)))

\end{verbatim}\begin{tabbing}{\sc Theorem}:  intersection-subsetp-identity \\ \index{intersection-subsetp-identity}
({\rm{properp}}\,({\it{x\/}})\index{properp} $\wedge$ {\rm{subsetp}}\,({\it{x\/}}, {\it{y\/}})\index{subsetp}) $\rightarrow$ ({\rm{intersection}}\,({\it{x\/}}, {\it{y\/}})\index{intersection} $=$ {\it{x\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  intersection-x-x \\ \index{intersection-x-x}
{\rm{properp}}\,({\it{x\/}})\index{properp} $\rightarrow$ ({\rm{intersection}}\,({\it{x\/}}, {\it{x\/}})\index{intersection} $=$ {\it{x\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subsetp-set-diff-mononone-2 \\ \index{subsetp-set-diff-mononone-2}
{\rm{subsetp}}\,({\rm{set-diff}}\,({\it{x\/}}, {\rm{append}}\,({\it{y\/}}, {\it{z\/}}))\index{set-diff}, {\rm{set-diff}}\,({\it{x\/}}, {\it{z\/}})\index{set-diff})\index{subsetp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subsetp-set-diff-monotone-second \\ \index{subsetp-set-diff-monotone-secon!d}
{\rm{subsetp}}\,({\rm{set-diff}}\,({\it{x\/}}, {\it{y\/}})\index{set-diff}, {\rm{set-diff}}\,({\it{x\/}}, {\it{z\/}})\index{set-diff})\index{subsetp} $=$ {\rm{subsetp}}\,({\rm{intersection}}\,({\it{x\/}}, {\it{z\/}})\index{intersection}, {\it{y\/}})\index{subsetp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  set-diff-nil \\ \index{set-diff-nil}
{\rm{set-diff}}\,({\it{x\/}}, {\bf{nil}})\index{set-diff} $=$ {\rm{fix-properp}}\,({\it{x\/}})\index{fix-properp}
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  length-intersection-set-diff \\ \index{length-intersection-set-diff}
{\rm{length}}\,({\it{x\/}})\index{length} $=$ ({\rm{length}}\,({\rm{set-diff}}\,({\it{x\/}}, {\it{y\/}})\index{set-diff})\index{length} $+$ {\rm{length}}\,({\rm{intersection}}\,({\it{x\/}}, {\it{y\/}})\index{intersection})\index{length})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  length-set-diff-opener \\ \index{length-set-diff-opener}
{\rm{length}}\,({\rm{set-diff}}\,({\it{x\/}}, {\it{y\/}})\index{set-diff})\index{length} $=$ ({\rm{length}}\,({\it{x\/}})\index{length} $-$ {\rm{length}}\,({\rm{intersection}}\,({\it{x\/}}, {\it{y\/}})\index{intersection})\index{length})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  listp-set-diff \\ \index{listp-set-diff}
{\rm{listp}}\,({\rm{set-diff}}\,({\it{x\/}}, {\it{y\/}})\index{set-diff}) $=$ ($\neg$ {\rm{subsetp}}\,({\it{x\/}}, {\it{y\/}})\index{subsetp})
\end{tabbing}

\begin{verbatim};; Here is a messy lemma about disjoint and such
\end{verbatim}\begin{tabbing}{\sc Theorem}:  disjoint-intersection-set-diff-intersection \\ \index{disjoint-intersection-set-diff-i!ntersection}
{\rm{disjoint}}\,({\it{x\/}}, {\rm{intersection}}\,({\it{y\/}}, {\rm{set-diff}}\,({\it{z\/}}, {\rm{intersection}}\,({\it{y\/}}, {\it{x\/}})\index{intersection})\index{set-diff})\index{intersection})\index{disjoint}
\end{tabbing}


\noindent{\sc Event}:   Disable set-diff.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  member-fix-properp \\ \index{member-fix-properp}
({\it{a\/}} $\in$ {\rm{fix-properp}}\,({\it{x\/}})\index{fix-properp}) $=$ ({\it{a\/}} $\in$ {\it{x\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  setp-append \\ \index{setp-append}
{\rm{setp}}\,({\rm{append}}\,({\it{x\/}}, {\it{y\/}}))\index{setp} $=$ ({\rm{disjoint}}\,({\it{x\/}}, {\it{y\/}})\index{disjoint} $\wedge$ {\rm{setp}}\,({\rm{fix-properp}}\,({\it{x\/}})\index{fix-properp})\index{setp} $\wedge$ {\rm{setp}}\,({\it{y\/}})\index{setp})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  setp-cons \\ \index{setp-cons}
{\rm{setp}}\,({\rm{cons}}\,({\it{a\/}}, {\it{x\/}}))\index{setp} $=$ (({\it{a\/}} $\not\in$ {\it{x\/}}) $\wedge$ {\rm{setp}}\,({\it{x\/}})\index{setp})
\end{tabbing}

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

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

\begin{tabbing}{\sc Theorem}:  make-set-preserves-member \\ \index{make-set-preserves-member}
({\it{x\/}} $\in$ {\rm{make-set}}\,({\it{l\/}})\index{make-set}) $=$ ({\it{x\/}} $\in$ {\it{l\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  make-set-preserves-subsetp-1 \\ \index{make-set-preserves-subsetp-1}
{\rm{subsetp}}\,({\rm{make-set}}\,({\it{x\/}})\index{make-set}, {\rm{make-set}}\,({\it{y\/}})\index{make-set})\index{subsetp} $=$ {\rm{subsetp}}\,({\it{x\/}}, {\it{y\/}})\index{subsetp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  make-set-preserves-subsetp-2 \\ \index{make-set-preserves-subsetp-2}
{\rm{subsetp}}\,({\it{x\/}}, {\rm{make-set}}\,({\it{y\/}})\index{make-set})\index{subsetp} $=$ {\rm{subsetp}}\,({\it{x\/}}, {\it{y\/}})\index{subsetp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  make-set-preserves-subsetp-3 \\ \index{make-set-preserves-subsetp-3}
{\rm{subsetp}}\,({\rm{make-set}}\,({\it{x\/}})\index{make-set}, {\it{y\/}})\index{subsetp} $=$ {\rm{subsetp}}\,({\it{x\/}}, {\it{y\/}})\index{subsetp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  make-set-gives-setp \\ \index{make-set-gives-setp}
{\rm{setp}}\,({\rm{make-set}}\,({\it{x\/}})\index{make-set})\index{setp}
\end{tabbing}

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

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

\begin{tabbing}{\sc Theorem}:  listp-make-set \\ \index{listp-make-set}
{\rm{listp}}\,({\rm{make-set}}\,({\it{x\/}})\index{make-set}) $=$ {\rm{listp}}\,({\it{x\/}})
\end{tabbing}


\noindent{\sc Event}:   Disable setp.

\addvspace{18pt}

\begin{verbatim};;;;;; The following were proved in the course of the final run
;;;;;; through the generalization proof.  There are a couple or
;;;;;; so noted above here, too.

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

\begin{tabbing}{\sc Theorem}:  length-set-diff-leq \\ \index{length-set-diff-leq}
{\rm{length}}\,({\it{x\/}})\index{length} $\not<$ {\rm{length}}\,({\rm{set-diff}}\,({\it{x\/}}, {\it{y\/}})\index{set-diff})\index{length}
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  listp-intersection \\ \index{listp-intersection}
{\rm{listp}}\,({\rm{intersection}}\,({\it{x\/}}, {\it{y\/}})\index{intersection}) $=$ ($\neg$ {\rm{disjoint}}\,({\it{x\/}}, {\it{y\/}})\index{disjoint})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  length-set-diff-lessp \\ \index{length-set-diff-lessp}
($\neg$ {\rm{disjoint}}\,({\it{x\/}}, {\it{new\/}})\index{disjoint}) $\rightarrow$ ({\rm{length}}\,({\rm{set-diff}}\,({\it{x\/}}, {\it{new\/}})\index{set-diff})\index{length} $<$ {\rm{length}}\,({\it{x\/}})\index{length})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  disjoint-implies-empty-intersection \\ \index{disjoint-implies-empty-intersecti!on}
{\rm{disjoint}}\,({\it{x\/}}, {\it{y\/}})\index{disjoint} $\rightarrow$ ({\rm{intersection}}\,({\it{x\/}}, {\it{y\/}})\index{intersection} $=$ {\bf{nil}})
\end{tabbing}

\begin{verbatim};; The following lemma DISJOINT-INTERSECTION3-MIDDLE is needed for the
;; proof of ALL-VARS-DISJOINT-OR-SUBSETP-GEN-CLOSURE in
;; generalize.events.  I think I could avoid lemmas like this one
;; INTERSECTION were actually commutative-associative (in which case
;; I'd get rid of disjoint and rely on normalization).

\end{verbatim}\begin{tabbing}{\sc Theorem}:  disjoint-intersection3-middle \\ \index{disjoint-intersection3-middle}
\=\+{\rm{disjoint}}\,({\it{y\/}}, {\rm{intersection}}\,({\it{x\/}}, {\it{z\/}})\index{intersection})\index{disjoint} \\ 
$\rightarrow$$\;\;\;\;$({\rm{intersection}}\,({\it{x\/}}, {\rm{intersection}}\,({\it{y\/}}, {\it{z\/}})\index{intersection})\index{intersection} $=$ {\bf{nil}})\-
\end{tabbing}

\begin{verbatim};; Maybe I should redo the notion of disjoint sometime, perhaps using
;; the fact that intersection is commutative and associative when it's
;; equated with nil.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  disjoint-subsetp-hack \\ \index{disjoint-subsetp-hack}
\=\+({\rm{disjoint}}\,({\it{x\/}}, {\rm{intersection}}\,({\it{u\/}}, {\it{v\/}})\index{intersection})\index{disjoint} $\wedge$ {\rm{subsetp}}\,({\it{w\/}}, {\it{x\/}})\index{subsetp}) \\ 
$\rightarrow$$\;\;\;\;${\rm{disjoint}}\,({\it{u\/}}, {\rm{intersection}}\,({\it{w\/}}, {\it{v\/}})\index{intersection})\index{disjoint}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subsetp-set-diff-sufficiency \\ \index{subsetp-set-diff-sufficiency}
{\rm{subsetp}}\,({\it{x\/}}, {\it{y\/}})\index{subsetp} $\rightarrow$ {\rm{subsetp}}\,({\rm{set-diff}}\,({\it{x\/}}, {\it{z\/}})\index{set-diff}, {\it{y\/}})\index{subsetp}
\end{tabbing}

\begin{verbatim};; The following lemma SETP-INTERSECTION-SUFFICIENCY is needed for
;; MAPPING-RESTRICT from "alists.events", because (I believe)
;; DOMAIN-RESTRICT, which was added during polishing, changed the
;; course of the previous proof.  Similarly for
;; SETP-SET-DIFF-SUFFICIENCY and the lemma MAPPING-CO-RESTRICT.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  setp-intersection-sufficiency \\ \index{setp-intersection-sufficiency}
{\rm{setp}}\,({\it{x\/}})\index{setp} $\rightarrow$ {\rm{setp}}\,({\rm{intersection}}\,({\it{x\/}}, {\it{y\/}})\index{intersection})\index{setp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  setp-set-diff-sufficiency \\ \index{setp-set-diff-sufficiency}
{\rm{setp}}\,({\it{x\/}})\index{setp} $\rightarrow$ {\rm{setp}}\,({\rm{set-diff}}\,({\it{x\/}}, {\it{y\/}})\index{set-diff})\index{setp}
\end{tabbing}

\begin{verbatim};; The definition of FIX-PROPERP was also added in polishing because
;; of a problem with the proof of GEN-CLOSURE-ACCEPT in
;; "generalize.events".  Here are a couple of lemmas about it that
;; might or might not be useful; all other lemmas about it above, and
;; the definition, were added during polishing.

\end{verbatim}
\noindent{\sc Event}:   Disable fix-properp.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  subsetp-fix-properp-1 \\ \index{subsetp-fix-properp-1}
{\rm{subsetp}}\,({\rm{fix-properp}}\,({\it{x\/}})\index{fix-properp}, {\it{y\/}})\index{subsetp} $=$ {\rm{subsetp}}\,({\it{x\/}}, {\it{y\/}})\index{subsetp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subsetp-fix-properp-2 \\ \index{subsetp-fix-properp-2}
{\rm{subsetp}}\,({\it{x\/}}, {\rm{fix-properp}}\,({\it{y\/}})\index{fix-properp})\index{subsetp} $=$ {\rm{subsetp}}\,({\it{x\/}}, {\it{y\/}})\index{subsetp}
\end{tabbing}


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

\addvspace{18pt}

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