\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{newpairs} \\  
\=\+{\rm{newpairs}}\,({\it{pair\/}}, {\it{pairs\/}})\index{newpairs} \\ 
$=$$\;\;\;\;$\=\+{\bf if }$\neg$ {\rm{listp}}\,({\it{pairs\/}})$\;\;${\bf then }{\bf{nil}} \\ 
{\bf elseif }{\rm{cdr}}\,({\it{pair\/}}) $=$ {\rm{caar}}\,({\it{pairs\/}}) \\ 
{\bf then }{\rm{cons}}\,({\rm{cons}}\,({\rm{car}}\,({\it{pair\/}}), {\rm{cdar}}\,({\it{pairs\/}})), {\rm{newpairs}}\,({\it{pair\/}}, {\rm{cdr}}\,({\it{pairs\/}}))\index{newpairs}) \\ 
{\bf else }{\rm{newpairs}}\,({\it{pair\/}}, {\rm{cdr}}\,({\it{pairs\/}}))\index{newpairs}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{all-newpairs} \\  
\=\+{\rm{all-newpairs}}\,({\it{pairs1\/}}, {\it{pairs2\/}})\index{all-newpairs} \\ 
$=$$\;\;\;\;$\=\+{\bf if }$\neg$ {\rm{listp}}\,({\it{pairs1\/}})$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{append}}\,(\=\+{\rm{newpairs}}\,({\rm{car}}\,({\it{pairs1\/}}), {\it{pairs2\/}})\index{newpairs}, \\ 
{\rm{all-newpairs}}\,({\rm{cdr}}\,({\it{pairs1\/}}), {\it{pairs2\/}})\index{all-newpairs})\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{all-cars} \\  
\=\+{\rm{all-cars}}\,({\it{pairs\/}})\index{all-cars} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{pairs\/}})$\;\;${\bf then }{\rm{cons}}\,({\rm{caar}}\,({\it{pairs\/}}), {\rm{all-cars}}\,({\rm{cdr}}\,({\it{pairs\/}}))\index{all-cars}) \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{all-cdrs} \\  
\=\+{\rm{all-cdrs}}\,({\it{pairs\/}})\index{all-cdrs} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{pairs\/}})$\;\;${\bf then }{\rm{cons}}\,({\rm{cdar}}\,({\it{pairs\/}}), {\rm{all-cdrs}}\,({\rm{cdr}}\,({\it{pairs\/}}))\index{all-cdrs}) \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

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

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

