\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{subsetp} \\  
\=\+{\rm{subsetp}}\,({\it{x\/}}, {\it{y\/}})\index{subsetp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\rm{car}}\,({\it{x\/}}) $\in$ {\it{y\/}}$\;\;${\bf then }{\rm{subsetp}}\,({\rm{cdr}}\,({\it{x\/}}), {\it{y\/}})\index{subsetp} \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member-cons \\ \index{member-cons}
({\it{a\/}} $\in$ {\it{l\/}}) $\rightarrow$ ({\it{a\/}} $\in$ {\rm{cons}}\,({\it{x\/}}, {\it{l\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subsetp-cons \\ \index{subsetp-cons}
{\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}:  append-is-subsetp \\ \index{append-is-subsetp}
{\rm{subsetp}}\,({\it{x\/}}, {\it{y\/}})\index{subsetp} $\rightarrow$ {\rm{subsetp}}\,({\rm{append}}\,({\it{x\/}}, {\it{y\/}}), {\it{y\/}})\index{subsetp}
\end{tabbing}

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

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

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

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

\begin{tabbing}{\sc Theorem}:  member-append-3 \\ \index{member-append-3}
({\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 Theorem}:  subsetp-of-append-1 \\ \index{subsetp-of-append-1}
{\rm{subsetp}}\,({\it{x\/}}, {\rm{append}}\,({\it{x\/}}, {\it{y\/}}))\index{subsetp}
\end{tabbing}

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

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

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

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

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

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

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

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

\begin{tabbing}{\sc Theorem}:  member-union-2 \\ \index{member-union-2}
({\it{x\/}} $\in$ {\it{z\/}}) $\rightarrow$ ({\it{x\/}} $\in$ ({\it{y\/}} $\cup$ {\it{z\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member-union-1 \\ \index{member-union-1}
({\it{x\/}} $\in$ {\it{y\/}}) $\rightarrow$ ({\it{x\/}} $\in$ ({\it{y\/}} $\cup$ {\it{z\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  non-member-eliminates-union-1 \\ \index{non-member-eliminates-union-1}
({\it{x\/}} $\not\in$ {\it{y\/}}) $\rightarrow$ (({\it{x\/}} $\in$ ({\it{y\/}} $\cup$ {\it{z\/}})) $=$ ({\it{x\/}} $\in$ {\it{z\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  non-member-eliminates-union-2 \\ \index{non-member-eliminates-union-2}
({\it{x\/}} $\not\in$ {\it{z\/}}) $\rightarrow$ (({\it{x\/}} $\in$ ({\it{y\/}} $\cup$ {\it{z\/}})) $=$ ({\it{x\/}} $\in$ {\it{y\/}}))
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  subsetp-of-union-1 \\ \index{subsetp-of-union-1}
{\rm{subsetp}}\,({\it{x\/}}, {\it{x\/}} $\cup$ {\it{y\/}})\index{subsetp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subsetp-of-union-2 \\ \index{subsetp-of-union-2}
{\rm{subsetp}}\,({\it{y\/}}, {\it{x\/}} $\cup$ {\it{y\/}})\index{subsetp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  union-preserves-subsetp-second-1 \\ \index{union-preserves-subsetp-second-!1}
{\rm{subsetp}}\,({\it{x\/}}, {\it{y\/}})\index{subsetp} $\rightarrow$ {\rm{subsetp}}\,({\it{x\/}}, {\it{y\/}} $\cup$ {\it{z\/}})\index{subsetp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  union-preserves-subsetp-second-2 \\ \index{union-preserves-subsetp-second-!2}
{\rm{subsetp}}\,({\it{x\/}}, {\it{z\/}})\index{subsetp} $\rightarrow$ {\rm{subsetp}}\,({\it{x\/}}, {\it{y\/}} $\cup$ {\it{z\/}})\index{subsetp}
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  subsetp-union-union \\ \index{subsetp-union-union}
({\rm{subsetp}}\,({\it{a\/}}, {\it{b\/}})\index{subsetp} $\wedge$ {\rm{subsetp}}\,({\it{c\/}}, {\it{d\/}})\index{subsetp}) $\rightarrow$ {\rm{subsetp}}\,({\it{a\/}} $\cup$ {\it{c\/}}, {\it{b\/}} $\cup$ {\it{d\/}})\index{subsetp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  union-subsetp \\ \index{union-subsetp}
{\rm{subsetp}}\,({\it{x\/}}, {\it{y\/}})\index{subsetp} $\rightarrow$ (({\it{x\/}} $\cup$ {\it{y\/}}) $=$ {\it{y\/}})
\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 Definition}:\index{setp} \\  
\=\+{\rm{setp}}\,({\it{x\/}})\index{setp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }$\neg$ {\rm{listp}}\,({\it{x\/}})$\;\;${\bf then }{\bf{t}} \\ 
{\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}:  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}:  union-of-sets-is-setp \\ \index{union-of-sets-is-setp}
({\rm{setp}}\,({\it{x\/}})\index{setp} $\wedge$ {\rm{setp}}\,({\it{y\/}})\index{setp}) $\rightarrow$ {\rm{setp}}\,({\it{x\/}} $\cup$ {\it{y\/}})\index{setp}
\end{tabbing}


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

\addvspace{18pt}

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