\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{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 Definition}:\index{bagdiff} \\  
\=\+{\rm{bagdiff}}\,({\it{x\/}}, {\it{y\/}})\index{bagdiff} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{y\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{car}}\,({\it{y\/}}) $\in$ {\it{x\/}}$\;\;${\bf then }{\rm{bagdiff}}\,({\rm{delete}}\,({\rm{car}}\,({\it{y\/}}), {\it{x\/}})\index{delete}, {\rm{cdr}}\,({\it{y\/}}))\index{bagdiff} \\ 
{\bf else }{\rm{bagdiff}}\,({\it{x\/}}, {\rm{cdr}}\,({\it{y\/}}))\index{bagdiff}$\;${\bf  endif}\- \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{bagint} \\  
\=\+{\rm{bagint}}\,({\it{x\/}}, {\it{y\/}})\index{bagint} \\ 
$=$$\;\;\;\;$\=\+{\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{bagint}}\,({\rm{cdr}}\,({\it{x\/}}), {\rm{delete}}\,({\rm{car}}\,({\it{x\/}}), {\it{y\/}})\index{delete})\index{bagint}) \\ 
{\bf else }{\rm{bagint}}\,({\rm{cdr}}\,({\it{x\/}}), {\it{y\/}})\index{bagint}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

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

\begin{tabbing}{\sc Definition}:\index{subbagp} \\  
\=\+{\rm{subbagp}}\,({\it{x\/}}, {\it{y\/}})\index{subbagp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{car}}\,({\it{x\/}}) $\in$ {\it{y\/}}$\;\;${\bf then }{\rm{subbagp}}\,({\rm{cdr}}\,({\it{x\/}}), {\rm{delete}}\,({\rm{car}}\,({\it{x\/}}), {\it{y\/}})\index{delete})\index{subbagp} \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\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}


\noindent{\sc Event}:   Disable listp-delete.

\addvspace{18pt}

\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}:  equal-occurrences-zero \\ \index{equal-occurrences-zero}
({\rm{occurrences}}\,({\it{x\/}}, {\it{l\/}})\index{occurrences} $=$ {\tt{0}}) $=$ ({\it{x\/}} $\not\in$ {\it{l\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member-non-list \\ \index{member-non-list}
($\neg$ {\rm{listp}}\,({\it{l\/}})) $\rightarrow$ ({\it{x\/}} $\not\in$ {\it{l\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member-delete \\ \index{member-delete}
\=\+({\it{x\/}} $\in$ {\rm{delete}}\,({\it{y\/}}, {\it{l\/}})\index{delete}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\in$ {\it{l\/}} \\ 
{\bf then }\=\+{\bf if }{\it{x\/}} $=$ {\it{y\/}}$\;\;${\bf then }{\tt{1}} $<$ {\rm{occurrences}}\,({\it{x\/}}, {\it{l\/}})\index{occurrences} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}


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

\begin{tabbing}{\sc Theorem}:  occurrences-delete \\ \index{occurrences-delete}
\=\+{\rm{occurrences}}\,({\it{x\/}}, {\rm{delete}}\,({\it{y\/}}, {\it{l\/}})\index{delete})\index{occurrences} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $=$ {\it{y\/}} \\ 
{\bf then }\=\+{\bf if }{\it{x\/}} $\in$ {\it{l\/}}$\;\;${\bf then }{\rm{occurrences}}\,({\it{x\/}}, {\it{l\/}})\index{occurrences} $-\;1$ \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\- \\ 
{\bf else }{\rm{occurrences}}\,({\it{x\/}}, {\it{l\/}})\index{occurrences}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member-bagdiff \\ \index{member-bagdiff}
({\it{x\/}} $\in$ {\rm{bagdiff}}\,({\it{a\/}}, {\it{b\/}})\index{bagdiff}) $=$ ({\rm{occurrences}}\,({\it{x\/}}, {\it{b\/}})\index{occurrences} $<$ {\rm{occurrences}}\,({\it{x\/}}, {\it{a\/}})\index{occurrences})
\end{tabbing}

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


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

\begin{tabbing}{\sc Theorem}:  subbagp-cdr1 \\ \index{subbagp-cdr1}
{\rm{subbagp}}\,({\it{x\/}}, {\it{y\/}})\index{subbagp} $\rightarrow$ {\rm{subbagp}}\,({\rm{cdr}}\,({\it{x\/}}), {\it{y\/}})\index{subbagp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subbagp-cdr2 \\ \index{subbagp-cdr2}
{\rm{subbagp}}\,({\it{x\/}}, {\rm{cdr}}\,({\it{y\/}}))\index{subbagp} $\rightarrow$ {\rm{subbagp}}\,({\it{x\/}}, {\it{y\/}})\index{subbagp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subbagp-bagint1 \\ \index{subbagp-bagint1}
{\rm{subbagp}}\,({\rm{bagint}}\,({\it{x\/}}, {\it{y\/}})\index{bagint}, {\it{x\/}})\index{subbagp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subbagp-bagint2 \\ \index{subbagp-bagint2}
{\rm{subbagp}}\,({\rm{bagint}}\,({\it{x\/}}, {\it{y\/}})\index{bagint}, {\it{y\/}})\index{subbagp}
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  occurrences-bagdiff \\ \index{occurrences-bagdiff}
{\rm{occurrences}}\,({\it{x\/}}, {\rm{bagdiff}}\,({\it{a\/}}, {\it{b\/}})\index{bagdiff})\index{occurrences} $=$ ({\rm{occurrences}}\,({\it{x\/}}, {\it{a\/}})\index{occurrences} $-$ {\rm{occurrences}}\,({\it{x\/}}, {\it{b\/}})\index{occurrences})
\end{tabbing}

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


\noindent{\sc Event}:   Let us define the theory {\it{bags}} to consist of the following events: occurrences-bagint,
bagdiff-delete,
occurrences-bagdiff,
member-bagint,
member-bagdiff,
subbagp-bagint2,
subbagp-bagint1,
subbagp-cdr2,
subbagp-cdr1,
subbagp-delete.\index{bags}

\addvspace{18pt}


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

\addvspace{18pt}

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