\begin{tabbing}{\sc Definition}:\index{field} \\  
{\rm{field}}\,({\it{pairs\/}})\index{field} $=$ {\rm{prod}}\,({\rm{all-cars}}\,({\it{pairs\/}})\index{all-cars}, {\rm{all-cdrs}}\,({\it{pairs\/}})\index{all-cdrs})\index{prod}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{all-pairsp} \\  
\=\+{\rm{all-pairsp}}\,({\it{pairs\/}})\index{all-pairsp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }$\neg$ {\rm{listp}}\,({\it{pairs\/}})$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{listp}}\,({\rm{car}}\,({\it{pairs\/}})) $\wedge$ {\rm{all-pairsp}}\,({\rm{cdr}}\,({\it{pairs\/}}))\index{all-pairsp}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  newpairs-prod1-subsetp \\ \index{newpairs-prod1-subsetp}
{\rm{subsetp}}\,({\rm{newpairs}}\,({\it{pair\/}}, {\it{pairs\/}})\index{newpairs}, {\rm{prod1}}\,({\rm{car}}\,({\it{pair\/}}), {\rm{all-cdrs}}\,({\it{pairs\/}})\index{all-cdrs})\index{prod1})\index{subsetp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-newpairs-field-subsetp-1 \\ \index{all-newpairs-field-subsetp-1}
{\rm{subsetp}}\,({\rm{all-newpairs}}\,({\it{pairs1\/}}, {\it{pairs2\/}})\index{all-newpairs}, {\rm{prod}}\,({\rm{all-cars}}\,({\it{pairs1\/}})\index{all-cars}, {\rm{all-cdrs}}\,({\it{pairs2\/}})\index{all-cdrs})\index{prod})\index{subsetp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-newpairs-field-subsetp \\ \index{all-newpairs-field-subsetp}
{\rm{subsetp}}\,({\rm{all-newpairs}}\,({\it{pairs\/}}, {\it{pairs\/}})\index{all-newpairs}, {\rm{field}}\,({\it{pairs\/}})\index{field})\index{subsetp}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{close1} \\  
{\rm{close1}}\,({\it{pairs\/}})\index{close1} $=$ ({\rm{make-set}}\,({\rm{all-newpairs}}\,({\it{pairs\/}}, {\it{pairs\/}})\index{all-newpairs})\index{make-set} $\cup$ {\it{pairs\/}})
\end{tabbing}

\begin{verbatim}; My goal is to show that 
; (SUBSETP PAIRS (FIELD PAIRS))
; and
; (IMPLIES (SUBSETP X (FIELD PAIRS))
;          (SUBSETP (CLOSE1 X) (FIELD PAIRS))) .
; For then we can prove the following lemma, which will
; show that the following definition should
; be accepted, where CARD is cardinality:

;(IMPLIES (AND (ALL-PAIRSP PAIRS)
;	      (NOT (EQUAL PAIRS (CLOSE1 PAIRS))))
;	 (EQUAL (LESSP (DIFFERENCE (CARD (FIELD (CLOSE1 PAIRS)))
;				   (CARD (CLOSE1 PAIRS)))
;		       (DIFFERENCE (CARD (FIELD PAIRS))
;				   (CARD PAIRS)))
;		T))

\end{verbatim}\begin{tabbing}{\sc Theorem}:  cdr-all-cars-subsetp \\ \index{cdr-all-cars-subsetp}
{\rm{subsetp}}\,({\rm{all-cars}}\,({\rm{cdr}}\,({\it{pairs\/}}))\index{all-cars}, {\rm{all-cars}}\,({\it{pairs\/}})\index{all-cars})\index{subsetp}
\end{tabbing}

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

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

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

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

\begin{tabbing}{\sc Theorem}:  field-subsetp \\ \index{field-subsetp}
{\rm{all-pairsp}}\,({\it{pairs\/}})\index{all-pairsp} $\rightarrow$ {\rm{subsetp}}\,({\it{pairs\/}}, {\rm{field}}\,({\it{pairs\/}})\index{field})\index{subsetp}
\end{tabbing}

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

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

\begin{tabbing}{\sc Theorem}:  member-all-cdrs \\ \index{member-all-cdrs}
({\it{a\/}} $\in$ {\it{y\/}}) $\rightarrow$ ({\rm{cdr}}\,({\it{a\/}}) $\in$ {\rm{all-cdrs}}\,({\it{y\/}})\index{all-cdrs})
\end{tabbing}

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

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

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

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

\begin{tabbing}{\sc Theorem}:  prod-subsetp \\ \index{prod-subsetp}
({\rm{subsetp}}\,({\it{x1\/}}, {\it{x2\/}})\index{subsetp} $\wedge$ {\rm{subsetp}}\,({\it{y1\/}}, {\it{y2\/}})\index{subsetp}) $\rightarrow$ {\rm{subsetp}}\,({\rm{prod}}\,({\it{x1\/}}, {\it{y1\/}})\index{prod}, {\rm{prod}}\,({\it{x2\/}}, {\it{y2\/}})\index{prod})\index{subsetp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subsetp-field-twice \\ \index{subsetp-field-twice}
{\rm{subsetp}}\,({\rm{field}}\,({\rm{field}}\,({\it{l\/}})\index{field})\index{field}, {\rm{field}}\,({\it{l\/}})\index{field})\index{subsetp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subsetp-close1-field \\ \index{subsetp-close1-field}
{\rm{subsetp}}\,({\it{x\/}}, {\rm{field}}\,({\it{pairs\/}})\index{field})\index{subsetp} $\rightarrow$ {\rm{subsetp}}\,({\rm{close1}}\,({\it{x\/}})\index{close1}, {\rm{field}}\,({\it{pairs\/}})\index{field})\index{subsetp}
\end{tabbing}

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

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

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

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

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

\begin{tabbing}{\sc Theorem}:  remove-subsetp \\ \index{remove-subsetp}
{\rm{subsetp}}\,({\rm{remove}}\,({\it{a\/}}, {\it{l\/}})\index{remove}, {\it{l\/}})\index{subsetp}
\end{tabbing}

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

\begin{verbatim}; Interestingly, I couldn't get the following at first, but in the
; course of performing a manual proof I found the rewrite lemmas
; (added above) that I needed.  By the way, as things are now the
; induction hint below is necessary.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  remove-card \\ \index{remove-card}
({\it{a\/}} $\in$ {\it{l\/}}) $\rightarrow$ ({\rm{card}}\,({\rm{remove}}\,({\it{a\/}}, {\it{l\/}})\index{remove})\index{card} $=$ ({\rm{card}}\,({\it{l\/}})\index{card} $-\;1$))
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  length-remove \\ \index{length-remove}
({\rm{length}}\,({\rm{remove}}\,({\it{a\/}}, {\it{x\/}})\index{remove})\index{length} $\not=$ {\rm{length}}\,({\it{x\/}})\index{length}) $\rightarrow$ ({\rm{length}}\,({\rm{remove}}\,({\it{a\/}}, {\it{x\/}})\index{remove})\index{length} $<$ {\rm{length}}\,({\it{x\/}})\index{length})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  card-subsetp-ind-help \\ \index{card-subsetp-ind-help}
{\rm{listp}}\,({\it{x\/}}) $\rightarrow$ ({\rm{length}}\,({\rm{remove}}\,({\rm{car}}\,({\it{x\/}}), {\it{x\/}})\index{remove})\index{length} $<$ {\rm{length}}\,({\it{x\/}})\index{length})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{card-subsetp-ind} \\  
\=\+{\rm{card-subsetp-ind}}\,({\it{x\/}}, {\it{y\/}})\index{card-subsetp-ind} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}})$\;\;${\bf then }{\rm{card-subsetp-ind}}\,({\rm{remove}}\,({\rm{car}}\,({\it{x\/}}), {\it{x\/}})\index{remove}, {\rm{remove}}\,({\rm{car}}\,({\it{x\/}}), {\it{y\/}})\index{remove})\index{card-subsetp-ind} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remove-preserves-subsetp \\ \index{remove-preserves-subsetp}
{\rm{subsetp}}\,({\it{x\/}}, {\it{y\/}})\index{subsetp} $\rightarrow$ {\rm{subsetp}}\,({\rm{remove}}\,({\it{a\/}}, {\it{x\/}})\index{remove}, {\rm{remove}}\,({\it{a\/}}, {\it{y\/}})\index{remove})\index{subsetp}
\end{tabbing}

\begin{verbatim}; Interestingly, I came to proving the following lemma by
; trying to do a hand proof of the one after it and
; realizing that the former was conceptually simpler.
; I'm still surprised that the theorem-prover handled the
; former but not (directly) the latter.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  card-subsetp \\ \index{card-subsetp}
{\rm{subsetp}}\,({\it{x\/}}, {\it{y\/}})\index{subsetp} $\rightarrow$ ({\rm{card}}\,({\it{x\/}})\index{card} $\leq$ {\rm{card}}\,({\it{y\/}})\index{card})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  card-subsetp-rewrite \\ \index{card-subsetp-rewrite}
({\rm{subsetp}}\,({\it{x\/}}, {\it{y\/}})\index{subsetp} $\wedge$ ({\rm{card}}\,({\it{x\/}})\index{card} $\not=$ {\rm{card}}\,({\it{y\/}})\index{card})) $\rightarrow$ (({\rm{card}}\,({\it{x\/}})\index{card} $<$ {\rm{card}}\,({\it{y\/}})\index{card}) $=$ {\bf{t}})
\end{tabbing}

\begin{verbatim}; Recall that we proved
; SUBSETP-CLOSE1-FIELD :
; (IMPLIES (SUBSETP X (FIELD PAIRS))
;	   (SUBSETP (CLOSE1 X) (FIELD PAIRS)))

\end{verbatim}\begin{tabbing}{\sc Theorem}:  field-of-close1-is-subsetp \\ \index{field-of-close1-is-subsetp}
{\rm{all-pairsp}}\,({\it{x\/}})\index{all-pairsp} $\rightarrow$ {\rm{subsetp}}\,({\rm{field}}\,({\rm{close1}}\,({\it{x\/}})\index{close1})\index{field}, {\rm{field}}\,({\it{x\/}})\index{field})\index{subsetp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  field-of-close1-is-superset \\ \index{field-of-close1-is-superset}
{\rm{subsetp}}\,({\rm{field}}\,({\it{x\/}})\index{field}, {\rm{field}}\,({\rm{close1}}\,({\it{x\/}})\index{close1})\index{field})\index{subsetp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  close1-preserves-card-of-field \\ \index{close1-preserves-card-of-field}
{\rm{all-pairsp}}\,({\it{x\/}})\index{all-pairsp} $\rightarrow$ ({\rm{card}}\,({\rm{field}}\,({\rm{close1}}\,({\it{x\/}})\index{close1})\index{field})\index{card} $=$ {\rm{card}}\,({\rm{field}}\,({\it{x\/}})\index{field})\index{card})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  union-card-lessp \\ \index{union-card-lessp}
(({\it{x\/}} $\cup$ {\it{y\/}}) $\not=$ {\it{y\/}}) $\rightarrow$ ({\rm{card}}\,({\it{y\/}})\index{card} $<$ {\rm{card}}\,({\it{x\/}} $\cup$ {\it{y\/}})\index{card})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  trans-accept-1 \\ \index{trans-accept-1}
\=\+({\rm{all-pairsp}}\,({\it{pairs\/}})\index{all-pairsp} $\wedge$ ({\it{pairs\/}} $\not=$ {\rm{close1}}\,({\it{pairs\/}})\index{close1})) \\ 
$\rightarrow$$\;\;\;\;$(({\rm{card}}\,({\it{pairs\/}})\index{card} $<$ {\rm{card}}\,({\rm{close1}}\,({\it{pairs\/}})\index{close1})\index{card}) $=$ {\bf{t}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  card-field-lessp \\ \index{card-field-lessp}
\=\+({\rm{all-pairsp}}\,({\it{x\/}})\index{all-pairsp} $\wedge$ ({\rm{card}}\,({\it{x\/}})\index{card} $\not=$ {\rm{card}}\,({\rm{field}}\,({\it{x\/}})\index{field})\index{card})) \\ 
$\rightarrow$$\;\;\;\;$(({\rm{card}}\,({\it{x\/}})\index{card} $<$ {\rm{card}}\,({\rm{field}}\,({\it{x\/}})\index{field})\index{card}) $=$ {\bf{t}})\-
\end{tabbing}


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

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

\begin{tabbing}{\sc Theorem}:  newpairs-preserves-all-pairsp \\ \index{newpairs-preserves-all-pairsp}
\=\+({\rm{all-pairsp}}\,({\it{pairs1\/}})\index{all-pairsp} $\wedge$ {\rm{all-pairsp}}\,({\it{pairs2\/}})\index{all-pairsp}) \\ 
$\rightarrow$$\;\;\;\;${\rm{all-pairsp}}\,({\rm{newpairs}}\,({\it{pairs1\/}}, {\it{pairs2\/}})\index{newpairs})\index{all-pairsp}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-newpairs-preserves-all-pairsp \\ \index{all-newpairs-preserves-all-pair!sp}
\=\+({\rm{all-pairsp}}\,({\it{pairs1\/}})\index{all-pairsp} $\wedge$ {\rm{all-pairsp}}\,({\it{pairs2\/}})\index{all-pairsp}) \\ 
$\rightarrow$$\;\;\;\;${\rm{all-pairsp}}\,({\rm{all-newpairs}}\,({\it{pairs1\/}}, {\it{pairs2\/}})\index{all-newpairs})\index{all-pairsp}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  make-set-preserves-all-pairsp \\ \index{make-set-preserves-all-pairsp}
{\rm{all-pairsp}}\,({\it{pairs\/}})\index{all-pairsp} $\rightarrow$ {\rm{all-pairsp}}\,({\rm{make-set}}\,({\it{pairs\/}})\index{make-set})\index{all-pairsp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  close-1-preserves-all-pairsp \\ \index{close-1-preserves-all-pairsp}
{\rm{all-pairsp}}\,({\it{pairs\/}})\index{all-pairsp} $\rightarrow$ {\rm{all-pairsp}}\,({\rm{close1}}\,({\it{pairs\/}})\index{close1})\index{all-pairsp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-difference-for-trans-accept \\ \index{lessp-difference-for-trans-accept}
(({\it{c\/}} $<$ {\it{a\/}}) $\wedge$ ({\it{c\/}} $<$ {\it{b\/}})) $\rightarrow$ ((({\it{a\/}} $-$ {\it{b\/}}) $<$ ({\it{a\/}} $-$ {\it{c\/}})) $=$ {\bf{t}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  card-field-not-lessp \\ \index{card-field-not-lessp}
{\rm{all-pairsp}}\,({\it{x\/}})\index{all-pairsp} $\rightarrow$ (({\rm{card}}\,({\rm{field}}\,({\it{x\/}})\index{field})\index{card} $<$ {\rm{card}}\,({\it{x\/}})\index{card}) $=$ {\bf{f}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  trans-accept \\ \index{trans-accept}
\=\+({\rm{all-pairsp}}\,({\it{pairs\/}})\index{all-pairsp} $\wedge$ ({\it{pairs\/}} $\not=$ {\rm{close1}}\,({\it{pairs\/}})\index{close1})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+({\rm{card}}\,({\rm{field}}\,({\rm{close1}}\,({\it{pairs\/}})\index{close1})\index{field})\index{card} $-$ {\rm{card}}\,({\rm{close1}}\,({\it{pairs\/}})\index{close1})\index{card}) \\ 
$<$$\;\;\;\;$({\rm{card}}\,({\rm{field}}\,({\it{pairs\/}})\index{field})\index{card} $-$ {\rm{card}}\,({\it{pairs\/}})\index{card}))\- \\ 
$=$$\;\;\;\;${\bf{t}})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable field.

\addvspace{18pt}


\noindent{\sc Event}:   Disable close1.

\addvspace{18pt}

\begin{verbatim}; It's unfortunate that the following is needed.

\end{verbatim}
\noindent{\sc Event}:   Disable close1-preserves-card-of-field.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{trans} \\  
\=\+{\rm{trans}}\,({\it{pairs\/}})\index{trans} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{all-pairsp}}\,({\it{pairs\/}})\index{all-pairsp} \\ 
{\bf then }\=\+{\bf if }{\it{pairs\/}} $=$ {\rm{close1}}\,({\it{pairs\/}})\index{close1}$\;\;${\bf then }{\it{pairs\/}} \\ 
{\bf else }{\rm{trans}}\,({\rm{close1}}\,({\it{pairs\/}})\index{close1})\index{trans}$\;${\bf  endif}\- \\ 
{\bf else }{\it{pairs\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-newpairs-closes \\ \index{all-newpairs-closes}
\=\+(({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}) $\in$ {\it{pairs1\/}}) $\wedge$ ({\rm{cons}}\,({\it{y\/}}, {\it{z\/}}) $\in$ {\it{pairs2\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{cons}}\,({\it{x\/}}, {\it{z\/}}) $\in$ {\rm{all-newpairs}}\,({\it{pairs1\/}}, {\it{pairs2\/}})\index{all-newpairs})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  close1-closes \\ \index{close1-closes}
\=\+({\rm{all-pairsp}}\,({\it{pairs\/}})\index{all-pairsp} $\wedge$ ({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}) $\in$ {\it{pairs\/}}) $\wedge$ ({\rm{cons}}\,({\it{y\/}}, {\it{z\/}}) $\in$ {\it{pairs\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{cons}}\,({\it{x\/}}, {\it{z\/}}) $\in$ {\rm{close1}}\,({\it{pairs\/}})\index{close1})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  trans-closes \\ \index{trans-closes}
\=\+({\rm{all-pairsp}}\,({\it{pairs\/}})\index{all-pairsp} $\wedge$ ({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}) $\in$ {\it{pairs\/}}) $\wedge$ ({\rm{cons}}\,({\it{y\/}}, {\it{z\/}}) $\in$ {\it{pairs\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{cons}}\,({\it{x\/}}, {\it{z\/}}) $\in$ {\rm{trans}}\,({\it{pairs\/}})\index{trans})\-
\end{tabbing}

\begin{verbatim}; Finally, we prove that TRANS gives the least transitive set
; containing the original pairs.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{transp} \\  
{\rm{transp}}\,({\it{l\/}})\index{transp} $=$ ({\rm{all-pairsp}}\,({\it{l\/}})\index{all-pairsp} $\wedge$ {\rm{subsetp}}\,({\rm{all-newpairs}}\,({\it{l\/}}, {\it{l\/}})\index{all-newpairs}, {\it{l\/}})\index{subsetp})
\end{tabbing}

\begin{verbatim};; ok to here 1/04/87 09:49:47

\end{verbatim}\begin{tabbing}{\sc Theorem}:  member-newpairs \\ \index{member-newpairs}
\=\+({\rm{all-pairsp}}\,({\it{l\/}})\index{all-pairsp} $\wedge$ ({\it{b\/}} $\in$ {\it{l\/}}) $\wedge$ ({\rm{cdr}}\,({\it{a\/}}) $=$ {\rm{car}}\,({\it{b\/}}))) \\ 
$\rightarrow$$\;\;\;\;$({\rm{cons}}\,({\rm{car}}\,({\it{a\/}}), {\rm{cdr}}\,({\it{b\/}})) $\in$ {\rm{newpairs}}\,({\it{a\/}}, {\it{l\/}})\index{newpairs})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  newpairs-preserves-subsetp \\ \index{newpairs-preserves-subsetp}
\=\+({\rm{all-pairsp}}\,({\it{l\/}})\index{all-pairsp} $\wedge$ {\rm{all-pairsp}}\,({\it{m\/}})\index{all-pairsp} $\wedge$ {\rm{subsetp}}\,({\it{l\/}}, {\it{m\/}})\index{subsetp}) \\ 
$\rightarrow$$\;\;\;\;${\rm{subsetp}}\,({\rm{newpairs}}\,({\it{a\/}}, {\it{l\/}})\index{newpairs}, {\rm{newpairs}}\,({\it{a\/}}, {\it{m\/}})\index{newpairs})\index{subsetp}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-newpairs-preserves-subsetp-2 \\ \index{all-newpairs-preserves-subsetp-!2}
\=\+({\rm{all-pairsp}}\,({\it{l\/}})\index{all-pairsp} $\wedge$ {\rm{all-pairsp}}\,({\it{m1\/}})\index{all-pairsp} $\wedge$ {\rm{all-pairsp}}\,({\it{m2\/}})\index{all-pairsp} $\wedge$ {\rm{subsetp}}\,({\it{m1\/}}, {\it{m2\/}})\index{subsetp}) \\ 
$\rightarrow$$\;\;\;\;${\rm{subsetp}}\,({\rm{all-newpairs}}\,({\it{l\/}}, {\it{m1\/}})\index{all-newpairs}, {\rm{all-newpairs}}\,({\it{l\/}}, {\it{m2\/}})\index{all-newpairs})\index{subsetp}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member-newpairs-all-newpairs \\ \index{member-newpairs-all-newpairs}
({\it{a\/}} $\in$ {\it{l\/}}) $\rightarrow$ {\rm{subsetp}}\,({\rm{newpairs}}\,({\it{a\/}}, {\it{m\/}})\index{newpairs}, {\rm{all-newpairs}}\,({\it{l\/}}, {\it{m\/}})\index{all-newpairs})\index{subsetp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-newpairs-preserves-subsetp-1 \\ \index{all-newpairs-preserves-subsetp-!1}
\=\+({\rm{all-pairsp}}\,({\it{l1\/}})\index{all-pairsp} $\wedge$ {\rm{all-pairsp}}\,({\it{l2\/}})\index{all-pairsp} $\wedge$ {\rm{all-pairsp}}\,({\it{m\/}})\index{all-pairsp} $\wedge$ {\rm{subsetp}}\,({\it{l1\/}}, {\it{l2\/}})\index{subsetp}) \\ 
$\rightarrow$$\;\;\;\;${\rm{subsetp}}\,({\rm{all-newpairs}}\,({\it{l1\/}}, {\it{m\/}})\index{all-newpairs}, {\rm{all-newpairs}}\,({\it{l2\/}}, {\it{m\/}})\index{all-newpairs})\index{subsetp}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-newpairs-preserves-subsetp-both \\ \index{all-newpairs-preserves-subsetp-!both}
\=\+(\=\+{\rm{all-pairsp}}\,({\it{l1\/}})\index{all-pairsp} \\ 
$\wedge$$\;\;\;\;${\rm{all-pairsp}}\,({\it{l2\/}})\index{all-pairsp} \\ 
$\wedge$$\;\;\;\;${\rm{all-pairsp}}\,({\it{m1\/}})\index{all-pairsp} \\ 
$\wedge$$\;\;\;\;${\rm{all-pairsp}}\,({\it{m2\/}})\index{all-pairsp} \\ 
$\wedge$$\;\;\;\;${\rm{subsetp}}\,({\it{l1\/}}, {\it{l2\/}})\index{subsetp} \\ 
$\wedge$$\;\;\;\;${\rm{subsetp}}\,({\it{m1\/}}, {\it{m2\/}})\index{subsetp})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{subsetp}}\,({\rm{all-newpairs}}\,({\it{l1\/}}, {\it{m1\/}})\index{all-newpairs}, {\rm{all-newpairs}}\,({\it{l2\/}}, {\it{m2\/}})\index{all-newpairs})\index{subsetp}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  close1-preserves-subsetp \\ \index{close1-preserves-subsetp}
\=\+({\rm{all-pairsp}}\,({\it{l\/}})\index{all-pairsp} $\wedge$ {\rm{all-pairsp}}\,({\it{m\/}})\index{all-pairsp} $\wedge$ {\rm{subsetp}}\,({\it{l\/}}, {\it{m\/}})\index{subsetp}) \\ 
$\rightarrow$$\;\;\;\;${\rm{subsetp}}\,({\rm{close1}}\,({\it{l\/}})\index{close1}, {\rm{close1}}\,({\it{m\/}})\index{close1})\index{subsetp}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  trans-is-least-transp \\ \index{trans-is-least-transp}
\=\+({\rm{all-pairsp}}\,({\it{pairs\/}})\index{all-pairsp} $\wedge$ {\rm{subsetp}}\,({\it{pairs\/}}, {\it{l\/}})\index{subsetp} $\wedge$ {\rm{transp}}\,({\it{l\/}})\index{transp}) \\ 
$\rightarrow$$\;\;\;\;${\rm{subsetp}}\,({\rm{trans}}\,({\it{pairs\/}})\index{trans}, {\it{l\/}})\index{subsetp}\-
\end{tabbing}

\begin{verbatim}; Now let's show that the transitive closure of a transitive set is itself.
; In particular, (TRANS (TRANS PAIRS)) = (TRANS PAIRS) for a list PAIRS of
; pairs.  Interestingly, though, the latter result is easily proved by
; a trivial induction on trans:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  trans-is-idempotent \\ \index{trans-is-idempotent}
{\rm{trans}}\,({\rm{trans}}\,({\it{pairs\/}})\index{trans})\index{trans} $=$ {\rm{trans}}\,({\it{pairs\/}})\index{trans}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  close1-of-transp \\ \index{close1-of-transp}
{\rm{transp}}\,({\it{pairs\/}})\index{transp} $\rightarrow$ ({\rm{close1}}\,({\it{pairs\/}})\index{close1} $=$ {\it{pairs\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  trans-of-transp \\ \index{trans-of-transp}
{\rm{transp}}\,({\it{pairs\/}})\index{transp} $\rightarrow$ ({\rm{trans}}\,({\it{pairs\/}})\index{trans} $=$ {\it{pairs\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  trans-closes-again \\ \index{trans-closes-again}
\=\+(\=\+{\rm{all-pairsp}}\,({\it{pairs\/}})\index{all-pairsp} \\ 
$\wedge$$\;\;\;\;$({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}) $\in$ {\rm{trans}}\,({\it{pairs\/}})\index{trans}) \\ 
$\wedge$$\;\;\;\;$({\rm{cons}}\,({\it{y\/}}, {\it{z\/}}) $\in$ {\rm{trans}}\,({\it{pairs\/}})\index{trans}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{cons}}\,({\it{x\/}}, {\it{z\/}}) $\in$ {\rm{trans}}\,({\it{pairs\/}})\index{trans})\-
\end{tabbing}

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