\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 library {\tt{"subset"}}.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{set-equal}$\;\;$
{\rm{set-equal}}\,({\it{x\/}}, {\it{y\/}})\index{set-equal} $=$ ({\rm{subsetp}}\,({\it{x\/}}, {\it{y\/}})\index{subsetp} $\wedge$ {\rm{subsetp}}\,({\it{y\/}}, {\it{x\/}})\index{subsetp})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  set-equal-char \\ \index{set-equal-char}
{\rm{set-equal}}\,({\it{x\/}}, {\it{y\/}})\index{set-equal} $\rightarrow$ (({\it{a\/}} $\in$ {\it{x\/}}) $=$ ({\it{a\/}} $\in$ {\it{y\/}}))
\end{tabbing}

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

\begin{tabbing}{\sc Definition}:\index{sym-diff}$\;\;$
{\rm{sym-diff}}\,({\it{x\/}}, {\it{y\/}})\index{sym-diff} $=$ ({\rm{diff}}\,({\it{x\/}}, {\it{y\/}})\index{diff} $\cup$ {\rm{diff}}\,({\it{y\/}}, {\it{x\/}})\index{diff})
\end{tabbing}

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

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

\begin{tabbing}{\sc Theorem}:  subsetp-witness \\ \index{subsetp-witness}
\=\+(({\rm{not-subsetp-skolem}}\,({\it{x\/}}, {\it{y\/}})\index{not-subsetp-skolem} $\not\in$ {\it{x\/}}) $\vee$ ({\rm{not-subsetp-skolem}}\,({\it{x\/}}, {\it{y\/}})\index{not-subsetp-skolem} $\in$ {\it{y\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{subsetp}}\,({\it{x\/}}, {\it{y\/}})\index{subsetp}\-
\end{tabbing}

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

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

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

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


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

\addvspace{18pt}

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

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

\begin{verbatim};(PROVE-LEMMA SYM-DIFF-ASSOC (REWRITE)
;	     (SET-EQUAL (SYM-DIFF (SYM-DIFF X Y) Z)
;			(SYM-DIFF X (SYM-DIFF Y Z))))

\end{verbatim}
\noindent{\sc Event}:   Enable sym-diff.

\addvspace{18pt}

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

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