\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[]

\begin{verbatim}#|

 Copyright (C) 1994 by Computational Logic, Inc.  All Rights Reserved.

 This script is hereby placed in the public domain, and therefore unlimited
 editing and redistribution is permitted.

 NO WARRANTY

 Computational Logic, Inc. PROVIDES ABSOLUTELY NO WARRANTY.  THE EVENT SCRIPT
 IS PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS OR IMPLIED,
 INCLUDING, BUT NOT LIMITED TO, ANY IMPLIED WARRANTIES OF MERCHANTABILITY AND
 FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND
 PERFORMANCE OF THE SCRIPT IS WITH YOU.  SHOULD THE SCRIPT PROVE DEFECTIVE, YOU
 ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION.

 IN NO EVENT WILL Computational Logic, Inc. BE LIABLE TO YOU FOR ANY DAMAGES,
 ANY LOST PROFITS, LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR CONSEQUENTIAL
 DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THIS SCRIPT (INCLUDING BUT
 NOT LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES
 SUSTAINED BY THIRD PARTIES), EVEN IF YOU HAVE ADVISED US OF THE POSSIBILITY OF
 SUCH DAMAGES, OR FOR ANY CLAIM BY ANY OTHER PARTY.
|#

;; Matt Kaufmann

\end{verbatim}
\noindent{\sc Event}:   Start with the initial {\bf nqthm} theory.

\addvspace{18pt}


\begin{verbatim};; These are events in support of the paper ``A Mechanically-Checked
;; Correctness Proof for Generalization in the Presence of Free
;; Variables,'' Journal of Automated Reasoning, Vol. 7, 1991.

;; This events file contains no DEFN-SK events, but instead contains two
;; DCLs and two ADD-AXIOMs from a DEFN-SK event that I commented out.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; sets.events file
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Requires deftheory enhancement.
;; Requires only ground-zero theory, nqthm mode.

;; 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}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; alists.events file
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Requires deftheory enhancement.
;; Requires sets.

;; Alists, March 1990.  Most of the definitions and some of the lemmas
;; were contributed by Bill Bevier; the rest are by Matt Kaufmann.

;; Functions defined here:

;; (deftheory alist-defns
;;   (alistp domain range value bind rembind invert mapping
;;           restrict co-restrict))

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

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

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

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


\noindent{\sc Event}:   Disable alistp.

\addvspace{18pt}

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

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

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

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

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

\begin{tabbing}{\sc Theorem}:  domain-cons \\ \index{domain-cons}
\=\+{\rm{domain}}\,({\rm{cons}}\,({\it{a\/}}, {\it{map\/}}))\index{domain} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{a\/}})$\;\;${\bf then }{\rm{cons}}\,({\rm{car}}\,({\it{a\/}}), {\rm{domain}}\,({\it{map\/}})\index{domain}) \\ 
{\bf else }{\rm{domain}}\,({\it{map\/}})\index{domain}$\;${\bf  endif}\-\-
\end{tabbing}

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

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


\noindent{\sc Event}:   Disable domain.

\addvspace{18pt}

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

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

\begin{tabbing}{\sc Theorem}:  range-append \\ \index{range-append}
{\rm{range}}\,({\rm{append}}\,({\it{s1\/}}, {\it{s2\/}}))\index{range} $=$ {\rm{append}}\,({\rm{range}}\,({\it{s1\/}})\index{range}, {\rm{range}}\,({\it{s2\/}})\index{range})
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  range-cons \\ \index{range-cons}
\=\+{\rm{range}}\,({\rm{cons}}\,({\it{a\/}}, {\it{map\/}}))\index{range} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{a\/}})$\;\;${\bf then }{\rm{cons}}\,({\rm{cdr}}\,({\it{a\/}}), {\rm{range}}\,({\it{map\/}})\index{range}) \\ 
{\bf else }{\rm{range}}\,({\it{map\/}})\index{range}$\;${\bf  endif}\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable range.

\addvspace{18pt}

\begin{verbatim};; BOUNDP has been eliminated in favor of membership in domain.
;; Notice that I have to talk about things like disjointness of
;; domains anyhow.  New definition body would be (member x (domain map)).

;(defn boundp (x map)
;  (if (listp map)
;      (if (listp (car map))
;          (if (equal x (caar map))
;              t
;            (boundp x (cdr map)))
;        (boundp x (cdr map)))
;    f))

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

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

\begin{tabbing}{\sc Theorem}:  value-cons \\ \index{value-cons}
\=\+{\rm{value}}\,({\it{x\/}}, {\rm{cons}}\,({\it{pair\/}}, {\it{map\/}}))\index{value} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{pair\/}}) $\wedge$ ({\it{x\/}} $=$ {\rm{car}}\,({\it{pair\/}}))$\;\;${\bf then }{\rm{cdr}}\,({\it{pair\/}}) \\ 
{\bf else }{\rm{value}}\,({\it{x\/}}, {\it{map\/}})\index{value}$\;${\bf  endif}\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable value.

\addvspace{18pt}

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

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

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

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

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

\begin{tabbing}{\sc Theorem}:  invert-cons \\ \index{invert-cons}
\=\+{\rm{invert}}\,({\rm{cons}}\,({\it{pair\/}}, {\it{map\/}}))\index{invert} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{pair\/}})$\;\;${\bf then }{\rm{cons}}\,({\rm{cons}}\,({\rm{cdr}}\,({\it{pair\/}}), {\rm{car}}\,({\it{pair\/}})), {\rm{invert}}\,({\it{map\/}})\index{invert}) \\ 
{\bf else }{\rm{invert}}\,({\it{map\/}})\index{invert}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  value-invert-not-member-of-domain \\ \index{value-invert-not-member-of-domai!n}
\=\+(({\it{g\/}} $\in$ {\rm{range}}\,({\it{sg\/}})\index{range}) $\wedge$ {\rm{disjoint}}\,({\rm{domain}}\,({\it{s\/}})\index{domain}, {\rm{domain}}\,({\it{sg\/}})\index{domain})\index{disjoint}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{value}}\,({\it{g\/}}, {\rm{invert}}\,({\it{sg\/}})\index{invert})\index{value} $\not\in$ {\rm{domain}}\,({\it{s\/}})\index{domain})\-
\end{tabbing}


\noindent{\sc Event}:   Disable invert.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{mapping}$\;\;$
{\rm{mapping}}\,({\it{map\/}})\index{mapping} $=$ ({\rm{alistp}}\,({\it{map\/}})\index{alistp} $\wedge$ {\rm{setp}}\,({\rm{domain}}\,({\it{map\/}})\index{domain})\index{setp})
\end{tabbing}

\begin{verbatim};; For when we disable mapping:
\end{verbatim}\begin{tabbing}{\sc Theorem}:  mapping-implies-alistp \\ \index{mapping-implies-alistp}
{\rm{mapping}}\,({\it{map\/}})\index{mapping} $\rightarrow$ {\rm{alistp}}\,({\it{map\/}})\index{alistp}
\end{tabbing}

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

\begin{tabbing}{\sc Definition}:\index{restrict} \\  
\=\+{\rm{restrict}}\,({\it{s\/}}, {\it{new-domain\/}})\index{restrict} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{s\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{listp}}\,({\rm{car}}\,({\it{s\/}})) $\wedge$ ({\rm{caar}}\,({\it{s\/}}) $\in$ {\it{new-domain\/}}) \\ 
{\bf then }{\rm{cons}}\,({\rm{car}}\,({\it{s\/}}), {\rm{restrict}}\,({\rm{cdr}}\,({\it{s\/}}), {\it{new-domain\/}})\index{restrict}) \\ 
{\bf else }{\rm{restrict}}\,({\rm{cdr}}\,({\it{s\/}}), {\it{new-domain\/}})\index{restrict}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{co-restrict} \\  
\=\+{\rm{co-restrict}}\,({\it{s\/}}, {\it{new-domain\/}})\index{co-restrict} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{s\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{listp}}\,({\rm{car}}\,({\it{s\/}})) $\wedge$ ({\rm{caar}}\,({\it{s\/}}) $\not\in$ {\it{new-domain\/}}) \\ 
{\bf then }{\rm{cons}}\,({\rm{car}}\,({\it{s\/}}), {\rm{co-restrict}}\,({\rm{cdr}}\,({\it{s\/}}), {\it{new-domain\/}})\index{co-restrict}) \\ 
{\bf else }{\rm{co-restrict}}\,({\rm{cdr}}\,({\it{s\/}}), {\it{new-domain\/}})\index{co-restrict}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}


\noindent{\sc Event}:   Let us define the theory {\it{alist-defns}} to consist of the following events: alistp,
domain,
range,
value,
bind,
rembind,
invert,
mapping,
restrict,
co-restrict.\index{alist-defns}

\addvspace{18pt}

\begin{verbatim};;;;; alist lemmas

; DOMAIN

;; The following was proved in the course of the final run through
;; the generalization proof.  The one after it isn't needed but
;; seems like it's worth proving too.  Actually now I see that
;; some other lemmas are now obsolete, so I'll put these both
;; early in the file and delete the others.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  domain-restrict \\ \index{domain-restrict}
{\rm{domain}}\,({\rm{restrict}}\,({\it{s\/}}, {\it{dom\/}})\index{restrict})\index{domain} $=$ {\rm{intersection}}\,({\rm{domain}}\,({\it{s\/}})\index{domain}, {\it{dom\/}})\index{intersection}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  domain-co-restrict \\ \index{domain-co-restrict}
{\rm{domain}}\,({\rm{co-restrict}}\,({\it{s\/}}, {\it{dom\/}})\index{co-restrict})\index{domain} $=$ {\rm{set-diff}}\,({\rm{domain}}\,({\it{s\/}})\index{domain}, {\it{dom\/}})\index{set-diff}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  domain-bind \\ \index{domain-bind}
\=\+{\rm{domain}}\,({\rm{bind}}\,({\it{x\/}}, {\it{v\/}}, {\it{map\/}})\index{bind})\index{domain} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\in$ {\rm{domain}}\,({\it{map\/}})\index{domain}$\;\;${\bf then }{\rm{domain}}\,({\it{map\/}})\index{domain} \\ 
{\bf else }{\rm{append}}\,({\rm{domain}}\,({\it{map\/}})\index{domain}, {\rm{list}}\,({\it{x\/}}))$\;${\bf  endif}\-\-
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  domain-invert \\ \index{domain-invert}
{\rm{domain}}\,({\rm{invert}}\,({\it{map\/}})\index{invert})\index{domain} $=$ {\rm{range}}\,({\it{map\/}})\index{range}
\end{tabbing}

\begin{verbatim}; RANGE

\end{verbatim}\begin{tabbing}{\sc Theorem}:  range-invert \\ \index{range-invert}
{\rm{range}}\,({\rm{invert}}\,({\it{map\/}})\index{invert})\index{range} $=$ {\rm{domain}}\,({\it{map\/}})\index{domain}
\end{tabbing}

\begin{verbatim}; BOUNDP

\end{verbatim}\begin{tabbing}{\sc Theorem}:  boundp-bind \\ \index{boundp-bind}
({\it{x\/}} $\in$ {\rm{domain}}\,({\rm{bind}}\,({\it{y\/}}, {\it{v\/}}, {\it{map\/}})\index{bind})\index{domain}) $=$ (({\it{x\/}} $=$ {\it{y\/}}) $\vee$ ({\it{x\/}} $\in$ {\rm{domain}}\,({\it{map\/}})\index{domain}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  boundp-rembind \\ \index{boundp-rembind}
\=\+{\rm{mapping}}\,({\it{map\/}})\index{mapping} \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\it{x\/}} $\in$ {\rm{domain}}\,({\rm{rembind}}\,({\it{y\/}}, {\it{map\/}})\index{rembind})\index{domain}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $=$ {\it{y\/}}$\;\;${\bf then }{\bf{f}} \\ 
{\bf else }{\it{x\/}} $\in$ {\rm{domain}}\,({\it{map\/}})\index{domain}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  boundp-subsetp \\ \index{boundp-subsetp}
\=\+({\rm{subsetp}}\,({\it{map1\/}}, {\it{map2\/}})\index{subsetp} $\wedge$ ({\it{name\/}} $\in$ {\rm{domain}}\,({\it{map1\/}})\index{domain})) \\ 
$\rightarrow$$\;\;\;\;$({\it{name\/}} $\in$ {\rm{domain}}\,({\it{map2\/}})\index{domain})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  disjoint-domain-singleton \\ \index{disjoint-domain-singleton}
\=\+({\rm{disjoint}}\,({\rm{domain}}\,({\it{s\/}})\index{domain}, {\rm{list}}\,({\it{x\/}}))\index{disjoint} $=$ ({\it{x\/}} $\not\in$ {\rm{domain}}\,({\it{s\/}})\index{domain})) \\ 
$\wedge$$\;\;\;\;$({\rm{disjoint}}\,({\rm{list}}\,({\it{x\/}}), {\rm{domain}}\,({\it{s\/}})\index{domain})\index{disjoint} $=$ ({\it{x\/}} $\not\in$ {\rm{domain}}\,({\it{s\/}})\index{domain}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  boundp-value-invert \\ \index{boundp-value-invert}
({\it{x\/}} $\in$ {\rm{range}}\,({\it{map\/}})\index{range}) $\rightarrow$ ({\rm{value}}\,({\it{x\/}}, {\rm{invert}}\,({\it{map\/}})\index{invert})\index{value} $\in$ {\rm{domain}}\,({\it{map\/}})\index{domain})
\end{tabbing}

\begin{verbatim}; VALUE

\end{verbatim}\begin{tabbing}{\sc Theorem}:  value-when-not-bound \\ \index{value-when-not-bound}
({\it{name\/}} $\not\in$ {\rm{domain}}\,({\it{map\/}})\index{domain}) $\rightarrow$ ({\rm{value}}\,({\it{name\/}}, {\it{map\/}})\index{value} $=$ {\tt{0}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  value-bind \\ \index{value-bind}
\=\+{\rm{value}}\,({\it{x\/}}, {\rm{bind}}\,({\it{y\/}}, {\it{v\/}}, {\it{map\/}})\index{bind})\index{value} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $=$ {\it{y\/}}$\;\;${\bf then }{\it{v\/}} \\ 
{\bf else }{\rm{value}}\,({\it{x\/}}, {\it{map\/}})\index{value}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  value-rembind \\ \index{value-rembind}
\=\+{\rm{mapping}}\,({\it{map\/}})\index{mapping} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{value}}\,({\it{x\/}}, {\rm{rembind}}\,({\it{y\/}}, {\it{map\/}})\index{rembind})\index{value} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $=$ {\it{y\/}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\rm{value}}\,({\it{x\/}}, {\it{map\/}})\index{value}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  value-append \\ \index{value-append}
\=\+{\rm{value}}\,({\it{x\/}}, {\rm{append}}\,({\it{s1\/}}, {\it{s2\/}}))\index{value} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\in$ {\rm{domain}}\,({\it{s1\/}})\index{domain}$\;\;${\bf then }{\rm{value}}\,({\it{x\/}}, {\it{s1\/}})\index{value} \\ 
{\bf else }{\rm{value}}\,({\it{x\/}}, {\it{s2\/}})\index{value}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  value-value-invert \\ \index{value-value-invert}
(({\it{x\/}} $\in$ {\rm{range}}\,({\it{s\/}})\index{range}) $\wedge$ {\rm{mapping}}\,({\it{s\/}})\index{mapping}) $\rightarrow$ ({\rm{value}}\,({\rm{value}}\,({\it{x\/}}, {\rm{invert}}\,({\it{s\/}})\index{invert})\index{value}, {\it{s\/}})\index{value} $=$ {\it{x\/}})
\end{tabbing}

\begin{verbatim}; MAPPING

\end{verbatim}\begin{tabbing}{\sc Theorem}:  mapping-append \\ \index{mapping-append}
\=\+{\rm{mapping}}\,({\rm{append}}\,({\it{s1\/}}, {\it{s2\/}}))\index{mapping} \\ 
$=$$\;\;\;\;$(\=\+{\rm{disjoint}}\,({\rm{domain}}\,({\it{s1\/}})\index{domain}, {\rm{domain}}\,({\it{s2\/}})\index{domain})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{mapping}}\,({\rm{fix-properp}}\,({\it{s1\/}})\index{fix-properp})\index{mapping} \\ 
$\wedge$$\;\;\;\;${\rm{mapping}}\,({\it{s2\/}})\index{mapping})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable mapping.

\addvspace{18pt}

\begin{verbatim};; RESTRICT and CO-RESTRICT

\end{verbatim}\begin{tabbing}{\sc Theorem}:  alistp-restrict \\ \index{alistp-restrict}
{\rm{alistp}}\,({\rm{restrict}}\,({\it{s\/}}, {\it{r\/}})\index{restrict})\index{alistp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  alistp-co-restrict \\ \index{alistp-co-restrict}
{\rm{alistp}}\,({\rm{co-restrict}}\,({\it{s\/}}, {\it{r\/}})\index{co-restrict})\index{alistp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  value-restrict \\ \index{value-restrict}
\=\+(({\it{a\/}} $\in$ {\it{r\/}}) $\wedge$ ({\it{a\/}} $\in$ {\rm{domain}}\,({\it{s\/}})\index{domain})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{value}}\,({\it{a\/}}, {\rm{restrict}}\,({\it{s\/}}, {\it{r\/}})\index{restrict})\index{value} $=$ {\rm{value}}\,({\it{a\/}}, {\it{s\/}})\index{value})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  value-co-restrict \\ \index{value-co-restrict}
\=\+(({\it{a\/}} $\not\in$ {\it{r\/}}) $\wedge$ ({\it{a\/}} $\in$ {\rm{domain}}\,({\it{s\/}})\index{domain})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{value}}\,({\it{a\/}}, {\rm{co-restrict}}\,({\it{s\/}}, {\it{r\/}})\index{co-restrict})\index{value} $=$ {\rm{value}}\,({\it{a\/}}, {\it{s\/}})\index{value})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mapping-restrict \\ \index{mapping-restrict}
{\rm{mapping}}\,({\it{s\/}})\index{mapping} $\rightarrow$ {\rm{mapping}}\,({\rm{restrict}}\,({\it{s\/}}, {\it{x\/}})\index{restrict})\index{mapping}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mapping-co-restrict \\ \index{mapping-co-restrict}
{\rm{mapping}}\,({\it{s\/}})\index{mapping} $\rightarrow$ {\rm{mapping}}\,({\rm{co-restrict}}\,({\it{s\/}}, {\it{x\/}})\index{co-restrict})\index{mapping}
\end{tabbing}


\noindent{\sc Event}:   Disable restrict.

\addvspace{18pt}

\noindent{\sc Event}:   Disable co-restrict.

\addvspace{18pt}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; terms.events file
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Requires deftheory and constrain enhancments.
;; Requires sets and alists libraries.

;; This is a library of events about terms, including substitutions.
;; A TERMP is either a variable or the application of a function
;; symbol to a "proper list" of terms.  Variables and function symbols
;; are introduced with CONSTRAIN.

;; NOTE:  In functions like TERMP that have a flag, it seems to be
;; important to use T and F rather than, say, T and 'LIST.  That's
;; because otherwise, the "worse-than" heuristic will otherwise
;; prevent some necessary backchaining in cases where the hypothesis
;; to be relieved is of the form (TERMP 'LIST ...) and an "ancestor"
;; is of the form (TERMP T ...).

;; Definitions:

;; (deftheory term-defns
;;  (variablep-intro variable-listp termp function-symbol-intro all-vars))

;; (deftheory substitution-defns
;;   (instance var-substp compose apply-to-subst subst
;;    nullify-subst ;; returns a substitution whose range has no variables
;;    ))

\end{verbatim}\begin{tabbing}{\sc Conservative Axiom}:  variablep-intro \\ \index{variablep-intro}
\=\+({\rm{listp}}\,({\it{x\/}}) $\rightarrow$ ($\neg$ {\rm{variablep}}\,({\it{x\/}})\index{variablep})) \\ 
$\wedge$$\;\;\;\;$({\rm{truep}}\,({\rm{variablep}}\,({\it{x\/}})\index{variablep}) $\vee$ {\rm{falsep}}\,({\rm{variablep}}\,({\it{x\/}})\index{variablep}))\-
\end{tabbing}\noindent Simultaneously, we introduce the new function symbol {\it variablep\/}.

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

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

\begin{tabbing}{\sc Theorem}:  variable-listp-cons \\ \index{variable-listp-cons}
{\rm{variable-listp}}\,({\rm{cons}}\,({\it{a\/}}, {\it{x\/}}))\index{variable-listp} $=$ ({\rm{variablep}}\,({\it{a\/}})\index{variablep} $\wedge$ {\rm{variable-listp}}\,({\it{x\/}})\index{variable-listp})
\end{tabbing}

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


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

\addvspace{18pt}

\begin{tabbing}{\sc Conservative Axiom}:  function-symbol-intro \\ \index{function-symbol-intro}
{\rm{function-symbol-p}}\,({\sc{fn}}\index{fn})\index{function-symbol-p}
\end{tabbing}\noindent Simultaneously, we introduce the new function symbols {\it function-symbol-p\/} and {\it fn\/}.

\begin{tabbing}{\sc Definition}:\index{termp} \\  
\=\+{\rm{termp}}\,({\it{flg\/}}, {\it{x\/}})\index{termp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{flg\/}} \\ 
{\bf then }\=\+{\bf if }{\rm{variablep}}\,({\it{x\/}})\index{variablep}$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\rm{listp}}\,({\it{x\/}}) \\ 
{\bf then }{\rm{function-symbol-p}}\,({\rm{car}}\,({\it{x\/}}))\index{function-symbol-p} $\wedge$ {\rm{termp}}\,({\bf{f}}, {\rm{cdr}}\,({\it{x\/}}))\index{termp} \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\- \\ 
{\bf elseif }{\rm{listp}}\,({\it{x\/}})$\;\;${\bf then }{\rm{termp}}\,({\bf{t}}, {\rm{car}}\,({\it{x\/}}))\index{termp} $\wedge$ {\rm{termp}}\,({\bf{f}}, {\rm{cdr}}\,({\it{x\/}}))\index{termp} \\ 
{\bf else }{\it{x\/}} $=$ {\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  termp-list-cons \\ \index{termp-list-cons}
{\rm{termp}}\,({\bf{f}}, {\rm{cons}}\,({\it{a\/}}, {\it{x\/}}))\index{termp} $=$ ({\rm{termp}}\,({\bf{t}}, {\it{a\/}})\index{termp} $\wedge$ {\rm{termp}}\,({\bf{f}}, {\it{x\/}})\index{termp})
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  termp-t-cons \\ \index{termp-t-cons}
{\it{flg\/}} $\rightarrow$ ({\rm{termp}}\,({\it{flg\/}}, {\rm{cons}}\,({\it{a\/}}, {\it{x\/}}))\index{termp} $=$ ({\rm{function-symbol-p}}\,({\it{a\/}})\index{function-symbol-p} $\wedge$ {\rm{termp}}\,({\bf{f}}, {\it{x\/}})\index{termp}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  termp-t-nlistp \\ \index{termp-t-nlistp}
({\it{flg\/}} $\wedge$ ($\neg$ {\rm{listp}}\,({\it{x\/}}))) $\rightarrow$ ({\rm{termp}}\,({\it{flg\/}}, {\it{x\/}})\index{termp} $=$ {\rm{variablep}}\,({\it{x\/}})\index{variablep})
\end{tabbing}


\noindent{\sc Event}:   Disable termp.

\addvspace{18pt}

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

\begin{tabbing}{\sc Definition}:\index{all-vars} \\  
\=\+{\rm{all-vars}}\,({\it{flg\/}}, {\it{x\/}})\index{all-vars} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{flg\/}} \\ 
{\bf then }\=\+{\bf if }{\rm{variablep}}\,({\it{x\/}})\index{variablep}$\;\;${\bf then }{\rm{list}}\,({\it{x\/}}) \\ 
{\bf elseif }{\rm{listp}}\,({\it{x\/}})$\;\;${\bf then }{\rm{all-vars}}\,({\bf{f}}, {\rm{cdr}}\,({\it{x\/}}))\index{all-vars} \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\- \\ 
{\bf elseif }{\rm{listp}}\,({\it{x\/}})$\;\;${\bf then }{\rm{append}}\,({\rm{all-vars}}\,({\bf{t}}, {\rm{car}}\,({\it{x\/}}))\index{all-vars}, {\rm{all-vars}}\,({\bf{f}}, {\rm{cdr}}\,({\it{x\/}}))\index{all-vars}) \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  all-vars-list-cons \\ \index{all-vars-list-cons}
{\rm{all-vars}}\,({\bf{f}}, {\rm{cons}}\,({\it{a\/}}, {\it{x\/}}))\index{all-vars} $=$ {\rm{append}}\,({\rm{all-vars}}\,({\bf{t}}, {\it{a\/}})\index{all-vars}, {\rm{all-vars}}\,({\bf{f}}, {\it{x\/}})\index{all-vars})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-vars-t-cons \\ \index{all-vars-t-cons}
{\it{flg\/}} $\rightarrow$ ({\rm{all-vars}}\,({\it{flg\/}}, {\rm{cons}}\,({\it{a\/}}, {\it{x\/}}))\index{all-vars} $=$ {\rm{all-vars}}\,({\bf{f}}, {\it{x\/}})\index{all-vars})
\end{tabbing}

\begin{verbatim};; Here is a hack to deal with the flags.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  all-vars-subsetp-append-hack \\ \index{all-vars-subsetp-append-hack}
\=\+({\it{flg1\/}} $\wedge$ {\it{flg2\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{subsetp}}\,({\rm{all-vars}}\,({\it{flg1\/}}, {\it{x\/}})\index{all-vars}, {\rm{append}}\,({\rm{all-vars}}\,({\it{flg2\/}}, {\it{x\/}})\index{all-vars}, {\it{y\/}}))\index{subsetp} \\ 
$\wedge$$\;\;\;\;${\rm{subsetp}}\,({\rm{all-vars}}\,({\it{flg1\/}}, {\it{x\/}})\index{all-vars}, {\rm{append}}\,({\it{y\/}}, {\rm{all-vars}}\,({\it{flg2\/}}, {\it{x\/}})\index{all-vars}))\index{subsetp})\-\-
\end{tabbing}

\begin{verbatim};; The following is used later in the proof of MEMBER-PRESERVES-DISJOINT-ALL-VARS
;; and could conceivably be of use elsewhere.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  all-vars-flg-boolean \\ \index{all-vars-flg-boolean}
{\it{flg\/}} $\rightarrow$ ({\rm{all-vars}}\,({\it{flg\/}}, {\it{x\/}})\index{all-vars} $=$ {\rm{all-vars}}\,({\bf{t}}, {\it{x\/}})\index{all-vars})
\end{tabbing}


\noindent{\sc Event}:   Disable all-vars.

\addvspace{18pt}


\noindent{\sc Event}:   Let us define the theory {\it{term-defns}} to consist of the following events: variablep-intro,
variable-listp,
termp,
function-symbol-intro,
all-vars.\index{term-defns}

\addvspace{18pt}

\begin{verbatim};;;;; lemmas about termps

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

\begin{tabbing}{\sc Theorem}:  all-vars-variablep \\ \index{all-vars-variablep}
({\it{flg\/}} $\wedge$ {\rm{variablep}}\,({\it{x\/}})\index{variablep}) $\rightarrow$ ({\rm{all-vars}}\,({\it{flg\/}}, {\it{x\/}})\index{all-vars} $=$ {\rm{list}}\,({\it{x\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member-variable-listp-implies-variablep \\ \index{member-variable-listp-implies-v!ariablep}
(({\it{a\/}} $\in$ {\it{x\/}}) $\wedge$ {\rm{variable-listp}}\,({\it{x\/}})\index{variable-listp}) $\rightarrow$ {\rm{variablep}}\,({\it{a\/}})\index{variablep}
\end{tabbing}

\begin{verbatim};; The following was proved in the course of the final run through the
;; generalization proof.  But in fact it's useful for the next result,
;; especially in the presence of domain-restrict -- so I don't need to
;; enable restrict there any longer.  Similarly for the lemma after
;; that.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  variable-listp-intersection \\ \index{variable-listp-intersection}
\=\+({\rm{variable-listp}}\,({\it{x\/}})\index{variable-listp} $\vee$ {\rm{variable-listp}}\,({\it{y\/}})\index{variable-listp}) \\ 
$\rightarrow$$\;\;\;\;${\rm{variable-listp}}\,({\rm{intersection}}\,({\it{x\/}}, {\it{y\/}})\index{intersection})\index{variable-listp}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  variable-listp-domain-restrict \\ \index{variable-listp-domain-restrict}
{\rm{variable-listp}}\,({\rm{domain}}\,({\it{s\/}})\index{domain})\index{variable-listp} $\rightarrow$ {\rm{variable-listp}}\,({\rm{domain}}\,({\rm{restrict}}\,({\it{s\/}}, {\it{x\/}})\index{restrict})\index{domain})\index{variable-listp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  variable-listp-domain-co-restrict \\ \index{variable-listp-domain-co-restri!ct}
{\rm{variable-listp}}\,({\rm{domain}}\,({\it{s\/}})\index{domain})\index{variable-listp} $\rightarrow$ {\rm{variable-listp}}\,({\rm{domain}}\,({\rm{co-restrict}}\,({\it{s\/}}, {\it{x\/}})\index{co-restrict})\index{domain})\index{variable-listp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  termp-range-restrict \\ \index{termp-range-restrict}
{\rm{termp}}\,({\bf{f}}, {\rm{range}}\,({\it{s\/}})\index{range})\index{termp} $\rightarrow$ {\rm{termp}}\,({\bf{f}}, {\rm{range}}\,({\rm{restrict}}\,({\it{s\/}}, {\it{x\/}})\index{restrict})\index{range})\index{termp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  termp-range-co-restrict \\ \index{termp-range-co-restrict}
{\rm{termp}}\,({\bf{f}}, {\rm{range}}\,({\it{s\/}})\index{range})\index{termp} $\rightarrow$ {\rm{termp}}\,({\bf{f}}, {\rm{range}}\,({\rm{co-restrict}}\,({\it{s\/}}, {\it{x\/}})\index{co-restrict})\index{range})\index{termp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member-preserves-disjoint-all-vars-lemma \\ \index{member-preserves-disjoint-all-v!ars-lemma}
({\rm{disjoint}}\,({\it{y\/}}, {\rm{all-vars}}\,({\bf{f}}, {\it{x\/}})\index{all-vars})\index{disjoint} $\wedge$ ({\it{g\/}} $\in$ {\it{x\/}})) $\rightarrow$ {\rm{disjoint}}\,({\it{y\/}}, {\rm{all-vars}}\,({\bf{t}}, {\it{g\/}})\index{all-vars})\index{disjoint}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member-preserves-disjoint-all-vars \\ \index{member-preserves-disjoint-all-v!ars}
\=\+({\it{flg\/}} $\wedge$ {\rm{disjoint}}\,({\it{y\/}}, {\rm{all-vars}}\,({\bf{f}}, {\it{x\/}})\index{all-vars})\index{disjoint} $\wedge$ ({\it{g\/}} $\in$ {\it{x\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{disjoint}}\,({\it{y\/}}, {\rm{all-vars}}\,({\it{flg\/}}, {\it{g\/}})\index{all-vars})\index{disjoint}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member-all-vars-subsetp \\ \index{member-all-vars-subsetp}
({\it{flg\/}} $\wedge$ ({\it{a\/}} $\in$ {\it{x\/}})) $\rightarrow$ {\rm{subsetp}}\,({\rm{all-vars}}\,({\it{flg\/}}, {\it{a\/}})\index{all-vars}, {\rm{all-vars}}\,({\bf{f}}, {\it{x\/}})\index{all-vars})\index{subsetp}
\end{tabbing}

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

\begin{verbatim};;;;; substitutions:  definitions

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{var-substp} \\  
\=\+{\rm{var-substp}}\,({\it{s\/}})\index{var-substp} \\ 
$=$$\;\;\;\;$({\rm{mapping}}\,({\it{s\/}})\index{mapping} $\wedge$ {\rm{variable-listp}}\,({\rm{domain}}\,({\it{s\/}})\index{domain})\index{variable-listp} $\wedge$ {\rm{termp}}\,({\bf{f}}, {\rm{range}}\,({\it{s\/}})\index{range})\index{termp})\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{subst} \\  
\=\+{\rm{subst}}\,({\it{flg\/}}, {\it{s\/}}, {\it{x\/}})\index{subst} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{flg\/}} \\ 
{\bf then }\=\+{\bf if }{\it{x\/}} $\in$ {\rm{domain}}\,({\it{s\/}})\index{domain}$\;\;${\bf then }{\rm{value}}\,({\it{x\/}}, {\it{s\/}})\index{value} \\ 
{\bf elseif }{\rm{variablep}}\,({\it{x\/}})\index{variablep}$\;\;${\bf then }{\it{x\/}} \\ 
{\bf elseif }{\rm{listp}}\,({\it{x\/}})$\;\;${\bf then }{\rm{cons}}\,({\rm{car}}\,({\it{x\/}}), {\rm{subst}}\,({\bf{f}}, {\it{s\/}}, {\rm{cdr}}\,({\it{x\/}}))\index{subst}) \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\- \\ 
{\bf elseif }{\rm{listp}}\,({\it{x\/}})$\;\;${\bf then }{\rm{cons}}\,({\rm{subst}}\,({\bf{t}}, {\it{s\/}}, {\rm{car}}\,({\it{x\/}}))\index{subst}, {\rm{subst}}\,({\bf{f}}, {\it{s\/}}, {\rm{cdr}}\,({\it{x\/}}))\index{subst}) \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{apply-to-subst} \\  
\=\+{\rm{apply-to-subst}}\,({\it{s1\/}}, {\it{s2\/}})\index{apply-to-subst} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{s2\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{listp}}\,({\rm{car}}\,({\it{s2\/}})) \\ 
{\bf then }{\rm{cons}}\,(\=\+{\rm{cons}}\,({\rm{caar}}\,({\it{s2\/}}), {\rm{subst}}\,({\bf{t}}, {\it{s1\/}}, {\rm{cdar}}\,({\it{s2\/}}))\index{subst}), \\ 
{\rm{apply-to-subst}}\,({\it{s1\/}}, {\rm{cdr}}\,({\it{s2\/}}))\index{apply-to-subst})\- \\ 
{\bf else }{\rm{apply-to-subst}}\,({\it{s1\/}}, {\rm{cdr}}\,({\it{s2\/}}))\index{apply-to-subst}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{compose}$\;\;$
{\rm{compose}}\,({\it{s1\/}}, {\it{s2\/}})\index{compose} $=$ {\rm{append}}\,({\rm{apply-to-subst}}\,({\it{s2\/}}, {\it{s1\/}})\index{apply-to-subst}, {\it{s2\/}})
\end{tabbing}

\begin{verbatim};; The following was in the original version, but isn't needed.
;;;  (defn-sk instance (flg term1 term2)
;;;    ;; term1 is an instance of term2
;;;    (exists one-way-unifier
;;;            (and (var-substp one-way-unifier)
;;;                 (equal term1 (subst flg one-way-unifier term2)))))

;;;;; substitution lemmas

\end{verbatim}\begin{tabbing}{\sc Theorem}:  subst-list-cons \\ \index{subst-list-cons}
{\rm{subst}}\,({\bf{f}}, {\it{s\/}}, {\rm{cons}}\,({\it{a\/}}, {\it{x\/}}))\index{subst} $=$ {\rm{cons}}\,({\rm{subst}}\,({\bf{t}}, {\it{s\/}}, {\it{a\/}})\index{subst}, {\rm{subst}}\,({\bf{f}}, {\it{s\/}}, {\it{x\/}})\index{subst})
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  subst-t-variablep \\ \index{subst-t-variablep}
\=\+({\it{flg\/}} $\wedge$ {\rm{variablep}}\,({\it{x\/}})\index{variablep}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{subst}}\,({\it{flg\/}}, {\it{s\/}}, {\it{x\/}})\index{subst} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\in$ {\rm{domain}}\,({\it{s\/}})\index{domain}$\;\;${\bf then }{\rm{value}}\,({\it{x\/}}, {\it{s\/}})\index{value} \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subst-t-non-variablep \\ \index{subst-t-non-variablep}
{\it{flg\/}} $\rightarrow$ (\=\+{\rm{subst}}\,({\it{flg\/}}, {\it{s\/}}, {\rm{cons}}\,({\it{fn\/}}, {\it{x\/}}))\index{subst} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{cons}}\,({\it{fn\/}}, {\it{x\/}}) $\in$ {\rm{domain}}\,({\it{s\/}})\index{domain}$\;\;${\bf then }{\rm{value}}\,({\rm{cons}}\,({\it{fn\/}}, {\it{x\/}}), {\it{s\/}})\index{value} \\ 
{\bf else }{\rm{cons}}\,({\it{fn\/}}, {\rm{subst}}\,({\bf{f}}, {\it{s\/}}, {\it{x\/}})\index{subst})$\;${\bf  endif}\-)\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-vars-subst-lemma \\ \index{all-vars-subst-lemma}
\=\+({\it{flg\/}} $\wedge$ ({\it{x\/}} $\in$ {\rm{domain}}\,({\it{s\/}})\index{domain})) \\ 
$\rightarrow$$\;\;\;\;${\rm{subsetp}}\,({\rm{all-vars}}\,({\it{flg\/}}, {\rm{value}}\,({\it{x\/}}, {\it{s\/}})\index{value})\index{all-vars}, {\rm{all-vars}}\,({\bf{f}}, {\rm{range}}\,({\it{s\/}})\index{range})\index{all-vars})\index{subsetp}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-vars-subst \\ \index{all-vars-subst}
\=\+{\rm{termp}}\,({\it{flg\/}}, {\it{x\/}})\index{termp} \\ 
$\rightarrow$$\;\;\;\;${\rm{subsetp}}\,(\=\+{\rm{all-vars}}\,({\it{flg\/}}, {\rm{subst}}\,({\it{flg\/}}, {\it{s\/}}, {\it{x\/}})\index{subst})\index{all-vars}, \\ 
{\rm{append}}\,({\rm{all-vars}}\,({\it{flg\/}}, {\it{x\/}})\index{all-vars}, {\rm{all-vars}}\,({\bf{f}}, {\rm{range}}\,({\it{s\/}})\index{range})\index{all-vars}))\-\index{subsetp}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subst-occur \\ \index{subst-occur}
({\it{flg\/}} $\wedge$ ({\it{x\/}} $\in$ {\rm{domain}}\,({\it{s\/}})\index{domain})) $\rightarrow$ ({\rm{subst}}\,({\it{flg\/}}, {\it{s\/}}, {\it{x\/}})\index{subst} $=$ {\rm{value}}\,({\it{x\/}}, {\it{s\/}})\index{value})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  boundp-in-var-substp-implies-variablep \\ \index{boundp-in-var-substp-implies-va!riablep}
({\rm{variable-listp}}\,({\rm{domain}}\,({\it{s\/}})\index{domain})\index{variable-listp} $\wedge$ ($\neg$ {\rm{variablep}}\,({\it{a\/}})\index{variablep})) $\rightarrow$ ({\it{a\/}} $\not\in$ {\rm{domain}}\,({\it{s\/}})\index{domain})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  variablep-value-invert \\ \index{variablep-value-invert}
\=\+({\rm{variable-listp}}\,({\rm{domain}}\,({\it{s\/}})\index{domain})\index{variable-listp} $\wedge$ ({\it{x\/}} $\in$ {\rm{range}}\,({\it{s\/}})\index{range})) \\ 
$\rightarrow$$\;\;\;\;${\rm{variablep}}\,({\rm{value}}\,({\it{x\/}}, {\rm{invert}}\,({\it{s\/}})\index{invert})\index{value})\index{variablep}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subst-invert \\ \index{subst-invert}
\=\+({\rm{termp}}\,({\it{flg\/}}, {\it{x\/}})\index{termp} $\wedge$ {\rm{disjoint}}\,({\rm{domain}}\,({\it{s\/}})\index{domain}, {\rm{all-vars}}\,({\it{flg\/}}, {\it{x\/}})\index{all-vars})\index{disjoint} $\wedge$ {\rm{var-substp}}\,({\it{s\/}})\index{var-substp}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{subst}}\,({\it{flg\/}}, {\it{s\/}}, {\rm{subst}}\,({\it{flg\/}}, {\rm{invert}}\,({\it{s\/}})\index{invert}, {\it{x\/}})\index{subst})\index{subst} $=$ {\it{x\/}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  boundp-apply-to-subst \\ \index{boundp-apply-to-subst}
({\it{x\/}} $\in$ {\rm{domain}}\,({\rm{apply-to-subst}}\,({\it{s1\/}}, {\it{s2\/}})\index{apply-to-subst})\index{domain}) $=$ ({\it{x\/}} $\in$ {\rm{domain}}\,({\it{s2\/}})\index{domain})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mapping-apply-to-subst \\ \index{mapping-apply-to-subst}
{\rm{mapping}}\,({\it{s\/}})\index{mapping} $\rightarrow$ {\rm{mapping}}\,({\rm{apply-to-subst}}\,({\it{s1\/}}, {\it{s\/}})\index{apply-to-subst})\index{mapping}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  alistp-apply-to-subst \\ \index{alistp-apply-to-subst}
{\rm{alistp}}\,({\rm{apply-to-subst}}\,({\it{s1\/}}, {\it{s2\/}})\index{apply-to-subst})\index{alistp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subst-flg-not-list \\ \index{subst-flg-not-list}
{\it{flg\/}} $\rightarrow$ (\=\+(({\rm{subst}}\,({\it{flg\/}}, {\it{s\/}}, {\it{x\/}})\index{subst} $=$ {\rm{subst}}\,({\bf{t}}, {\it{s\/}}, {\it{x\/}})\index{subst}) $=$ {\bf{t}}) \\ 
$\wedge$$\;\;\;\;$(({\rm{subst}}\,({\bf{t}}, {\it{s\/}}, {\it{x\/}})\index{subst} $=$ {\rm{subst}}\,({\it{flg\/}}, {\it{s\/}}, {\it{x\/}})\index{subst}) $=$ {\bf{t}}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subst-co-restrict \\ \index{subst-co-restrict}
\=\+(\=\+{\rm{disjoint}}\,({\it{x\/}}, {\rm{intersection}}\,({\rm{domain}}\,({\it{s\/}})\index{domain}, {\rm{all-vars}}\,({\it{flg\/}}, {\it{term\/}})\index{all-vars})\index{intersection})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{variable-listp}}\,({\rm{domain}}\,({\it{s\/}})\index{domain})\index{variable-listp} \\ 
$\wedge$$\;\;\;\;${\rm{termp}}\,({\it{flg\/}}, {\it{term\/}})\index{termp})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{subst}}\,({\it{flg\/}}, {\rm{co-restrict}}\,({\it{s\/}}, {\it{x\/}})\index{co-restrict}, {\it{term\/}})\index{subst} $=$ {\rm{subst}}\,({\it{flg\/}}, {\it{s\/}}, {\it{term\/}})\index{subst})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subst-restrict \\ \index{subst-restrict}
\=\+(\=\+{\rm{subsetp}}\,({\rm{intersection}}\,({\rm{domain}}\,({\it{s\/}})\index{domain}, {\rm{all-vars}}\,({\it{flg\/}}, {\it{term\/}})\index{all-vars})\index{intersection}, {\it{x\/}})\index{subsetp} \\ 
$\wedge$$\;\;\;\;${\rm{variable-listp}}\,({\rm{domain}}\,({\it{s\/}})\index{domain})\index{variable-listp} \\ 
$\wedge$$\;\;\;\;${\rm{termp}}\,({\it{flg\/}}, {\it{term\/}})\index{termp})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{subst}}\,({\it{flg\/}}, {\rm{restrict}}\,({\it{s\/}}, {\it{x\/}})\index{restrict}, {\it{term\/}})\index{subst} $=$ {\rm{subst}}\,({\it{flg\/}}, {\it{s\/}}, {\it{term\/}})\index{subst})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  termp-value \\ \index{termp-value}
({\it{flg\/}} $\wedge$ ({\it{x\/}} $\in$ {\rm{domain}}\,({\it{s\/}})\index{domain}) $\wedge$ {\rm{termp}}\,({\bf{f}}, {\rm{range}}\,({\it{s\/}})\index{range})\index{termp}) $\rightarrow$ {\rm{termp}}\,({\it{flg\/}}, {\rm{value}}\,({\it{x\/}}, {\it{s\/}})\index{value})\index{termp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  termp-subst \\ \index{termp-subst}
({\rm{termp}}\,({\it{flg\/}}, {\it{x\/}})\index{termp} $\wedge$ {\rm{termp}}\,({\bf{f}}, {\rm{range}}\,({\it{s\/}})\index{range})\index{termp}) $\rightarrow$ {\rm{termp}}\,({\it{flg\/}}, {\rm{subst}}\,({\it{flg\/}}, {\it{s\/}}, {\it{x\/}})\index{subst})\index{termp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  termp-domain \\ \index{termp-domain}
{\rm{variable-listp}}\,({\rm{domain}}\,({\it{s\/}})\index{domain})\index{variable-listp} $\rightarrow$ {\rm{termp}}\,({\bf{f}}, {\rm{domain}}\,({\it{s\/}})\index{domain})\index{termp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  domain-apply-to-subst \\ \index{domain-apply-to-subst}
{\rm{domain}}\,({\rm{apply-to-subst}}\,({\it{s1\/}}, {\it{s2\/}})\index{apply-to-subst})\index{domain} $=$ {\rm{domain}}\,({\it{s2\/}})\index{domain}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  var-substp-apply-to-subst \\ \index{var-substp-apply-to-subst}
\=\+({\rm{termp}}\,({\bf{f}}, {\rm{range}}\,({\it{s\/}})\index{range})\index{termp} $\wedge$ {\rm{termp}}\,({\bf{f}}, {\rm{range}}\,({\it{sg\/}})\index{range})\index{termp}) \\ 
$\rightarrow$$\;\;\;\;${\rm{termp}}\,({\bf{f}}, {\rm{range}}\,({\rm{apply-to-subst}}\,({\it{sg\/}}, {\it{s\/}})\index{apply-to-subst})\index{range})\index{termp}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  value-apply-to-subst \\ \index{value-apply-to-subst}
\=\+({\it{g\/}} $\in$ {\rm{domain}}\,({\it{s\/}})\index{domain}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{value}}\,({\it{g\/}}, {\rm{apply-to-subst}}\,({\it{sg\/}}, {\it{s\/}})\index{apply-to-subst})\index{value} $=$ {\rm{subst}}\,({\bf{t}}, {\it{sg\/}}, {\rm{value}}\,({\it{g\/}}, {\it{s\/}})\index{value})\index{subst})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  non-variablep-not-member-of-variable-listp \\ \index{non-variablep-not-member-of-vari!able-listp}
({\rm{variable-listp}}\,({\it{d\/}})\index{variable-listp} $\wedge$ ($\neg$ {\rm{variablep}}\,({\it{term\/}})\index{variablep})) $\rightarrow$ ({\it{term\/}} $\not\in$ {\it{d\/}})
\end{tabbing}
  
\begin{tabbing}{\sc Theorem}:  compose-property \\ \index{compose-property}
\=\+({\rm{variable-listp}}\,({\rm{domain}}\,({\it{s2\/}})\index{domain})\index{variable-listp} $\wedge$ {\rm{termp}}\,({\it{flg\/}}, {\it{x\/}})\index{termp}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{subst}}\,({\it{flg\/}}, {\rm{compose}}\,({\it{s1\/}}, {\it{s2\/}})\index{compose}, {\it{x\/}})\index{subst} $=$ {\rm{subst}}\,({\it{flg\/}}, {\it{s2\/}}, {\rm{subst}}\,({\it{flg\/}}, {\it{s1\/}}, {\it{x\/}})\index{subst})\index{subst})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  compose-property-reversed \\ \index{compose-property-reversed}
\=\+({\rm{variable-listp}}\,({\rm{domain}}\,({\it{s2\/}})\index{domain})\index{variable-listp} $\wedge$ {\rm{termp}}\,({\it{flg\/}}, {\it{x\/}})\index{termp}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{subst}}\,({\it{flg\/}}, {\it{s2\/}}, {\rm{subst}}\,({\it{flg\/}}, {\it{s1\/}}, {\it{x\/}})\index{subst})\index{subst} $=$ {\rm{subst}}\,({\it{flg\/}}, {\rm{compose}}\,({\it{s1\/}}, {\it{s2\/}})\index{compose}, {\it{x\/}})\index{subst})\-
\end{tabbing}


\noindent{\sc Event}:   Disable compose-property.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  subst-not-occur \\ \index{subst-not-occur}
\=\+(\=\+{\rm{termp}}\,({\it{flg\/}}, {\it{x\/}})\index{termp} \\ 
$\wedge$$\;\;\;\;${\rm{variable-listp}}\,({\rm{domain}}\,({\it{s\/}})\index{domain})\index{variable-listp} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{domain}}\,({\it{s\/}})\index{domain}, {\rm{all-vars}}\,({\it{flg\/}}, {\it{x\/}})\index{all-vars})\index{disjoint})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{subst}}\,({\it{flg\/}}, {\it{s\/}}, {\it{x\/}})\index{subst} $=$ {\it{x\/}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  disjoint-range-implies-disjoint-value \\ \index{disjoint-range-implies-disjoint!-value}
\=\+(({\it{x\/}} $\in$ {\rm{domain}}\,({\it{s\/}})\index{domain}) $\wedge$ {\it{flg\/}} $\wedge$ {\rm{disjoint}}\,({\it{z\/}}, {\rm{all-vars}}\,({\bf{f}}, {\rm{range}}\,({\it{s\/}})\index{range})\index{all-vars})\index{disjoint}) \\ 
$\rightarrow$$\;\;\;\;${\rm{disjoint}}\,({\it{z\/}}, {\rm{all-vars}}\,({\it{flg\/}}, {\rm{value}}\,({\it{x\/}}, {\it{s\/}})\index{value})\index{all-vars})\index{disjoint}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  disjoint-all-vars-subst \\ \index{disjoint-all-vars-subst}
\=\+(\=\+{\rm{termp}}\,({\it{flg\/}}, {\it{x\/}})\index{termp} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{z\/}}, {\rm{all-vars}}\,({\it{flg\/}}, {\it{x\/}})\index{all-vars})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{z\/}}, {\rm{all-vars}}\,({\bf{f}}, {\rm{range}}\,({\it{s\/}})\index{range})\index{all-vars})\index{disjoint})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{disjoint}}\,({\it{z\/}}, {\rm{all-vars}}\,({\it{flg\/}}, {\rm{subst}}\,({\it{flg\/}}, {\it{s\/}}, {\it{x\/}})\index{subst})\index{all-vars})\index{disjoint}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-vars-variable-listp \\ \index{all-vars-variable-listp}
{\rm{variable-listp}}\,({\it{x\/}})\index{variable-listp} $\rightarrow$ ({\rm{all-vars}}\,({\bf{f}}, {\it{x\/}})\index{all-vars} $=$ {\it{x\/}})
\end{tabbing}

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

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

\begin{tabbing}{\sc Theorem}:  apply-to-subst-append \\ \index{apply-to-subst-append}
\=\+{\rm{apply-to-subst}}\,({\it{sg\/}}, {\rm{append}}\,({\it{s1\/}}, {\it{s2\/}}))\index{apply-to-subst} \\ 
$=$$\;\;\;\;${\rm{append}}\,({\rm{apply-to-subst}}\,({\it{sg\/}}, {\it{s1\/}})\index{apply-to-subst}, {\rm{apply-to-subst}}\,({\it{sg\/}}, {\it{s2\/}})\index{apply-to-subst})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subst-apply-to-subst \\ \index{subst-apply-to-subst}
\=\+({\it{flg\/}} $\wedge$ ({\it{g\/}} $\in$ {\rm{domain}}\,({\it{s\/}})\index{domain})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{subst}}\,({\it{flg\/}}, {\rm{apply-to-subst}}\,({\it{sg\/}}, {\it{s\/}})\index{apply-to-subst}, {\it{g\/}})\index{subst} $=$ {\rm{subst}}\,({\it{flg\/}}, {\it{sg\/}}, {\rm{value}}\,({\it{g\/}}, {\it{s\/}})\index{value})\index{subst})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subst-append-not-occur-1 \\ \index{subst-append-not-occur-1}
\=\+(\=\+{\rm{termp}}\,({\it{flg\/}}, {\it{x\/}})\index{termp} \\ 
$\wedge$$\;\;\;\;${\rm{variable-listp}}\,({\rm{domain}}\,({\it{s1\/}})\index{domain})\index{variable-listp} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{all-vars}}\,({\bf{f}}, {\rm{domain}}\,({\it{s1\/}})\index{domain})\index{all-vars}, {\rm{all-vars}}\,({\it{flg\/}}, {\it{x\/}})\index{all-vars})\index{disjoint})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{subst}}\,({\it{flg\/}}, {\rm{append}}\,({\it{s1\/}}, {\it{s2\/}}), {\it{x\/}})\index{subst} $=$ {\rm{subst}}\,({\it{flg\/}}, {\it{s2\/}}, {\it{x\/}})\index{subst})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subst-append-not-occur-2 \\ \index{subst-append-not-occur-2}
\=\+(\=\+{\rm{termp}}\,({\it{flg\/}}, {\it{x\/}})\index{termp} \\ 
$\wedge$$\;\;\;\;${\rm{variable-listp}}\,({\rm{domain}}\,({\it{s2\/}})\index{domain})\index{variable-listp} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{all-vars}}\,({\bf{f}}, {\rm{domain}}\,({\it{s2\/}})\index{domain})\index{all-vars}, {\rm{all-vars}}\,({\it{flg\/}}, {\it{x\/}})\index{all-vars})\index{disjoint})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{subst}}\,({\it{flg\/}}, {\rm{append}}\,({\it{s1\/}}, {\it{s2\/}}), {\it{x\/}})\index{subst} $=$ {\rm{subst}}\,({\it{flg\/}}, {\it{s1\/}}, {\it{x\/}})\index{subst})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  apply-to-subst-is-no-op-for-disjoint-domain \\ \index{apply-to-subst-is-no-op-for-dis!joint-domain}
\=\+(\=\+{\rm{variable-listp}}\,({\rm{domain}}\,({\it{s1\/}})\index{domain})\index{variable-listp} \\ 
$\wedge$$\;\;\;\;${\rm{alistp}}\,({\it{s2\/}})\index{alistp} \\ 
$\wedge$$\;\;\;\;${\rm{termp}}\,({\bf{f}}, {\rm{range}}\,({\it{s2\/}})\index{range})\index{termp} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{domain}}\,({\it{s1\/}})\index{domain}, {\rm{all-vars}}\,({\bf{f}}, {\rm{range}}\,({\it{s2\/}})\index{range})\index{all-vars})\index{disjoint})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{apply-to-subst}}\,({\it{s1\/}}, {\it{s2\/}})\index{apply-to-subst} $=$ {\it{s2\/}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member-subst \\ \index{member-subst}
({\it{flg\/}} $\wedge$ ({\it{a\/}} $\in$ {\it{x\/}})) $\rightarrow$ ({\rm{subst}}\,({\it{flg\/}}, {\it{s\/}}, {\it{a\/}})\index{subst} $\in$ {\rm{subst}}\,({\bf{f}}, {\it{s\/}}, {\it{x\/}})\index{subst})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subsetp-subst \\ \index{subsetp-subst}
{\rm{subsetp}}\,({\it{x\/}}, {\it{y\/}})\index{subsetp} $\rightarrow$ {\rm{subsetp}}\,({\rm{subst}}\,({\bf{f}}, {\it{s\/}}, {\it{x\/}})\index{subst}, {\rm{subst}}\,({\bf{f}}, {\it{s\/}}, {\it{y\/}})\index{subst})\index{subsetp}
\end{tabbing}

\begin{verbatim};;; (disable instance) -- not included in this version
;;;(disable compose) -- COMPOSE is left enabled for use with COMPOSE-PROPERTY-REVERSED
\end{verbatim}
\noindent{\sc Event}:   Disable apply-to-subst.

\addvspace{18pt}

\noindent{\sc Event}:   Disable subst.

\addvspace{18pt}

\noindent{\sc Event}:   Disable rembind.

\addvspace{18pt}

\noindent{\sc Event}:   Disable bind.

\addvspace{18pt}

\begin{verbatim};;;;; nullify-subst:  a substitution that has a range containing
;;                    no variables

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{nullify-subst} \\  
\=\+{\rm{nullify-subst}}\,({\it{s\/}})\index{nullify-subst} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{s\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{listp}}\,({\rm{car}}\,({\it{s\/}})) \\ 
{\bf then }{\rm{cons}}\,({\rm{cons}}\,({\rm{caar}}\,({\it{s\/}}), {\rm{list}}\,({\sc{fn}}\index{fn})), {\rm{nullify-subst}}\,({\rm{cdr}}\,({\it{s\/}}))\index{nullify-subst}) \\ 
{\bf else }{\rm{nullify-subst}}\,({\rm{cdr}}\,({\it{s\/}}))\index{nullify-subst}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  properp-nullify-subst \\ \index{properp-nullify-subst}
{\rm{properp}}\,({\rm{nullify-subst}}\,({\it{s\/}})\index{nullify-subst})\index{properp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-vars-f-range-nullify-subst \\ \index{all-vars-f-range-nullify-subst}
{\rm{all-vars}}\,({\bf{f}}, {\rm{range}}\,({\rm{nullify-subst}}\,({\it{s\/}})\index{nullify-subst})\index{range})\index{all-vars} $=$ {\bf{nil}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  termp-range-nullify-subst \\ \index{termp-range-nullify-subst}
{\rm{termp}}\,({\bf{f}}, {\rm{range}}\,({\rm{nullify-subst}}\,({\it{s\/}})\index{nullify-subst})\index{range})\index{termp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  domain-nullify-subst \\ \index{domain-nullify-subst}
{\rm{domain}}\,({\rm{nullify-subst}}\,({\it{s\/}})\index{nullify-subst})\index{domain} $=$ {\rm{domain}}\,({\it{s\/}})\index{domain}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mapping-nullify-subst \\ \index{mapping-nullify-subst}
{\rm{alistp}}\,({\it{s\/}})\index{alistp} $\rightarrow$ ({\rm{mapping}}\,({\rm{nullify-subst}}\,({\it{s\/}})\index{nullify-subst})\index{mapping} $=$ {\rm{mapping}}\,({\it{s\/}})\index{mapping})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  disjoint-all-vars-subst-nullify-subst \\ \index{disjoint-all-vars-subst-nullify!-subst}
\=\+{\rm{termp}}\,({\it{flg\/}}, {\it{term\/}})\index{termp} \\ 
$\rightarrow$$\;\;\;\;${\rm{disjoint}}\,({\rm{domain}}\,({\it{sg\/}})\index{domain}, {\rm{all-vars}}\,({\it{flg\/}}, {\rm{subst}}\,({\it{flg\/}}, {\rm{nullify-subst}}\,({\it{sg\/}})\index{nullify-subst}, {\it{term\/}})\index{subst})\index{all-vars})\index{disjoint}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  disjoint-all-vars-range-apply-subst-nullify-subst \\ \index{disjoint-all-vars-range-apply-s!ubst-nullify-subst}
\=\+{\rm{termp}}\,({\bf{f}}, {\rm{range}}\,({\it{s\/}})\index{range})\index{termp} \\ 
$\rightarrow$$\;\;\;\;${\rm{disjoint}}\,(\=\+{\rm{domain}}\,({\it{sg\/}})\index{domain}, \\ 
{\rm{all-vars}}\,({\bf{f}}, {\rm{range}}\,({\rm{apply-to-subst}}\,({\rm{nullify-subst}}\,({\it{sg\/}})\index{nullify-subst}, {\it{s\/}})\index{apply-to-subst})\index{range})\index{all-vars})\-\index{disjoint}\-
\end{tabbing}


\noindent{\sc Event}:   Disable nullify-subst.

\addvspace{18pt}


\noindent{\sc Event}:   Let us define the theory {\it{substitution-defns}} to consist of the following events: var-substp,
compose,
apply-to-subst,
subst,
nullify-subst.\index{substitution-defns}

\addvspace{18pt}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; generalize.events file
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Requires sets, alists, and terms, which currently contain a number
;; of rules that aren't really needed here, even indirectly.

;; This is a proof soundness of a slight abstraction of the GENERALIZE
;; command of PC-NQTHM.

#| Here's what I want to prove.

(implies (and (generalize-okp sg state)
              (valid-state (generalize sg state)))
         (valid-state state))

I also prove the much simpler fact, GENERALIZE-STATEP:

(implies (generalize-okp sg state)
         (statep (generalize sg state)))

|#

;; << 1 >>
\end{verbatim}\begin{tabbing}{\sc Conservative Axiom}:  theorem-intro \\ \index{theorem-intro}
\=\+(({\rm{theorem}}\,({\it{x\/}})\index{theorem} $\wedge$ {\it{flg\/}}) $\rightarrow$ {\rm{termp}}\,({\it{flg\/}}, {\it{x\/}})\index{termp}) \\ 
$\wedge$$\;\;\;\;$(({\rm{theorem}}\,({\it{x\/}})\index{theorem} $\wedge$ {\it{flg\/}} $\wedge$ {\rm{var-substp}}\,({\it{s\/}})\index{var-substp}) $\rightarrow$ {\rm{theorem}}\,({\rm{subst}}\,({\it{flg\/}}, {\it{s\/}}, {\it{x\/}})\index{subst})\index{theorem})\-
\end{tabbing}\noindent Simultaneously, we introduce the new function symbol {\it theorem\/}.

\begin{verbatim};; << 2 >>
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{theorem-list} \\  
\=\+{\rm{theorem-list}}\,({\it{x\/}})\index{theorem-list} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}})$\;\;${\bf then }{\rm{theorem}}\,({\rm{car}}\,({\it{x\/}}))\index{theorem} $\wedge$ {\rm{theorem-list}}\,({\rm{cdr}}\,({\it{x\/}}))\index{theorem-list} \\ 
{\bf else }{\it{x\/}} $=$ {\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};; << 3 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  theorem-list-properties \\ \index{theorem-list-properties}
\=\+({\rm{theorem-list}}\,({\it{x\/}})\index{theorem-list} $\rightarrow$ {\rm{termp}}\,({\bf{f}}, {\it{x\/}})\index{termp}) \\ 
$\wedge$$\;\;\;\;$(({\rm{theorem-list}}\,({\it{x\/}})\index{theorem-list} $\wedge$ {\rm{var-substp}}\,({\it{s\/}})\index{var-substp}) $\rightarrow$ {\rm{theorem-list}}\,({\rm{subst}}\,({\bf{f}}, {\it{s\/}}, {\it{x\/}})\index{subst})\index{theorem-list})\-
\end{tabbing}

\begin{verbatim};; << 4 >>
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{statep} \\  
\=\+{\rm{statep}}\,({\it{state\/}})\index{statep} \\ 
$=$$\;\;\;\;$({\rm{listp}}\,({\it{state\/}}) $\wedge$ {\rm{termp}}\,({\bf{f}}, {\rm{car}}\,({\it{state\/}}))\index{termp} $\wedge$ {\rm{variable-listp}}\,({\rm{cdr}}\,({\it{state\/}}))\index{variable-listp})\-
\end{tabbing}

\begin{verbatim};; << 5 >>
#|
(DEFN-SK VALID-STATE
         (STATE)
         (AND (STATEP STATE)
              (EXISTS WITNESSING-INSTANTIATION
                      (AND (VAR-SUBSTP WITNESSING-INSTANTIATION)
                           (SUBSETP (DOMAIN WITNESSING-INSTANTIATION)
                                    (CDR STATE))
                           (THEOREM-LIST (SUBST F WITNESSING-INSTANTIATION
                                                (CAR STATE)))))))


Adding the Skolem axiom:
      (AND
       (IMPLIES (AND (STATEP STATE)
                     (VAR-SUBSTP WITNESSING-INSTANTIATION)
                     (SUBSETP (DOMAIN WITNESSING-INSTANTIATION)
                              (CDR STATE))
                     (THEOREM-LIST (SUBST F WITNESSING-INSTANTIATION
                                          (CAR STATE))))
                (VALID-STATE STATE))
       (IMPLIES (NOT (AND (STATEP STATE)
                          (VAR-SUBSTP (WITNESSING-INSTANTIATION STATE))
                          (SUBSETP (DOMAIN (WITNESSING-INSTANTIATION STATE))
                                   (CDR STATE))
                          (THEOREM-LIST (SUBST F
                                               (WITNESSING-INSTANTIATION STATE)
                                               (CAR STATE)))))
                (NOT (VALID-STATE STATE)))).


     As this is a DEFN-SK we can conclude that:
      (OR (TRUEP (VALID-STATE STATE))
          (FALSEP (VALID-STATE STATE)))
is a theorem.


|#

\end{verbatim}
\noindent{\sc Event}:   Introduce the function symbol {\it witnessing-instantiation\index{witnessing-instantiation}\/} of one argument.

\addvspace{18pt}

\noindent{\sc Event}:   Introduce the function symbol {\it valid-state\index{valid-state}\/} of one argument.

\addvspace{18pt}

\begin{tabbing}{\sc Axiom}:  valid-state-intro \\ \index{valid-state-intro}
\=\+(\=\+(\=\+{\rm{statep}}\,({\it{state\/}})\index{statep} \\ 
$\wedge$$\;\;\;\;${\rm{var-substp}}\,({\it{witnessing-instantiation\/}})\index{var-substp} \\ 
$\wedge$$\;\;\;\;${\rm{subsetp}}\,({\rm{domain}}\,({\it{witnessing-instantiation\/}})\index{domain}, {\rm{cdr}}\,({\it{state\/}}))\index{subsetp} \\ 
$\wedge$$\;\;\;\;${\rm{theorem-list}}\,({\rm{subst}}\,({\bf{f}}, {\it{witnessing-instantiation\/}}, {\rm{car}}\,({\it{state\/}}))\index{subst})\index{theorem-list})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{valid-state}}\,({\it{state\/}})\index{valid-state})\- \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ (\=\+{\rm{statep}}\,({\it{state\/}})\index{statep} \\ 
$\wedge$$\;\;\;\;${\rm{var-substp}}\,({\rm{witnessing-instantiation}}\,({\it{state\/}})\index{witnessing-instantiation})\index{var-substp} \\ 
$\wedge$$\;\;\;\;${\rm{subsetp}}\,(\=\+{\rm{domain}}\,({\rm{witnessing-instantiation}}\,({\it{state\/}})\index{witnessing-instantiation})\index{domain}, \\ 
{\rm{cdr}}\,({\it{state\/}}))\-\index{subsetp} \\ 
$\wedge$$\;\;\;\;${\rm{theorem-list}}\,({\rm{subst}}\,(\=\+{\bf{f}}, \\ 
{\rm{witnessing-instantiation}}\,({\it{state\/}})\index{witnessing-instantiation}, \\ 
{\rm{car}}\,({\it{state\/}}))\-\index{subst})\index{theorem-list})\-) \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{valid-state}}\,({\it{state\/}})\index{valid-state}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Axiom}:  valid-state-type \\ \index{valid-state-type}
{\rm{truep}}\,({\rm{valid-state}}\,({\it{state\/}})\index{valid-state}) $\vee$ {\rm{falsep}}\,({\rm{valid-state}}\,({\it{state\/}})\index{valid-state})
\end{tabbing}

\begin{verbatim};; << 6 >>
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{new-gen-vars} \\  
\=\+{\rm{new-gen-vars}}\,({\it{goals\/}}, {\it{free\/}}, {\it{vars\/}})\index{new-gen-vars} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{goals\/}}) \\ 
{\bf then }\=\+{\bf let }\=\+{\it{current-free-vars\/}}{\bf $\;$ be$\;\;$}{\rm{intersection}}\,(\=\+{\it{free\/}}, \\ 
{\rm{all-vars}}\,({\bf{t}}, {\rm{car}}\,({\it{goals\/}}))\index{all-vars})\-\index{intersection}\- \\ 
{\bf in} \\ 
\=\+{\bf if }{\rm{disjoint}}\,({\it{current-free-vars\/}}, {\it{vars\/}})\index{disjoint} \\ 
{\bf then }{\rm{new-gen-vars}}\,({\rm{cdr}}\,({\it{goals\/}}), {\it{free\/}}, {\it{vars\/}})\index{new-gen-vars} \\ 
{\bf else }{\rm{append}}\,(\=\+{\it{current-free-vars\/}}, \\ 
{\rm{new-gen-vars}}\,({\rm{cdr}}\,({\it{goals\/}}), {\it{free\/}}, {\it{vars\/}})\index{new-gen-vars})\-$\;${\bf  endif}\-$\;${\bf  endlet}\- \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};; << 7 >>
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{cardinality}$\;\;$
{\rm{cardinality}}\,({\it{x\/}})\index{cardinality} $=$ {\rm{length}}\,({\rm{make-set}}\,({\it{x\/}})\index{make-set})\index{length}
\end{tabbing}

\begin{verbatim};; Next goal:  get the definition of GEN-CLOSURE accepted.  In fact,
;; the lemma GEN-CLOSURE-ACCEPT below suffices, taking NEW to be
;; (NEW-GEN-VARS GOALS FREE FREE-VARS-SO-FAR), as long as we prove the
;; following lemma, NEW-GEN-VARS-SUBSET.

;; << 8 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  new-gen-vars-subset \\ \index{new-gen-vars-subset}
{\rm{subsetp}}\,({\rm{new-gen-vars}}\,({\it{goals\/}}, {\it{free\/}}, {\it{vars\/}})\index{new-gen-vars}, {\it{free\/}})\index{subsetp}
\end{tabbing}

\begin{verbatim};; It is interesting to note that the exact form of the following
;; lemma changed while polishing the proof, since rewrite rules
;; applied to the old version so as to make it irrelevant.

;; << 9 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  gen-closure-accept \\ \index{gen-closure-accept}
\=\+(($\neg$ {\rm{subsetp}}\,({\it{new\/}}, {\it{free-vars-so-far\/}})\index{subsetp}) $\wedge$ {\rm{subsetp}}\,({\it{new\/}}, {\it{free\/}})\index{subsetp}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+(\=\+{\rm{length}}\,({\rm{make-set}}\,({\it{free\/}})\index{make-set})\index{length} \\ 
$-$$\;\;\;\;${\rm{length}}\,({\rm{intersection}}\,({\rm{make-set}}\,({\it{free\/}})\index{make-set}, {\it{free-vars-so-far\/}})\index{intersection})\index{length})\- \\ 
$-$$\;\;\;\;${\rm{length}}\,({\rm{intersection}}\,(\=\+{\rm{set-diff}}\,({\rm{make-set}}\,({\it{free\/}})\index{make-set}, {\it{free-vars-so-far\/}})\index{set-diff}, \\ 
{\it{new\/}})\-\index{intersection})\index{length})\- \\ 
$<$$\;\;\;\;$(\=\+{\rm{length}}\,({\rm{make-set}}\,({\it{free\/}})\index{make-set})\index{length} \\ 
$-$$\;\;\;\;${\rm{length}}\,({\rm{intersection}}\,({\rm{make-set}}\,({\it{free\/}})\index{make-set}, {\it{free-vars-so-far\/}})\index{intersection})\index{length})\-)\-\-
\end{tabbing}

\begin{verbatim};; Here I have a choice:  I could intersect the accumulator with free
;; at the end, or I could assume that it's intersected with free
;; before it's input.  I'll choose the former approach, so that I'll
;; have a simpler rewrite rule and so that I can call gen-closure more
;; simply.  I may wish to commute the arguments to intersection in the
;; exit below, but probably that won't matter because I'll only be
;; talking about membership.

;; << 10 >>
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{gen-closure} \\  
\=\+{\rm{gen-closure}}\,({\it{goals\/}}, {\it{free\/}}, {\it{free-vars-so-far\/}})\index{gen-closure} \\ 
$=$$\;\;\;\;$\=\+{\bf let }\=\+{\it{new-free-vars\/}}{\bf $\;$ be$\;\;$}{\rm{new-gen-vars}}\,({\it{goals\/}}, {\it{free\/}}, {\it{free-vars-so-far\/}})\index{new-gen-vars}\- \\ 
{\bf in} \\ 
\=\+{\bf if }{\rm{subsetp}}\,({\it{new-free-vars\/}}, {\it{free-vars-so-far\/}})\index{subsetp} \\ 
{\bf then }{\rm{intersection}}\,({\it{free-vars-so-far\/}}, {\it{free\/}})\index{intersection} \\ 
{\bf else }{\rm{gen-closure}}\,(\=\+{\it{goals\/}}, \\ 
{\it{free\/}}, \\ 
{\rm{append}}\,({\it{new-free-vars\/}}, {\it{free-vars-so-far\/}}))\-\index{gen-closure}$\;${\bf  endif}\-$\;${\bf  endlet}\-\-
\end{tabbing}

\begin{verbatim};; << 11 >>
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{generalize-okp} \\  
\=\+{\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} \\ 
$=$$\;\;\;\;$(\=\+{\rm{var-substp}}\,({\it{sg\/}})\index{var-substp} \\ 
$\wedge$$\;\;\;\;${\rm{statep}}\,({\it{state\/}})\index{statep} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{domain}}\,({\it{sg\/}})\index{domain}, {\rm{all-vars}}\,({\bf{f}}, {\rm{car}}\,({\it{state\/}}))\index{all-vars})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\rm{car}}\,({\it{state\/}})) \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{domain}}\,({\it{sg\/}})\index{domain}, {\rm{cdr}}\,({\it{state\/}}))\index{disjoint})\-\-
\end{tabbing}

\begin{verbatim};; << 12 >>
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{generalize} \\  
\=\+{\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize} \\ 
$=$$\;\;\;\;$\=\+{\bf let }\=\+{\it{g\/}}{\bf $\;$ be$\;\;$}{\rm{caar}}\,({\it{state\/}}), \\ 
{\it{p\/}}{\bf $\;$ be$\;\;$}{\rm{cdar}}\,({\it{state\/}}), \\ 
{\it{free\/}}{\bf $\;$ be$\;\;$}{\rm{cdr}}\,({\it{state\/}}), \\ 
{\it{sg-vars\/}}{\bf $\;$ be$\;\;$}{\rm{all-vars}}\,({\bf{f}}, {\rm{range}}\,({\it{sg\/}})\index{range})\index{all-vars}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{new-g\/}}{\bf $\;$ be$\;\;$}{\rm{subst}}\,({\bf{t}}, {\rm{invert}}\,({\it{sg\/}})\index{invert}, {\it{g\/}})\index{subst}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{new-free\/}}{\bf $\;$ be$\;\;$}{\rm{set-diff}}\,(\=\+{\it{free\/}}, \\ 
{\rm{intersection}}\,(\=\+{\rm{gen-closure}}\,(\=\+{\rm{cons}}\,(\=\+{\it{new-g\/}}, \\ 
{\it{p\/}})\-, \\ 
{\it{free\/}}, \\ 
{\rm{all-vars}}\,(\=\+{\bf{t}}, \\ 
{\it{new-g\/}})\-\index{all-vars})\-\index{gen-closure}, \\ 
{\rm{all-vars}}\,(\=\+{\bf{f}}, \\ 
{\rm{range}}\,({\it{sg\/}})\index{range})\-\index{all-vars})\-\index{intersection})\-\index{set-diff}\- \\ 
{\bf in} \\ 
{\rm{cons}}\,({\rm{cons}}\,({\it{new-g\/}}, {\it{p\/}}), {\it{new-free\/}})$\;${\bf  endlet}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-\-
\end{tabbing}

\begin{verbatim};; Here is a fact, not needed elsewhere, that is worth noticing, in
;; case we wish to extend the current theorem to a sequence of commands.

;; << 13 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  generalize-statep \\ \index{generalize-statep}
{\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} $\rightarrow$ {\rm{statep}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{statep}
\end{tabbing}

\begin{verbatim};; << 14 >>
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{gen-inst} \\  
\=\+{\rm{gen-inst}}\,({\it{sg\/}}, {\it{state\/}})\index{gen-inst} \\ 
$=$$\;\;\;\;$\=\+{\bf let }\=\+{\it{s\/}}{\bf $\;$ be$\;\;$}{\rm{witnessing-instantiation}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{witnessing-instantiation}, \\ 
{\it{domain-1\/}}{\bf $\;$ be$\;\;$}{\rm{gen-closure}}\,(\=\+{\rm{cons}}\,(\=\+{\rm{subst}}\,({\bf{t}}, {\rm{invert}}\,({\it{sg\/}})\index{invert}, {\rm{caar}}\,({\it{state\/}}))\index{subst}, \\ 
{\rm{cdar}}\,({\it{state\/}}))\-, \\ 
{\rm{cdr}}\,({\it{state\/}}), \\ 
{\rm{all-vars}}\,(\=\+{\bf{t}}, \\ 
{\rm{subst}}\,(\=\+{\bf{t}}, \\ 
{\rm{invert}}\,({\it{sg\/}})\index{invert}, \\ 
{\rm{caar}}\,({\it{state\/}}))\-\index{subst})\-\index{all-vars})\-\index{gen-closure}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{s1\/}}{\bf $\;$ be$\;\;$}{\rm{restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{restrict}, \\ 
{\it{s2\/}}{\bf $\;$ be$\;\;$}{\rm{apply-to-subst}}\,(\=\+{\rm{nullify-subst}}\,({\it{sg\/}})\index{nullify-subst}, \\ 
{\rm{co-restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{co-restrict})\-\index{apply-to-subst}\- \\ 
{\bf in} \\ 
{\rm{apply-to-subst}}\,({\rm{apply-to-subst}}\,({\it{s2\/}}, {\it{sg\/}})\index{apply-to-subst}, {\rm{append}}\,({\it{s1\/}}, {\it{s2\/}}))\index{apply-to-subst}$\;${\bf  endlet}\-$\;${\bf  endlet}\-\-
\end{tabbing}

\begin{verbatim};; Let's see that it suffices to prove the result of opening up the
;; conclusion of the main theorem with a particular witness.

#|

(add-axiom main-theorem-1 (rewrite)
  (let ((wit (gen-inst sg state)))
    (implies (and (generalize-okp sg state)
                  (valid-state (generalize sg state)))
             (and (statep state)
                  (var-substp wit)
                  (subsetp (domain wit) (cdr state))
                  (theorem-list (subst f wit (car state)))))))

(prove-lemma generalize-is-correct (rewrite)
  (implies (and (generalize-okp sg state)
                (valid-state (generalize sg state)))
           (valid-state state))
  ((disable-theory t)
   (enable-theory ground-zero)
   (enable main-theorem-1)
   (use (valid-state-intro
         (witnessing-instantiation (gen-inst sg state))))))

|#

;; So, it suffices to prove main-theorem-1.  The first three conjuncts
;; of the conclusion are quite trivial.

;; << 15 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-theorem-1-case-1 \\ \index{main-theorem-1-case-1}
{\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} $\rightarrow$ {\rm{statep}}\,({\it{state\/}})\index{statep}
\end{tabbing}

\begin{verbatim};; We put one direction of the definition of valid-state here, for
;; efficiency in proofs.

;; << 16 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  valid-state-opener \\ \index{valid-state-opener}
\=\+{\rm{valid-state}}\,({\it{state\/}})\index{valid-state} \\ 
$=$$\;\;\;\;$(\=\+{\rm{statep}}\,({\it{state\/}})\index{statep} \\ 
$\wedge$$\;\;\;\;$\=\+{\bf let }\=\+{\it{witnessing-instantiation\/}}{\bf $\;$ be$\;\;$}{\rm{witnessing-instantiation}}\,({\it{state\/}})\index{witnessing-instantiation}\- \\ 
{\bf in} \\ 
\=\+{\rm{var-substp}}\,({\it{witnessing-instantiation\/}})\index{var-substp} \\ 
$\wedge$$\;\;\;\;${\rm{subsetp}}\,(\=\+{\rm{domain}}\,({\it{witnessing-instantiation\/}})\index{domain}, \\ 
{\rm{cdr}}\,({\it{state\/}}))\-\index{subsetp} \\ 
$\wedge$$\;\;\;\;${\rm{theorem-list}}\,({\rm{subst}}\,(\=\+{\bf{f}}, \\ 
{\it{witnessing-instantiation\/}}, \\ 
{\rm{car}}\,({\it{state\/}}))\-\index{subst})\index{theorem-list}\-$\;${\bf  endlet}\-)\-\-
\end{tabbing}

\begin{verbatim};; << 17 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-theorem-1-case-2 \\ \index{main-theorem-1-case-2}
\=\+{\bf let }\=\+{\it{wit\/}}{\bf $\;$ be$\;\;$}{\rm{gen-inst}}\,({\it{sg\/}}, {\it{state\/}})\index{gen-inst}\- \\ 
{\bf in} \\ 
\=\+({\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} $\wedge$ {\rm{valid-state}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{valid-state}) \\ 
$\rightarrow$$\;\;\;\;${\rm{var-substp}}\,({\it{wit\/}})\index{var-substp}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim};; << 18 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  subsetp-cdr-generalize \\ \index{subsetp-cdr-generalize}
{\rm{subsetp}}\,({\rm{cdr}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize}), {\rm{cdr}}\,({\it{state\/}}))\index{subsetp}
\end{tabbing}

\begin{verbatim};; At this point I had to prove SUBSETP-SET-DIFF-SUFFICIENCY because
;; of some lemma that was created during the polishing process
;; (perhaps DOMAIN-RESTRICT).

;; << 19 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-theorem-1-case-3 \\ \index{main-theorem-1-case-3}
\=\+{\bf let }\=\+{\it{wit\/}}{\bf $\;$ be$\;\;$}{\rm{gen-inst}}\,({\it{sg\/}}, {\it{state\/}})\index{gen-inst}\- \\ 
{\bf in} \\ 
\=\+{\rm{valid-state}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{valid-state} \\ 
$\rightarrow$$\;\;\;\;${\rm{subsetp}}\,({\rm{domain}}\,({\it{wit\/}})\index{domain}, {\rm{cdr}}\,({\it{state\/}}))\index{subsetp}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim};; So now we only have to prove MAIN-THEOREM-1-CASE-4 (written here
;; without use of LET):

#|

(add-axiom main-theorem-1-case-4 (rewrite)
  (implies (and (generalize-okp sg state)
                (valid-state (generalize sg state)))
           (theorem-list (subst f (gen-inst sg state) (car state)))))

(prove-lemma main-theorem-1 (rewrite)
  (let ((wit (gen-inst sg state)))
    (implies (and (generalize-okp sg state)
                  (valid-state (generalize sg state)))
             (and (statep state)
                  (var-substp wit)
                  (subsetp (domain wit) (cdr state))
                  (theorem-list (subst f wit (car state))))))
  ((disable-theory t)
   (enable-theory ground-zero)
   (enable main-theorem-1-case-1 main-theorem-1-case-2
           main-theorem-1-case-3 main-theorem-1-case-4)))

|#

;; << 20 >>
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{gen-setting-substitutions} \\  
\=\+{\rm{gen-setting-substitutions}}\,({\it{s1\/}}, {\it{s2\/}}, {\it{sg\/}})\index{gen-setting-substitutions} \\ 
$=$$\;\;\;\;$(\=\+{\rm{var-substp}}\,({\it{s1\/}})\index{var-substp} \\ 
$\wedge$$\;\;\;\;${\rm{var-substp}}\,({\it{s2\/}})\index{var-substp} \\ 
$\wedge$$\;\;\;\;${\rm{var-substp}}\,({\it{sg\/}})\index{var-substp} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{domain}}\,({\it{s1\/}})\index{domain}, {\rm{domain}}\,({\it{s2\/}})\index{domain})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{domain}}\,({\it{s1\/}})\index{domain}, {\rm{domain}}\,({\it{sg\/}})\index{domain})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{domain}}\,({\it{s2\/}})\index{domain}, {\rm{domain}}\,({\it{sg\/}})\index{domain})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{all-vars}}\,({\bf{f}}, {\rm{range}}\,({\it{sg\/}})\index{range})\index{all-vars}, {\rm{domain}}\,({\it{s1\/}})\index{domain})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{all-vars}}\,({\bf{f}}, {\rm{range}}\,({\it{s2\/}})\index{range})\index{all-vars}, {\rm{domain}}\,({\it{sg\/}})\index{domain})\index{disjoint})\-\-
\end{tabbing}

\begin{verbatim};; << 21 >>
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{main-hyps} \\  
\=\+{\rm{main-hyps}}\,({\it{s1\/}}, {\it{s2\/}}, {\it{sg\/}}, {\it{g\/}}, {\it{p\/}})\index{main-hyps} \\ 
$=$$\;\;\;\;$(\=\+{\rm{termp}}\,({\bf{t}}, {\it{g\/}})\index{termp} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{all-vars}}\,({\bf{t}}, {\it{g\/}})\index{all-vars}, {\rm{domain}}\,({\it{sg\/}})\index{domain})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{termp}}\,({\bf{f}}, {\it{p\/}})\index{termp} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{all-vars}}\,({\bf{f}}, {\it{p\/}})\index{all-vars}, {\rm{domain}}\,({\it{sg\/}})\index{domain})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{gen-setting-substitutions}}\,({\it{s1\/}}, {\it{s2\/}}, {\it{sg\/}})\index{gen-setting-substitutions} \\ 
$\wedge$$\;\;\;\;${\rm{theorem-list}}\,({\rm{subst}}\,(\=\+{\bf{f}}, \\ 
{\rm{append}}\,({\it{s1\/}}, {\it{s2\/}}), \\ 
{\rm{cons}}\,({\rm{subst}}\,({\bf{t}}, {\rm{invert}}\,({\it{sg\/}})\index{invert}, {\it{g\/}})\index{subst}, {\it{p\/}}))\-\index{subst})\index{theorem-list})\-\-
\end{tabbing}

\begin{verbatim};; The goal above, MAIN-THEOREM-1-CASE-4, should follow from the
;; following two lemmas.

#|

(add-axiom main-hyps-suffice (rewrite)
  (implies (and (listp goals)
                (main-hyps s1 s2 sg (car goals) (cdr goals)))
           (theorem-list (subst f
                                (apply-to-subst (apply-to-subst s2 sg)
                                                (append s1 s2))
                                goals))))

(add-axiom main-hyps-relieved (rewrite)
  (let ((g (caar state))
        (p (cdar state))
        (free (cdr state))
        (s (witnessing-instantiation (generalize sg state))))
    (let ((new-g (subst t (invert sg) g)))
      (let ((domain-1
             (gen-closure (cons new-g p) free (all-vars t new-g))))
        (let ((s1 (restrict s domain-1))
              (s2 (apply-to-subst (nullify-subst sg)
                                  (co-restrict s domain-1))))
          (implies (and (generalize-okp sg state)
                        (valid-state (generalize sg state)))
                   (main-hyps s1 s2 sg g p)))))))

(prove-lemma main-theorem-1-case-4 (rewrite)
  (implies (and (generalize-okp sg state)
                (valid-state (generalize sg state)))
           (theorem-list (subst f (gen-inst sg state) (car state))))
  ((disable-theory t)
   (enable-theory ground-zero)
   (enable gen-inst main-hyps-suffice generalize-okp main-hyps-relieved)))

|#

;; So, now let us start with MAIN-HYPS-SUFFICE.  It should follow from
;; two subgoals, as shown:

#|

(add-axiom main-hyps-suffice-first (rewrite)
  (implies (main-hyps s1 s2 sg g p)
           (theorem (subst t
                           (apply-to-subst (apply-to-subst s2 sg)
                                           (append s1 s2))
                           g))))

(add-axiom main-hyps-suffice-rest (rewrite)
  (implies (main-hyps s1 s2 sg g p)
           (theorem-list (subst f
                                (apply-to-subst (apply-to-subst s2 sg)
                                                (append s1 s2))
                                p))))

(prove-lemma main-hyps-suffice (rewrite)
  (implies (and (listp goals)
                (main-hyps s1 s2 sg (car goals) (cdr goals)))
           (theorem-list (subst f
                                (apply-to-subst (apply-to-subst s2 sg)
                                                (append s1 s2))
                                goals)))
  ((disable-theory t)
   (enable-theory ground-zero)
   (enable theorem-list subst main-hyps-suffice-first main-hyps-suffice-rest)))

|#

;; Consider the first of these.  Although COMPOSE-PROPERTY-REVERSED is
;; used in the proof (because it's enabled), it's actually not
;; necessary.  A proof took slightly over 10 minutes with the rule
;; enabled, and roughly 9 minutes without.

;; << 22 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-suffice-first-lemma-general \\ \index{main-hyps-suffice-first-lemma-ge!neral}
\=\+(\=\+{\rm{termp}}\,({\it{flg\/}}, {\it{g\/}})\index{termp} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{all-vars}}\,({\it{flg\/}}, {\it{g\/}})\index{all-vars}, {\rm{domain}}\,({\it{sg\/}})\index{domain})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{gen-setting-substitutions}}\,({\it{s1\/}}, {\it{s2\/}}, {\it{sg\/}})\index{gen-setting-substitutions} \\ 
$\wedge$$\;\;\;\;$({\it{sg-1\/}} $=$ {\rm{invert}}\,({\it{sg\/}})\index{invert}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{subst}}\,({\it{flg\/}}, {\rm{apply-to-subst}}\,({\rm{apply-to-subst}}\,({\it{s2\/}}, {\it{sg\/}})\index{apply-to-subst}, {\rm{append}}\,({\it{s1\/}}, {\it{s2\/}}))\index{apply-to-subst}, {\it{g\/}})\index{subst} \\ 
$=$$\;\;\;\;${\rm{subst}}\,(\=\+{\it{flg\/}}, \\ 
{\rm{apply-to-subst}}\,({\it{s2\/}}, {\it{sg\/}})\index{apply-to-subst}, \\ 
{\rm{subst}}\,({\it{flg\/}}, {\rm{append}}\,({\it{s1\/}}, {\it{s2\/}}), {\rm{subst}}\,({\it{flg\/}}, {\it{sg-1\/}}, {\it{g\/}})\index{subst})\index{subst})\-\index{subst})\-\-
\end{tabbing}

\begin{verbatim};; << 23 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-suffice-first-lemma \\ \index{main-hyps-suffice-first-lemma}
\=\+(\=\+{\rm{termp}}\,({\bf{t}}, {\it{g\/}})\index{termp} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{all-vars}}\,({\bf{t}}, {\it{g\/}})\index{all-vars}, {\rm{domain}}\,({\it{sg\/}})\index{domain})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{gen-setting-substitutions}}\,({\it{s1\/}}, {\it{s2\/}}, {\it{sg\/}})\index{gen-setting-substitutions})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{subst}}\,({\bf{t}}, {\rm{apply-to-subst}}\,({\rm{apply-to-subst}}\,({\it{s2\/}}, {\it{sg\/}})\index{apply-to-subst}, {\rm{append}}\,({\it{s1\/}}, {\it{s2\/}}))\index{apply-to-subst}, {\it{g\/}})\index{subst} \\ 
$=$$\;\;\;\;${\rm{subst}}\,(\=\+{\bf{t}}, \\ 
{\rm{apply-to-subst}}\,({\it{s2\/}}, {\it{sg\/}})\index{apply-to-subst}, \\ 
{\rm{subst}}\,({\bf{t}}, {\rm{append}}\,({\it{s1\/}}, {\it{s2\/}}), {\rm{subst}}\,({\bf{t}}, {\rm{invert}}\,({\it{sg\/}})\index{invert}, {\it{g\/}})\index{subst})\index{subst})\-\index{subst})\-\-
\end{tabbing}

\begin{verbatim};; << 24 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-suffice-first \\ \index{main-hyps-suffice-first}
\=\+{\rm{main-hyps}}\,({\it{s1\/}}, {\it{s2\/}}, {\it{sg\/}}, {\it{g\/}}, {\it{p\/}})\index{main-hyps} \\ 
$\rightarrow$$\;\;\;\;${\rm{theorem}}\,({\rm{subst}}\,({\bf{t}}, {\rm{apply-to-subst}}\,({\rm{apply-to-subst}}\,({\it{s2\/}}, {\it{sg\/}})\index{apply-to-subst}, {\rm{append}}\,({\it{s1\/}}, {\it{s2\/}}))\index{apply-to-subst}, {\it{g\/}})\index{subst})\index{theorem}\-
\end{tabbing}

\begin{verbatim};; The following is useful with s = (append s1 s2).

;; << 25 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-suffice-rest-lemma \\ \index{main-hyps-suffice-rest-lemma}
\=\+(\=\+{\rm{termp}}\,({\it{flg\/}}, {\it{p\/}})\index{termp} \\ 
$\wedge$$\;\;\;\;${\rm{variable-listp}}\,({\rm{domain}}\,({\it{sg\/}})\index{domain})\index{variable-listp} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{all-vars}}\,({\it{flg\/}}, {\it{p\/}})\index{all-vars}, {\rm{domain}}\,({\it{sg\/}})\index{domain})\index{disjoint})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{subst}}\,({\it{flg\/}}, {\rm{apply-to-subst}}\,({\rm{apply-to-subst}}\,({\it{s2\/}}, {\it{sg\/}})\index{apply-to-subst}, {\it{s\/}})\index{apply-to-subst}, {\it{p\/}})\index{subst} \\ 
$=$$\;\;\;\;${\rm{subst}}\,({\it{flg\/}}, {\rm{apply-to-subst}}\,({\it{s2\/}}, {\it{sg\/}})\index{apply-to-subst}, {\rm{subst}}\,({\it{flg\/}}, {\it{s\/}}, {\it{p\/}})\index{subst})\index{subst})\-\-
\end{tabbing}

\begin{verbatim};; << 26 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-suffice-rest \\ \index{main-hyps-suffice-rest}
\=\+{\rm{main-hyps}}\,({\it{s1\/}}, {\it{s2\/}}, {\it{sg\/}}, {\it{g\/}}, {\it{p\/}})\index{main-hyps} \\ 
$\rightarrow$$\;\;\;\;${\rm{theorem-list}}\,({\rm{subst}}\,(\=\+{\bf{f}}, \\ 
{\rm{apply-to-subst}}\,({\rm{apply-to-subst}}\,({\it{s2\/}}, {\it{sg\/}})\index{apply-to-subst}, {\rm{append}}\,({\it{s1\/}}, {\it{s2\/}}))\index{apply-to-subst}, \\ 
{\it{p\/}})\-\index{subst})\index{theorem-list}\-
\end{tabbing}

\begin{verbatim};; << 27 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-suffice \\ \index{main-hyps-suffice}
\=\+({\rm{listp}}\,({\it{goals\/}}) $\wedge$ {\rm{main-hyps}}\,({\it{s1\/}}, {\it{s2\/}}, {\it{sg\/}}, {\rm{car}}\,({\it{goals\/}}), {\rm{cdr}}\,({\it{goals\/}}))\index{main-hyps}) \\ 
$\rightarrow$$\;\;\;\;${\rm{theorem-list}}\,({\rm{subst}}\,(\=\+{\bf{f}}, \\ 
{\rm{apply-to-subst}}\,({\rm{apply-to-subst}}\,({\it{s2\/}}, {\it{sg\/}})\index{apply-to-subst}, {\rm{append}}\,({\it{s1\/}}, {\it{s2\/}}))\index{apply-to-subst}, \\ 
{\it{goals\/}})\-\index{subst})\index{theorem-list}\-
\end{tabbing}

\begin{verbatim};; I'll disable the two lemmas used above so that I avoid the possibility
;; of looping with COMPOSE-PROPERTY-REVERSED.

;; << 28 >>
\end{verbatim}
\noindent{\sc Event}:   Disable main-hyps-suffice-first-lemma.

\addvspace{18pt}
\begin{verbatim};; << 29 >>
\end{verbatim}
\noindent{\sc Event}:   Disable main-hyps-suffice-rest-lemma.

\addvspace{18pt}

\begin{verbatim};; All that remains now is to prove MAIN-HYPS-RELIEVED.  If we open up
;; MAIN-HYPS we see what the necessary subgoals are.  Recall the
;; definition of MAIN-HYPS:

#| 
(defn main-hyps (s1 s2 sg g p)
  (and (termp t g)
       (disjoint (all-vars t g) (domain sg))
       (termp f p)
       (disjoint (all-vars f p) (domain sg))
       (gen-setting-substitutions s1 s2 sg)
       (theorem-list (subst f (append s1 s2)
                            (cons (subst t (invert sg) g) p)))))
|#

;; << 30 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-relieved-1 \\ \index{main-hyps-relieved-1}
\=\+{\bf let }\=\+{\it{g\/}}{\bf $\;$ be$\;\;$}{\rm{caar}}\,({\it{state\/}})\- \\ 
{\bf in} \\ 
{\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} $\rightarrow$ {\rm{termp}}\,({\bf{t}}, {\it{g\/}})\index{termp}$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim};; << 31 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-relieved-2 \\ \index{main-hyps-relieved-2}
\=\+{\bf let }\=\+{\it{g\/}}{\bf $\;$ be$\;\;$}{\rm{caar}}\,({\it{state\/}})\- \\ 
{\bf in} \\ 
{\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} $\rightarrow$ {\rm{disjoint}}\,({\rm{all-vars}}\,({\bf{t}}, {\it{g\/}})\index{all-vars}, {\rm{domain}}\,({\it{sg\/}})\index{domain})\index{disjoint}$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim};; << 32 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-relieved-3 \\ \index{main-hyps-relieved-3}
\=\+{\bf let }\=\+{\it{p\/}}{\bf $\;$ be$\;\;$}{\rm{cdar}}\,({\it{state\/}})\- \\ 
{\bf in} \\ 
{\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} $\rightarrow$ {\rm{termp}}\,({\bf{f}}, {\it{p\/}})\index{termp}$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim};; << 33 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-relieved-4 \\ \index{main-hyps-relieved-4}
\=\+{\bf let }\=\+{\it{p\/}}{\bf $\;$ be$\;\;$}{\rm{cdar}}\,({\it{state\/}})\- \\ 
{\bf in} \\ 
{\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} $\rightarrow$ {\rm{disjoint}}\,({\rm{all-vars}}\,({\bf{f}}, {\it{p\/}})\index{all-vars}, {\rm{domain}}\,({\it{sg\/}})\index{domain})\index{disjoint}$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim}#|

(add-axiom main-hyps-relieved-5 (rewrite)
  (let ((g (caar state))
        (p (cdar state))
        (free (cdr state))
        (s (witnessing-instantiation (generalize sg state))))
    (let ((new-g (subst t (invert sg) g)))
      (let ((domain-1
             (gen-closure (cons new-g p) free (all-vars t new-g))))
        (let ((s1 (restrict s domain-1))
              (s2 (apply-to-subst (nullify-subst sg)
                                  (co-restrict s domain-1))))
          (implies (and (generalize-okp sg state)
                        (valid-state (generalize sg state)))
                   (gen-setting-substitutions s1 s2 sg)))))))

(add-axiom main-hyps-relieved-6 (rewrite)
  (let ((g (caar state))
        (p (cdar state))
        (free (cdr state))
        (s (witnessing-instantiation (generalize sg state))))
    (let ((new-g (subst t (invert sg) g)))
      (let ((domain-1
             (gen-closure (cons new-g p) free (all-vars t new-g))))
        (let ((s1 (restrict s domain-1))
              (s2 (apply-to-subst (nullify-subst sg)
                                  (co-restrict s domain-1))))
          (implies (and (generalize-okp sg state)
                        (valid-state (generalize sg state)))
                   (theorem-list (subst f (append s1 s2)
                                        (cons (subst t (invert sg) g) p)))))))))

(prove-lemma main-hyps-relieved (rewrite)
  (let ((g (caar state))
        (p (cdar state))
        (free (cdr state))
        (s (witnessing-instantiation (generalize sg state))))
    (let ((new-g (subst t (invert sg) g)))
      (let ((domain-1
             (gen-closure (cons new-g p) free (all-vars t new-g))))
        (let ((s1 (restrict s domain-1))
              (s2 (apply-to-subst (nullify-subst sg)
                                  (co-restrict s domain-1))))
          (implies (and (generalize-okp sg state)
                        (valid-state (generalize sg state)))
                   (main-hyps s1 s2 sg g p))))))
  ((disable-theory t)
   (enable-theory ground-zero)
   (enable main-hyps main-hyps-relieved-1 main-hyps-relieved-2 main-hyps-relieved-3
           main-hyps-relieved-4 main-hyps-relieved-5 main-hyps-relieved-6)))

|#

;; So, we have left the goals MAIN-HYPS-RELIEVED-5 and
;; MAIN-HYPS-RELIEVED-6.  Let us start with the first.  Opening up
;; GEN-SETTING-SUBSTITUTIONS gives us a number of subgoals.

;; The first two cases below do not require knowledge about DOMAIN-1
;; (or G, P, FREE, or NEW-G), but simply following from the validity
;; of the state (GENERALIZE SG STATE).  Disabling GENERALIZE is very
;; useful (probably not necessary, though I didn't let the prover run
;; long enough to find out).

;; << 34 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-relieved-5-lemma-1 \\ \index{main-hyps-relieved-5-lemma-1}
\=\+{\bf let }\=\+{\it{s\/}}{\bf $\;$ be$\;\;$}{\rm{witnessing-instantiation}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{witnessing-instantiation}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{s1\/}}{\bf $\;$ be$\;\;$}{\rm{restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{restrict}, \\ 
{\it{s2\/}}{\bf $\;$ be$\;\;$}{\rm{apply-to-subst}}\,({\rm{nullify-subst}}\,({\it{sg\/}})\index{nullify-subst}, {\rm{co-restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{co-restrict})\index{apply-to-subst}\- \\ 
{\bf in} \\ 
\=\+{\rm{valid-state}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{valid-state} \\ 
$\rightarrow$$\;\;\;\;$({\rm{var-substp}}\,({\it{s1\/}})\index{var-substp} $\wedge$ {\rm{var-substp}}\,({\it{s2\/}})\index{var-substp})\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim};; The next case is trivial.

;; << 35 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-relieved-5-lemma-2 \\ \index{main-hyps-relieved-5-lemma-2}
{\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} $\rightarrow$ {\rm{var-substp}}\,({\it{sg\/}})\index{var-substp}
\end{tabbing}

\begin{verbatim};; The next case is also quite trivial; notice how abstracted it is.

;; << 36 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-relieved-5-lemma-3 \\ \index{main-hyps-relieved-5-lemma-3}
\=\+{\bf let }\=\+{\it{s1\/}}{\bf $\;$ be$\;\;$}{\rm{restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{restrict}, \\ 
{\it{s2\/}}{\bf $\;$ be$\;\;$}{\rm{apply-to-subst}}\,({\rm{nullify-subst}}\,({\it{sg\/}})\index{nullify-subst}, {\rm{co-restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{co-restrict})\index{apply-to-subst}\- \\ 
{\bf in} \\ 
{\rm{disjoint}}\,({\rm{domain}}\,({\it{s1\/}})\index{domain}, {\rm{domain}}\,({\it{s2\/}})\index{domain})\index{disjoint}$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim};; For the next two cases we first observe that (DOMAIN S) is disjoint
;; from (DOMAIN SG), and then we use SUBSETP-DISJOINT-1 where X is the
;; domain of S1 or S2, Y is the domain of S, and Z is the domain of
;; SG:
;;             (IMPLIES (AND (SUBSETP X Y) (DISJOINT Y Z))
;;                      (DISJOINT X Z))

;; << 37 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  witnessing-instantiation-is-disjoint-from-generalizing-substitution \\ \index{witnessing-instantiation-is-dis!joint-from-generalizing-substitution}
\=\+{\bf let }\=\+{\it{s\/}}{\bf $\;$ be$\;\;$}{\rm{witnessing-instantiation}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{witnessing-instantiation}\- \\ 
{\bf in} \\ 
\=\+({\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} $\wedge$ {\rm{valid-state}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{valid-state}) \\ 
$\rightarrow$$\;\;\;\;${\rm{disjoint}}\,({\rm{domain}}\,({\it{s\/}})\index{domain}, {\rm{domain}}\,({\it{sg\/}})\index{domain})\index{disjoint}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim};; In the next case we abstract away DOMAIN-1 (and hence G, P, FREE,
;; and NEW-G).  Incidentally, a similar phenomenon occurred here to
;; the one reported just above the statement above of MAIN-THEOREM-1-CASE-3:
;; final polishing resulted in the need for another lemma.  That extra
;; lemma is DISJOINT-SET-DIFF-SUFFICIENCY in this case, to be found
;; in "sets.events".

;; << 38 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-relieved-5-lemma-4 \\ \index{main-hyps-relieved-5-lemma-4}
\=\+{\bf let }\=\+{\it{s\/}}{\bf $\;$ be$\;\;$}{\rm{witnessing-instantiation}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{witnessing-instantiation}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{s1\/}}{\bf $\;$ be$\;\;$}{\rm{restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{restrict}, \\ 
{\it{s2\/}}{\bf $\;$ be$\;\;$}{\rm{apply-to-subst}}\,({\rm{nullify-subst}}\,({\it{sg\/}})\index{nullify-subst}, {\rm{co-restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{co-restrict})\index{apply-to-subst}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} \\ 
$\wedge$$\;\;\;\;${\rm{valid-state}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{valid-state})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{disjoint}}\,({\rm{domain}}\,({\it{s1\/}})\index{domain}, {\rm{domain}}\,({\it{sg\/}})\index{domain})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{domain}}\,({\it{s2\/}})\index{domain}, {\rm{domain}}\,({\it{sg\/}})\index{domain})\index{disjoint})\-\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim};; The lemma MAIN-HYPS-RELIEVED-5-LEMMA-5-WIT is true because the
;; domain of s is contained in the free variables of the generalized
;; state (by choice, i.e. definition, of witnessing-instantiation),
;; which is disjoint from the intersection of the indicated
;; GEN-CLOSURE with the variables in the range of sg.  I'll use a
;; trick that I learned from Ken Kunen (definable Skolem function is
;; all, really) to reduce disjointness considerations to membership
;; considerations.

;; << 39 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-relieved-5-lemma-5-wit \\ \index{main-hyps-relieved-5-lemma-5-wit}
\=\+{\bf let }\=\+{\it{g\/}}{\bf $\;$ be$\;\;$}{\rm{caar}}\,({\it{state\/}}), \\ 
{\it{p\/}}{\bf $\;$ be$\;\;$}{\rm{cdar}}\,({\it{state\/}}), \\ 
{\it{free\/}}{\bf $\;$ be$\;\;$}{\rm{cdr}}\,({\it{state\/}}), \\ 
{\it{s\/}}{\bf $\;$ be$\;\;$}{\rm{witnessing-instantiation}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{witnessing-instantiation}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{new-g\/}}{\bf $\;$ be$\;\;$}{\rm{subst}}\,({\bf{t}}, {\rm{invert}}\,({\it{sg\/}})\index{invert}, {\it{g\/}})\index{subst}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{domain-1\/}}{\bf $\;$ be$\;\;$}{\rm{gen-closure}}\,(\=\+{\rm{cons}}\,({\it{new-g\/}}, {\it{p\/}}), \\ 
{\it{free\/}}, \\ 
{\rm{all-vars}}\,({\bf{t}}, {\it{new-g\/}})\index{all-vars})\-\index{gen-closure}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{s1\/}}{\bf $\;$ be$\;\;$}{\rm{restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{restrict}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} \\ 
$\wedge$$\;\;\;\;${\rm{valid-state}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{valid-state} \\ 
$\wedge$$\;\;\;\;$({\it{wit\/}} $\in$ {\rm{all-vars}}\,({\bf{f}}, {\rm{range}}\,({\it{sg\/}})\index{range})\index{all-vars}) \\ 
$\wedge$$\;\;\;\;$({\it{wit\/}} $\in$ {\rm{domain}}\,({\it{s\/}})\index{domain}))\- \\ 
$\rightarrow$$\;\;\;\;$({\it{wit\/}} $\not\in$ {\it{domain-1\/}})\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim};; << 40 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-relieved-5-lemma-5 \\ \index{main-hyps-relieved-5-lemma-5}
\=\+{\bf let }\=\+{\it{g\/}}{\bf $\;$ be$\;\;$}{\rm{caar}}\,({\it{state\/}}), \\ 
{\it{p\/}}{\bf $\;$ be$\;\;$}{\rm{cdar}}\,({\it{state\/}}), \\ 
{\it{free\/}}{\bf $\;$ be$\;\;$}{\rm{cdr}}\,({\it{state\/}}), \\ 
{\it{s\/}}{\bf $\;$ be$\;\;$}{\rm{witnessing-instantiation}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{witnessing-instantiation}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{new-g\/}}{\bf $\;$ be$\;\;$}{\rm{subst}}\,({\bf{t}}, {\rm{invert}}\,({\it{sg\/}})\index{invert}, {\it{g\/}})\index{subst}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{domain-1\/}}{\bf $\;$ be$\;\;$}{\rm{gen-closure}}\,(\=\+{\rm{cons}}\,({\it{new-g\/}}, {\it{p\/}}), \\ 
{\it{free\/}}, \\ 
{\rm{all-vars}}\,({\bf{t}}, {\it{new-g\/}})\index{all-vars})\-\index{gen-closure}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{s1\/}}{\bf $\;$ be$\;\;$}{\rm{restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{restrict}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} \\ 
$\wedge$$\;\;\;\;${\rm{valid-state}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{valid-state})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{disjoint}}\,({\rm{all-vars}}\,({\bf{f}}, {\rm{range}}\,({\it{sg\/}})\index{range})\index{all-vars}, {\rm{domain}}\,({\it{s1\/}})\index{domain})\index{disjoint}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim};; << 41 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-relieved-5-lemma-6 \\ \index{main-hyps-relieved-5-lemma-6}
\=\+{\bf let }\=\+{\it{g\/}}{\bf $\;$ be$\;\;$}{\rm{caar}}\,({\it{state\/}}), \\ 
{\it{p\/}}{\bf $\;$ be$\;\;$}{\rm{cdar}}\,({\it{state\/}}), \\ 
{\it{free\/}}{\bf $\;$ be$\;\;$}{\rm{cdr}}\,({\it{state\/}}), \\ 
{\it{s\/}}{\bf $\;$ be$\;\;$}{\rm{witnessing-instantiation}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{witnessing-instantiation}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{new-g\/}}{\bf $\;$ be$\;\;$}{\rm{subst}}\,({\bf{t}}, {\rm{invert}}\,({\it{sg\/}})\index{invert}, {\it{g\/}})\index{subst}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{domain-1\/}}{\bf $\;$ be$\;\;$}{\rm{gen-closure}}\,(\=\+{\rm{cons}}\,({\it{new-g\/}}, {\it{p\/}}), \\ 
{\it{free\/}}, \\ 
{\rm{all-vars}}\,({\bf{t}}, {\it{new-g\/}})\index{all-vars})\-\index{gen-closure}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{s2\/}}{\bf $\;$ be$\;\;$}{\rm{apply-to-subst}}\,(\=\+{\rm{nullify-subst}}\,({\it{sg\/}})\index{nullify-subst}, \\ 
{\rm{co-restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{co-restrict})\-\index{apply-to-subst}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} \\ 
$\wedge$$\;\;\;\;${\rm{valid-state}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{valid-state})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{disjoint}}\,({\rm{all-vars}}\,({\bf{f}}, {\rm{range}}\,({\it{s2\/}})\index{range})\index{all-vars}, {\rm{domain}}\,({\it{sg\/}})\index{domain})\index{disjoint}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim};; << 42 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-relieved-5 \\ \index{main-hyps-relieved-5}
\=\+{\bf let }\=\+{\it{g\/}}{\bf $\;$ be$\;\;$}{\rm{caar}}\,({\it{state\/}}), \\ 
{\it{p\/}}{\bf $\;$ be$\;\;$}{\rm{cdar}}\,({\it{state\/}}), \\ 
{\it{free\/}}{\bf $\;$ be$\;\;$}{\rm{cdr}}\,({\it{state\/}}), \\ 
{\it{s\/}}{\bf $\;$ be$\;\;$}{\rm{witnessing-instantiation}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{witnessing-instantiation}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{new-g\/}}{\bf $\;$ be$\;\;$}{\rm{subst}}\,({\bf{t}}, {\rm{invert}}\,({\it{sg\/}})\index{invert}, {\it{g\/}})\index{subst}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{domain-1\/}}{\bf $\;$ be$\;\;$}{\rm{gen-closure}}\,(\=\+{\rm{cons}}\,({\it{new-g\/}}, {\it{p\/}}), \\ 
{\it{free\/}}, \\ 
{\rm{all-vars}}\,({\bf{t}}, {\it{new-g\/}})\index{all-vars})\-\index{gen-closure}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{s1\/}}{\bf $\;$ be$\;\;$}{\rm{restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{restrict}, \\ 
{\it{s2\/}}{\bf $\;$ be$\;\;$}{\rm{apply-to-subst}}\,(\=\+{\rm{nullify-subst}}\,({\it{sg\/}})\index{nullify-subst}, \\ 
{\rm{co-restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{co-restrict})\-\index{apply-to-subst}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} \\ 
$\wedge$$\;\;\;\;${\rm{valid-state}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{valid-state})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{gen-setting-substitutions}}\,({\it{s1\/}}, {\it{s2\/}}, {\it{sg\/}})\index{gen-setting-substitutions}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim};; Now all that is left is MAIN-HYPS-RELIEVED-6.  Actually, this lemma
;; doesn't have anything to do with inverse substitutions or even with
;; generalization, really.  The idea is simply that one takes a valid
;; state and wishes to split its witnessing substitution into two
;; parts.  The parts are the respective restriction and co-restriction
;; of the original substitution to some set that is ``closed'' in the
;; appropriate sense.  Actually, the co-restriction is allowed to have
;; a substitution applied to it, whose domain is disjoint from the
;; goals ``outside'' that closure.  Below we give the lemmas and the
;; proof of MAIN-HYPS-RELIEVED-6 from those lemmas.  But first let us
;; introduce the necessary notions.

;; << 43 >>
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{all-vars-disjoint-or-subsetp} \\  
\=\+{\rm{all-vars-disjoint-or-subsetp}}\,({\it{goals\/}}, {\it{free\/}}, {\it{x\/}})\index{all-vars-disjoint-or-subsetp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{goals\/}}) \\ 
{\bf then }\=\+(\=\+{\rm{subsetp}}\,({\rm{intersection}}\,({\it{free\/}}, {\rm{all-vars}}\,({\bf{t}}, {\rm{car}}\,({\it{goals\/}}))\index{all-vars})\index{intersection}, {\it{x\/}})\index{subsetp} \\ 
$\vee$$\;\;\;\;${\rm{disjoint}}\,({\rm{intersection}}\,({\it{free\/}}, {\rm{all-vars}}\,({\bf{t}}, {\rm{car}}\,({\it{goals\/}}))\index{all-vars})\index{intersection}, {\it{x\/}})\index{disjoint})\- \\ 
$\wedge$$\;\;\;\;${\rm{all-vars-disjoint-or-subsetp}}\,({\rm{cdr}}\,({\it{goals\/}}), {\it{free\/}}, {\it{x\/}})\index{all-vars-disjoint-or-subsetp}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};; Our plan will be to show that (CDR STATE) has the above property
;; with respect to the free variables of the generalized state and the
;; appropriate gen-closure.  In cases where one applies a substitution
;; of the form (append s1 s2) to such a list of goals, where the
;; domain of s1 is contained in the intersection of those free
;; variables with that closure and the domain of s2 is disjoint from
;; that intersection, we'll show that the result is a theorem-list iff
;; each of the following are theorem-lists:  apply s1 to the goals
;; whose vars intersect its domain, and apply s2 to the rest.
;; Reduction rules about applying restrictions etc. will then finish
;; the job.

;; Notice the similarity of the following definition with new-gen-vars.
;; Think of vars as the closure variables, and free as the free variable
;; set within which this all "takes place".

;; << 44 >>
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{goals-intersecting-vars} \\  
\=\+{\rm{goals-intersecting-vars}}\,({\it{goals\/}}, {\it{free\/}}, {\it{vars\/}})\index{goals-intersecting-vars} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{goals\/}}) \\ 
{\bf then }\=\+{\bf let }\=\+{\it{current-free-vars\/}}{\bf $\;$ be$\;\;$}{\rm{intersection}}\,(\=\+{\it{free\/}}, \\ 
{\rm{all-vars}}\,({\bf{t}}, {\rm{car}}\,({\it{goals\/}}))\index{all-vars})\-\index{intersection}\- \\ 
{\bf in} \\ 
\=\+{\bf if }{\rm{disjoint}}\,({\it{current-free-vars\/}}, {\it{vars\/}})\index{disjoint} \\ 
{\bf then }{\rm{goals-intersecting-vars}}\,({\rm{cdr}}\,({\it{goals\/}}), {\it{free\/}}, {\it{vars\/}})\index{goals-intersecting-vars} \\ 
{\bf else }{\rm{cons}}\,(\=\+{\rm{car}}\,({\it{goals\/}}), \\ 
{\rm{goals-intersecting-vars}}\,(\=\+{\rm{cdr}}\,({\it{goals\/}}), \\ 
{\it{free\/}}, \\ 
{\it{vars\/}})\-\index{goals-intersecting-vars})\-$\;${\bf  endif}\-$\;${\bf  endlet}\- \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};; << 45 >>
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{goals-disjoint-from-vars} \\  
\=\+{\rm{goals-disjoint-from-vars}}\,({\it{goals\/}}, {\it{free\/}}, {\it{vars\/}})\index{goals-disjoint-from-vars} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{goals\/}}) \\ 
{\bf then }\=\+{\bf let }\=\+{\it{current-free-vars\/}}{\bf $\;$ be$\;\;$}{\rm{intersection}}\,(\=\+{\it{free\/}}, \\ 
{\rm{all-vars}}\,({\bf{t}}, {\rm{car}}\,({\it{goals\/}}))\index{all-vars})\-\index{intersection}\- \\ 
{\bf in} \\ 
\=\+{\bf if }{\rm{disjoint}}\,({\it{current-free-vars\/}}, {\it{vars\/}})\index{disjoint} \\ 
{\bf then }{\rm{cons}}\,(\=\+{\rm{car}}\,({\it{goals\/}}), \\ 
{\rm{goals-disjoint-from-vars}}\,({\rm{cdr}}\,({\it{goals\/}}), {\it{free\/}}, {\it{vars\/}})\index{goals-disjoint-from-vars})\- \\ 
{\bf else }{\rm{goals-disjoint-from-vars}}\,({\rm{cdr}}\,({\it{goals\/}}), {\it{free\/}}, {\it{vars\/}})\index{goals-disjoint-from-vars}$\;${\bf  endif}\-$\;${\bf  endlet}\- \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};; Now we begin the remaining goal, MAIN-HYPS-RELIEVED-6.  The idea is
;; to show that the appropriate goal list is a theorem-list by showing
;; separately that the first and the rest are theorems, since the
;; reasons are slightly different.  The first is a theorem because its
;; free vars are all in domain-1, hence in the domain of s1; so, s2
;; can be dropped from the APPEND.  The rest all have the property
;; that their free vars are contained in or disjoint from domain-1,
;; and for those disjoint from it, they do not contain variables from
;; the domain of sg.  Notice that the new current goal may violate the
;; latter requirement, since it may have no free vars at all but
;; contain vars from the domain of sg, and that's why we have to make
;; a special case out of it.

#|

(add-axiom main-hyps-relieved-6-first (rewrite)
  (let ((g (caar state))
        (p (cdar state))
        (free (cdr state))
        (s (witnessing-instantiation (generalize sg state))))
    (let ((new-g (subst t (invert sg) g)))
      (let ((domain-1
             (gen-closure (cons new-g p) free (all-vars t new-g))))
        (let ((s1 (restrict s domain-1))
              (s2 (apply-to-subst (nullify-subst sg)
                                  (co-restrict s domain-1))))
          (implies (and (generalize-okp sg state)
                        (valid-state (generalize sg state)))
                   (theorem (subst t (append s1 s2)
                                   (subst t (invert sg) g)))))))))

(add-axiom main-hyps-relieved-6-rest (rewrite)
  (let ((g (caar state))
        (p (cdar state))
        (free (cdr state))
        (s (witnessing-instantiation (generalize sg state))))
    (let ((new-g (subst t (invert sg) g)))
      (let ((domain-1
             (gen-closure (cons new-g p) free (all-vars t new-g))))
        (let ((s1 (restrict s domain-1))
              (s2 (apply-to-subst (nullify-subst sg)
                                  (co-restrict s domain-1))))
          (implies (and (generalize-okp sg state)
                        (valid-state (generalize sg state)))
                   (theorem-list (subst f (append s1 s2) p))))))))

(prove-lemma main-hyps-relieved-6 (rewrite)
  (let ((g (caar state))
        (p (cdar state))
        (free (cdr state))
        (s (witnessing-instantiation (generalize sg state))))
    (let ((new-g (subst t (invert sg) g)))
      (let ((domain-1
             (gen-closure (cons new-g p) free (all-vars t new-g))))
        (let ((s1 (restrict s domain-1))
              (s2 (apply-to-subst (nullify-subst sg)
                                  (co-restrict s domain-1))))
          (implies (and (generalize-okp sg state)
                        (valid-state (generalize sg state)))
                   (theorem-list (subst f (append s1 s2)
                                        (cons (subst t (invert sg) g) p))))))))
  ((disable-theory t)
   (enable-theory ground-zero)
   (enable main-hyps-relieved-6-first main-hyps-relieved-6-rest subst theorem-list)))

|#

;; The first is true because the free vars in new-g are all in the
;; domain of s1, since they are all in domain-1.  By the way, the
;; proof-checker was useful here; I dove to the subst term (after
;; adding abbreviations and promoting hypotheses) and saw that I
;; wanted to rewrite with SUBST-APPEND-NOT-OCCUR-2.  I also notice the
;; need for GEN-CLOSURE-CONTAINS-THIRD-ARG during the attempt to prove
;; a goal.

;; First, we only want to open up GENERALIZE when we are looking at
;; goals, not when we are simply asking about the witnessing
;; substitution.

;; << 46 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  car-generalize \\ \index{car-generalize}
\=\+{\rm{car}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize}) \\ 
$=$$\;\;\;\;${\rm{cons}}\,({\rm{subst}}\,({\bf{t}}, {\rm{invert}}\,({\it{sg\/}})\index{invert}, {\rm{caar}}\,({\it{state\/}}))\index{subst}, {\rm{cdar}}\,({\it{state\/}}))\-
\end{tabbing}

\begin{verbatim};; << 47 >>
\end{verbatim}
\noindent{\sc Event}:   Disable generalize.

\addvspace{18pt}

\begin{verbatim};; Inspection of the proof of a subgoal of MAIN-HYPS-RELIEVED-6-FIRST
;; suggests that we need the following lemma.  Actually, before the
;; final polishing it was the case that the following version sufficed.
;; But final polishing led me to prove a "better" version, as well
;; as the lemma DISJOINT-SET-DIFF-GENERAL in "sets.events".

#|
(prove-lemma gen-closure-contains-third-arg (rewrite)
  (implies (subsetp domain free)
           (subsetp (intersection domain free-vars-so-far)
                    (gen-closure goals free free-vars-so-far))))
|#

;; << 48 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  gen-closure-contains-third-arg \\ \index{gen-closure-contains-third-arg}
\=\+{\rm{subsetp}}\,({\it{x\/}}, {\rm{intersection}}\,({\it{free\/}}, {\it{free-vars-so-far\/}})\index{intersection})\index{subsetp} \\ 
$\rightarrow$$\;\;\;\;${\rm{subsetp}}\,({\it{x\/}}, {\rm{gen-closure}}\,({\it{goals\/}}, {\it{free\/}}, {\it{free-vars-so-far\/}})\index{gen-closure})\index{subsetp}\-
\end{tabbing}


\begin{verbatim};; << 49 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-relieved-6-first \\ \index{main-hyps-relieved-6-first}
\=\+{\bf let }\=\+{\it{g\/}}{\bf $\;$ be$\;\;$}{\rm{caar}}\,({\it{state\/}}), \\ 
{\it{p\/}}{\bf $\;$ be$\;\;$}{\rm{cdar}}\,({\it{state\/}}), \\ 
{\it{free\/}}{\bf $\;$ be$\;\;$}{\rm{cdr}}\,({\it{state\/}}), \\ 
{\it{s\/}}{\bf $\;$ be$\;\;$}{\rm{witnessing-instantiation}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{witnessing-instantiation}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{new-g\/}}{\bf $\;$ be$\;\;$}{\rm{subst}}\,({\bf{t}}, {\rm{invert}}\,({\it{sg\/}})\index{invert}, {\it{g\/}})\index{subst}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{domain-1\/}}{\bf $\;$ be$\;\;$}{\rm{gen-closure}}\,(\=\+{\rm{cons}}\,({\it{new-g\/}}, {\it{p\/}}), \\ 
{\it{free\/}}, \\ 
{\rm{all-vars}}\,({\bf{t}}, {\it{new-g\/}})\index{all-vars})\-\index{gen-closure}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{s1\/}}{\bf $\;$ be$\;\;$}{\rm{restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{restrict}, \\ 
{\it{s2\/}}{\bf $\;$ be$\;\;$}{\rm{apply-to-subst}}\,(\=\+{\rm{nullify-subst}}\,({\it{sg\/}})\index{nullify-subst}, \\ 
{\rm{co-restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{co-restrict})\-\index{apply-to-subst}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} \\ 
$\wedge$$\;\;\;\;${\rm{valid-state}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{valid-state})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{theorem}}\,({\rm{subst}}\,({\bf{t}}, {\rm{append}}\,({\it{s1\/}}, {\it{s2\/}}), {\it{new-g\/}})\index{subst})\index{theorem}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-
\end{tabbing}


\begin{verbatim};; Now all that remains is MAIN-HYPS-RELIEVED-6-REST.

#|

;; I originally forgot the (TERMP F P) hypothesis below, but it wasn't
;; very hard to back up and fix this.

(add-axiom main-hyps-relieved-6-rest-generalization (rewrite)
  (let ((s1 (restrict s domain-1))
        (s2 (apply-to-subst (nullify-subst sg)
                            (co-restrict s domain-1))))
    (implies (and (var-substp sg)
                  (var-substp s)
                  (subsetp (domain s) new-free)
                  (termp f p)
                  (theorem-list (subst f s p)) 
                  (disjoint (domain sg)
                            (all-vars f (goals-disjoint-from-vars
                                         p new-free domain-1)))
                  (all-vars-disjoint-or-subsetp p new-free domain-1)) 
             (theorem-list (subst f (append s1 s2) p)))))

(add-axiom main-hyps-relieved-6-rest-lemma-1 (rewrite)
  (let ((g (caar state))
        (p (cdar state))
        (free (cdr state))
        (s (witnessing-instantiation (generalize sg state))))
    (let ((new-g (subst t (invert sg) g)))
      (let ((domain-1
             (gen-closure (cons new-g p) free (all-vars t new-g))))
        (let ((s1 (restrict s domain-1))
              (s2 (apply-to-subst (nullify-subst sg)
                                  (co-restrict s domain-1))))
          (implies (and (generalize-okp sg state)
                        (valid-state (generalize sg state)))
                   (disjoint (domain sg)
                             (all-vars f (goals-disjoint-from-vars
                                          p (cdr (generalize sg state)) domain-1)))))))))

;; Minor note:  I used the BREAK-LEMMA feature of NQTHM to realize
;; that I needed the following lemma.

(add-axiom main-hyps-relieved-6-rest-lemma-2 (rewrite)
  (let ((g (caar state))
        (p (cdar state))
        (free (cdr state))
        (s (witnessing-instantiation (generalize sg state))))
    (let ((new-g (subst t (invert sg) g)))
      (let ((domain-1
             (gen-closure (cons new-g p) free (all-vars t new-g))))
        (let ((s1 (restrict s domain-1))
              (s2 (apply-to-subst (nullify-subst sg)
                                  (co-restrict s domain-1))))
          (implies (and (generalize-okp sg state)
                        (valid-state (generalize sg state)))
                   (all-vars-disjoint-or-subsetp p (cdr (generalize sg state)) domain-1)))))))

(prove-lemma main-hyps-relieved-6-rest (rewrite)
  (let ((g (caar state))
        (p (cdar state))
        (free (cdr state))
        (s (witnessing-instantiation (generalize sg state))))
    (let ((new-g (subst t (invert sg) g)))
      (let ((domain-1
             (gen-closure (cons new-g p) free (all-vars t new-g))))
        (let ((s1 (restrict s domain-1))
              (s2 (apply-to-subst (nullify-subst sg)
                                  (co-restrict s domain-1))))
          (implies (and (generalize-okp sg state)
                        (valid-state (generalize sg state)))
                   (theorem-list (subst f (append s1 s2) p)))))))
  ((disable-theory t)
   (enable-theory ground-zero)
   (enable theorem-list subst car-generalize ;; so that we can get at p from (car state)
           ;; relieving hyps of main-hyps-relieved-6-rest-generalization:
           main-hyps-relieved-6-rest-lemma-1 main-hyps-relieved-6-rest-lemma-2
           ;; to relieve the (termp f p) hypothesis in main-hyps-relieved-6-rest-generalization:
           statep termp-list-cons
           generalize-okp valid-state-opener main-hyps-relieved-6-rest-generalization)))

;; At this point I did a sanity check and sure enough, the pushed
;; lemmas all go through at this point:  main-hyps-relieved-6,
;; main-hyps-relieved, main-theorem-1-case-4, main-theorem-1, and
;; generalize-is-correct.

|#

;; It remains to prove MAIN-HYPS-RELIEVED-6-REST-LEMMA-1,
;; MAIN-HYPS-RELIEVED-6-REST-LEMMA-2, and
;; MAIN-HYPS-RELIEVED-6-REST-GENERALIZATION.

;; For the first of these we need the following trivial observation.

;; << 50 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  goals-disjoint-from-vars-subsetp \\ \index{goals-disjoint-from-vars-subsetp}
{\rm{subsetp}}\,({\rm{goals-disjoint-from-vars}}\,({\it{goals\/}}, {\it{free\/}}, {\it{vars\/}})\index{goals-disjoint-from-vars}, {\it{goals\/}})\index{subsetp}
\end{tabbing}

\begin{verbatim};; Unfortunately the observation above doesn't quite suffice, because
;; of a technical problem with free variables in hypotheses.  The
;; following consequence does, though.

;; << 51 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  disjoint-all-vars-goals-disjoint-from-vars \\ \index{disjoint-all-vars-goals-disjoint!-from-vars}
\=\+{\rm{disjoint}}\,({\it{x\/}}, {\rm{all-vars}}\,({\bf{f}}, {\it{goals\/}})\index{all-vars})\index{disjoint} \\ 
$\rightarrow$$\;\;\;\;${\rm{disjoint}}\,({\it{x\/}}, {\rm{all-vars}}\,({\bf{f}}, {\rm{goals-disjoint-from-vars}}\,({\it{goals\/}}, {\it{free\/}}, {\it{vars\/}})\index{goals-disjoint-from-vars})\index{all-vars})\index{disjoint}\-
\end{tabbing}

\begin{verbatim};; << 52 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-relieved-6-rest-lemma-1 \\ \index{main-hyps-relieved-6-rest-lemma!-1}
\=\+{\bf let }\=\+{\it{g\/}}{\bf $\;$ be$\;\;$}{\rm{caar}}\,({\it{state\/}}), \\ 
{\it{p\/}}{\bf $\;$ be$\;\;$}{\rm{cdar}}\,({\it{state\/}}), \\ 
{\it{free\/}}{\bf $\;$ be$\;\;$}{\rm{cdr}}\,({\it{state\/}}), \\ 
{\it{s\/}}{\bf $\;$ be$\;\;$}{\rm{witnessing-instantiation}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{witnessing-instantiation}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{new-g\/}}{\bf $\;$ be$\;\;$}{\rm{subst}}\,({\bf{t}}, {\rm{invert}}\,({\it{sg\/}})\index{invert}, {\it{g\/}})\index{subst}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{domain-1\/}}{\bf $\;$ be$\;\;$}{\rm{gen-closure}}\,(\=\+{\rm{cons}}\,({\it{new-g\/}}, {\it{p\/}}), \\ 
{\it{free\/}}, \\ 
{\rm{all-vars}}\,({\bf{t}}, {\it{new-g\/}})\index{all-vars})\-\index{gen-closure}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{s1\/}}{\bf $\;$ be$\;\;$}{\rm{restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{restrict}, \\ 
{\it{s2\/}}{\bf $\;$ be$\;\;$}{\rm{apply-to-subst}}\,(\=\+{\rm{nullify-subst}}\,({\it{sg\/}})\index{nullify-subst}, \\ 
{\rm{co-restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{co-restrict})\-\index{apply-to-subst}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} \\ 
$\wedge$$\;\;\;\;${\rm{valid-state}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{valid-state})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{disjoint}}\,(\=\+{\rm{domain}}\,({\it{sg\/}})\index{domain}, \\ 
{\rm{all-vars}}\,(\=\+{\bf{f}}, \\ 
{\rm{goals-disjoint-from-vars}}\,(\=\+{\it{p\/}}, \\ 
{\rm{cdr}}\,({\rm{generalize}}\,(\=\+{\it{sg\/}}, \\ 
{\it{state\/}})\-\index{generalize}), \\ 
{\it{domain-1\/}})\-\index{goals-disjoint-from-vars})\-\index{all-vars})\-\index{disjoint}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim};; The next goal, MAIN-HYPS-RELIEVED-6-REST-LEMMA-2, needs the lemma
;; ALL-VARS-DISJOINT-OR-SUBSETP-GEN-CLOSURE below.  That lemma's
;; mechanical proof depends on the trivial observation
;; DISJOINT-INTERSECTION3-MIDDLE in file sets.events.

;; << 53 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  all-vars-disjoint-or-subsetp-gen-closure \\ \index{all-vars-disjoint-or-subsetp-ge!n-closure}
\=\+{\rm{subsetp}}\,({\it{domain\/}}, {\it{free\/}})\index{subsetp} \\ 
$\rightarrow$$\;\;\;\;${\rm{all-vars-disjoint-or-subsetp}}\,(\=\+{\it{goals\/}}, \\ 
{\it{domain\/}}, \\ 
{\rm{gen-closure}}\,({\rm{cons}}\,({\it{g\/}}, {\it{goals\/}}), {\it{free\/}}, {\it{vars\/}})\index{gen-closure})\-\index{all-vars-disjoint-or-subsetp}\-
\end{tabbing}

\begin{verbatim};; << 54 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-relieved-6-rest-lemma-2 \\ \index{main-hyps-relieved-6-rest-lemma!-2}
\=\+{\bf let }\=\+{\it{g\/}}{\bf $\;$ be$\;\;$}{\rm{caar}}\,({\it{state\/}}), \\ 
{\it{p\/}}{\bf $\;$ be$\;\;$}{\rm{cdar}}\,({\it{state\/}}), \\ 
{\it{free\/}}{\bf $\;$ be$\;\;$}{\rm{cdr}}\,({\it{state\/}}), \\ 
{\it{s\/}}{\bf $\;$ be$\;\;$}{\rm{witnessing-instantiation}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{witnessing-instantiation}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{new-g\/}}{\bf $\;$ be$\;\;$}{\rm{subst}}\,({\bf{t}}, {\rm{invert}}\,({\it{sg\/}})\index{invert}, {\it{g\/}})\index{subst}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{domain-1\/}}{\bf $\;$ be$\;\;$}{\rm{gen-closure}}\,(\=\+{\rm{cons}}\,({\it{new-g\/}}, {\it{p\/}}), \\ 
{\it{free\/}}, \\ 
{\rm{all-vars}}\,({\bf{t}}, {\it{new-g\/}})\index{all-vars})\-\index{gen-closure}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{s1\/}}{\bf $\;$ be$\;\;$}{\rm{restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{restrict}, \\ 
{\it{s2\/}}{\bf $\;$ be$\;\;$}{\rm{apply-to-subst}}\,(\=\+{\rm{nullify-subst}}\,({\it{sg\/}})\index{nullify-subst}, \\ 
{\rm{co-restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{co-restrict})\-\index{apply-to-subst}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} \\ 
$\wedge$$\;\;\;\;${\rm{valid-state}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{valid-state})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{all-vars-disjoint-or-subsetp}}\,(\=\+{\it{p\/}}, \\ 
{\rm{cdr}}\,({\rm{generalize}}\,(\=\+{\it{sg\/}}, \\ 
{\it{state\/}})\-\index{generalize}), \\ 
{\it{domain-1\/}})\-\index{all-vars-disjoint-or-subsetp}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim};; Finally, all that's left is
;; MAIN-HYPS-RELIEVED-6-REST-GENERALIZATION.  An attempted proof by
;; induction of that theorem results in 11 goals, all but one of which
;; goes through automatically.  The remaining one is as follows.

#|

(IMPLIES
 (AND
  (DISJOINT NEW-FREE
            (INTERSECTION DOMAIN-1
                          (ALL-VARS T X)))
  (THEOREM-LIST
   (SUBST F
          (APPEND (RESTRICT S DOMAIN-1)
                  (APPLY-TO-SUBST (NULLIFY-SUBST SG)
                                  (CO-RESTRICT S DOMAIN-1)))
          Z))
  (MAPPING SG)
  (VARIABLE-LISTP (DOMAIN SG))
  (TERMP F (RANGE SG))
  (MAPPING S)
  (VARIABLE-LISTP (DOMAIN S))
  (TERMP F (RANGE S))
  (SUBSETP (DOMAIN S) NEW-FREE)
  (TERMP T X)
  (TERMP F Z)
  (THEOREM (SUBST T S X))
  (THEOREM-LIST (SUBST F S Z))
  (DISJOINT (DOMAIN SG) (ALL-VARS T X))
  (DISJOINT (DOMAIN SG)
            (ALL-VARS F
                      (GOALS-DISJOINT-FROM-VARS Z NEW-FREE DOMAIN-1)))
  (ALL-VARS-DISJOINT-OR-SUBSETP Z NEW-FREE DOMAIN-1))
 (THEOREM (SUBST T
                 (APPEND (RESTRICT S DOMAIN-1)
                         (APPLY-TO-SUBST (NULLIFY-SUBST SG)
                                         (CO-RESTRICT S DOMAIN-1)))
                 X)))

|#

;; Let us attempt to prove this goal with the proof-checker, thus
;; seeing why the rewriter can't handle it automatically.  We would
;; like to rewrite with SUBST-APPEND-NOT-OCCUR-1 to replace the
;; conclusion with:

#|
(THEOREM (SUBST T
                (APPLY-TO-SUBST (NULLIFY-SUBST SG)
                                (CO-RESTRICT S DOMAIN-1))
                X))
|#

;; However, in order to do that we need to observe that under the
;; hypotheses, the following holds.

#|
(DISJOINT (ALL-VARS F
                    (DOMAIN (RESTRICT S DOMAIN-1)))
          (ALL-VARS T X))
|#

;; This is one of those cases of a problem with free variables in
;; hypotheses that are so annoying.  The lemma DOMAIN-RESTRICT has
;; been put in alists.events to help with this.  But then we lose the
;; fact that the first ALL-VARS in the goal above may be removed.  The
;; lemma VARIABLE-LISTP-INTERSECTION has been added to terms.events to
;; take care of that.

;; Now it looks like the rewrite using SUBST-APPEND-NOT-OCCUR-1 should
;; succeed, since all hypotheses are relieved by rewriting alone.
;; Just to make sure, we back up in the proof checker and see if BASH
;; uses this rule on our original goal.  Sure enough, it does.

;; Now our conclusion is the one displayed above, i.e.

#|
(THEOREM (SUBST T
                (APPLY-TO-SUBST (NULLIFY-SUBST SG)
                                (CO-RESTRICT S DOMAIN-1))
                X))
|#

;; Since (as we already know) (NULLIFY-SUBST SG) has the same domain
;; as does SG, and since the hypotheses imply that (DOMAIN SG) is
;; disjoint from the variables of X, the SUBST expression in this
;; conclusion should simplify to:

#|
(SUBST T (NULLIFY-SUBST SG)
       (SUBST T (CO-RESTRICT S DOMAIN-1)
              X))
|#

;; We therefore need the lemma SUBST-APPLY-TO-SUBST-ELIMINATOR below
;; (which is used under the substitution where S gets (CO-RESTRICT S
;; DOMAIN-1) and SG gets (NULLIFY-SUBST SG)).  However, we'll
;; immediately derive the desired consequence and then disable this
;; lemma, since it appears that it would loop with
;; COMPOSE-PROPERTY-REVERSED.

;; << 55 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  subst-apply-to-subst-eliminator \\ \index{subst-apply-to-subst-eliminator}
\=\+(\=\+{\rm{variable-listp}}\,({\rm{domain}}\,({\it{sg\/}})\index{domain})\index{variable-listp} \\ 
$\wedge$$\;\;\;\;${\rm{variable-listp}}\,({\rm{domain}}\,({\it{s\/}})\index{domain})\index{variable-listp} \\ 
$\wedge$$\;\;\;\;${\rm{termp}}\,({\bf{t}}, {\it{x\/}})\index{termp} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{domain}}\,({\it{sg\/}})\index{domain}, {\rm{all-vars}}\,({\bf{t}}, {\it{x\/}})\index{all-vars})\index{disjoint})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{subst}}\,({\bf{t}}, {\rm{apply-to-subst}}\,({\it{sg\/}}, {\it{s\/}})\index{apply-to-subst}, {\it{x\/}})\index{subst} $=$ {\rm{subst}}\,({\bf{t}}, {\it{sg\/}}, {\rm{subst}}\,({\bf{t}}, {\it{s\/}}, {\it{x\/}})\index{subst})\index{subst})\-
\end{tabbing}

\begin{verbatim};; << 56 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  theorem-subst-apply-to-subst-with-disjoint-domain \\ \index{theorem-subst-apply-to-subst-wit!h-disjoint-domain}
\=\+(\=\+{\rm{var-substp}}\,({\it{sg\/}})\index{var-substp} \\ 
$\wedge$$\;\;\;\;${\rm{var-substp}}\,({\it{s\/}})\index{var-substp} \\ 
$\wedge$$\;\;\;\;${\rm{termp}}\,({\bf{t}}, {\it{x\/}})\index{termp} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{domain}}\,({\it{sg\/}})\index{domain}, {\rm{all-vars}}\,({\bf{t}}, {\it{x\/}})\index{all-vars})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{theorem}}\,({\rm{subst}}\,({\bf{t}}, {\it{s\/}}, {\it{x\/}})\index{subst})\index{theorem})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{theorem}}\,({\rm{subst}}\,({\bf{t}}, {\rm{apply-to-subst}}\,({\it{sg\/}}, {\it{s\/}})\index{apply-to-subst}, {\it{x\/}})\index{subst})\index{theorem}\-
\end{tabbing}

\begin{verbatim};; << 57 >>
\end{verbatim}
\noindent{\sc Event}:   Disable subst-apply-to-subst-eliminator.

\addvspace{18pt}

\begin{verbatim};; The proof of the remaining goal should go through now, one might
;; think.  However, we need one more observation first, because we
;; need to apply the following lemma.

#|
(PROVE-LEMMA SUBST-CO-RESTRICT
             (REWRITE)
             (IMPLIES (AND (DISJOINT X
                                     (INTERSECTION (DOMAIN S)
                                                   (ALL-VARS FLG TERM)))
                           (VARIABLE-LISTP (DOMAIN S))
                           (TERMP FLG TERM))
                      (EQUAL (SUBST FLG (CO-RESTRICT S X) TERM)
                             (SUBST FLG S TERM))))
|#

;; but the first hypothesis of this lemma needs special handling because of
;; free variables.  The lemma DISJOINT-SUBSETP-HACK was proved at this point,
;; and appears now in sets.events.

;; And finally, we finish.  During polishing I suddenly needed the
;; lemma SUBSETP-INTERSECTION-MONOTONE-2, which is now included in
;; "sets.events", and which in turn suggested
;; SUBSETP-INTERSECTION-COMMUTER there.

;; << 58 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-relieved-6-rest-generalization \\ \index{main-hyps-relieved-6-rest-gener!alization}
\=\+{\bf let }\=\+{\it{s1\/}}{\bf $\;$ be$\;\;$}{\rm{restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{restrict}, \\ 
{\it{s2\/}}{\bf $\;$ be$\;\;$}{\rm{apply-to-subst}}\,({\rm{nullify-subst}}\,({\it{sg\/}})\index{nullify-subst}, {\rm{co-restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{co-restrict})\index{apply-to-subst}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{var-substp}}\,({\it{sg\/}})\index{var-substp} \\ 
$\wedge$$\;\;\;\;${\rm{var-substp}}\,({\it{s\/}})\index{var-substp} \\ 
$\wedge$$\;\;\;\;${\rm{subsetp}}\,({\rm{domain}}\,({\it{s\/}})\index{domain}, {\it{new-free\/}})\index{subsetp} \\ 
$\wedge$$\;\;\;\;${\rm{termp}}\,({\bf{f}}, {\it{p\/}})\index{termp} \\ 
$\wedge$$\;\;\;\;${\rm{theorem-list}}\,({\rm{subst}}\,({\bf{f}}, {\it{s\/}}, {\it{p\/}})\index{subst})\index{theorem-list} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,(\=\+{\rm{domain}}\,({\it{sg\/}})\index{domain}, \\ 
{\rm{all-vars}}\,(\=\+{\bf{f}}, \\ 
{\rm{goals-disjoint-from-vars}}\,(\=\+{\it{p\/}}, \\ 
{\it{new-free\/}}, \\ 
{\it{domain-1\/}})\-\index{goals-disjoint-from-vars})\-\index{all-vars})\-\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{all-vars-disjoint-or-subsetp}}\,({\it{p\/}}, {\it{new-free\/}}, {\it{domain-1\/}})\index{all-vars-disjoint-or-subsetp})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{theorem-list}}\,({\rm{subst}}\,({\bf{f}}, {\rm{append}}\,({\it{s1\/}}, {\it{s2\/}}), {\it{p\/}})\index{subst})\index{theorem-list}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim};; Now to clean up the goals that have been pushed above:

;; << 59 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-relieved-6-rest \\ \index{main-hyps-relieved-6-rest}
\=\+{\bf let }\=\+{\it{g\/}}{\bf $\;$ be$\;\;$}{\rm{caar}}\,({\it{state\/}}), \\ 
{\it{p\/}}{\bf $\;$ be$\;\;$}{\rm{cdar}}\,({\it{state\/}}), \\ 
{\it{free\/}}{\bf $\;$ be$\;\;$}{\rm{cdr}}\,({\it{state\/}}), \\ 
{\it{s\/}}{\bf $\;$ be$\;\;$}{\rm{witnessing-instantiation}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{witnessing-instantiation}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{new-g\/}}{\bf $\;$ be$\;\;$}{\rm{subst}}\,({\bf{t}}, {\rm{invert}}\,({\it{sg\/}})\index{invert}, {\it{g\/}})\index{subst}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{domain-1\/}}{\bf $\;$ be$\;\;$}{\rm{gen-closure}}\,(\=\+{\rm{cons}}\,({\it{new-g\/}}, {\it{p\/}}), \\ 
{\it{free\/}}, \\ 
{\rm{all-vars}}\,({\bf{t}}, {\it{new-g\/}})\index{all-vars})\-\index{gen-closure}\- \\ 
{\bf in} \\ 
\=\+{\bf let }\=\+{\it{s1\/}}{\bf $\;$ be$\;\;$}{\rm{restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{restrict}, \\ 
{\it{s2\/}}{\bf $\;$ be$\;\;$}{\rm{apply-to-subst}}\,(\=\+{\rm{nullify-subst}}\,({\it{sg\/}})\index{nullify-subst}, \\ 
{\rm{co-restrict}}\,({\it{s\/}}, {\it{domain-1\/}})\index{co-restrict})\-\index{apply-to-subst}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} \\ 
$\wedge$$\;\;\;\;${\rm{valid-state}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{valid-state})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{theorem-list}}\,({\rm{subst}}\,({\bf{f}}, {\rm{append}}\,({\it{s1\/}}, {\it{s2\/}}), {\it{p\/}})\index{subst})\index{theorem-list}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim};; << 60 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-relieved-6 \\ \index{main-hyps-relieved-6}
\=\+({\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} $\wedge$ {\rm{valid-state}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{valid-state}) \\ 
$\rightarrow$$\;\;\;\;${\rm{theorem-list}}\,({\rm{subst}}\,(\=\+{\bf{f}}, \\ 
{\rm{append}}\,(\=\+{\rm{restrict}}\,(\=\+{\rm{witnessing-instantiation}}\,({\rm{generalize}}\,(\=\+{\it{sg\/}}, \\ 
{\it{state\/}})\-\index{generalize})\index{witnessing-instantiation}, \\ 
{\rm{gen-closure}}\,(\=\+{\rm{cons}}\,(\=\+{\rm{subst}}\,(\=\+{\bf{t}}, \\ 
{\rm{invert}}\,({\it{sg\/}})\index{invert}, \\ 
{\rm{caar}}\,({\it{state\/}}))\-\index{subst}, \\ 
{\rm{cdar}}\,({\it{state\/}}))\-, \\ 
{\rm{cdr}}\,({\it{state\/}}), \\ 
{\rm{all-vars}}\,(\=\+{\bf{t}}, \\ 
{\rm{subst}}\,(\=\+{\bf{t}}, \\ 
{\rm{invert}}\,({\it{sg\/}})\index{invert}, \\ 
{\rm{caar}}\,({\it{state\/}}))\-\index{subst})\-\index{all-vars})\-\index{gen-closure})\-\index{restrict}, \\ 
{\rm{apply-to-subst}}\,(\=\+{\rm{nullify-subst}}\,({\it{sg\/}})\index{nullify-subst}, \\ 
{\rm{co-restrict}}\,(\=\+{\rm{witnessing-instantiation}}\,({\rm{generalize}}\,(\=\+{\it{sg\/}}, \\ 
{\it{state\/}})\-\index{generalize})\index{witnessing-instantiation}, \\ 
{\rm{gen-closure}}\,(\=\+{\rm{cons}}\,(\=\+{\rm{subst}}\,(\=\+{\bf{t}}, \\ 
{\rm{invert}}\,({\it{sg\/}})\index{invert}, \\ 
{\rm{caar}}\,({\it{state\/}}))\-\index{subst}, \\ 
{\rm{cdar}}\,({\it{state\/}}))\-, \\ 
{\rm{cdr}}\,({\it{state\/}}), \\ 
{\rm{all-vars}}\,(\=\+{\bf{t}}, \\ 
{\rm{subst}}\,(\=\+{\bf{t}}, \\ 
{\rm{invert}}\,({\it{sg\/}})\index{invert}, \\ 
{\rm{caar}}\,({\it{state\/}}))\-\index{subst})\-\index{all-vars})\-\index{gen-closure})\-\index{co-restrict})\-\index{apply-to-subst})\-, \\ 
{\rm{cons}}\,({\rm{subst}}\,({\bf{t}}, {\rm{invert}}\,({\it{sg\/}})\index{invert}, {\rm{caar}}\,({\it{state\/}}))\index{subst}, {\rm{cdar}}\,({\it{state\/}})))\-\index{subst})\index{theorem-list}\-
\end{tabbing}

\begin{verbatim};; << 61 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-hyps-relieved \\ \index{main-hyps-relieved}
\=\+({\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} $\wedge$ {\rm{valid-state}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{valid-state}) \\ 
$\rightarrow$$\;\;\;\;${\rm{main-hyps}}\,(\=\+{\rm{restrict}}\,(\=\+{\rm{witnessing-instantiation}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{witnessing-instantiation}, \\ 
{\rm{gen-closure}}\,(\=\+{\rm{cons}}\,(\=\+{\rm{subst}}\,({\bf{t}}, {\rm{invert}}\,({\it{sg\/}})\index{invert}, {\rm{caar}}\,({\it{state\/}}))\index{subst}, \\ 
{\rm{cdar}}\,({\it{state\/}}))\-, \\ 
{\rm{cdr}}\,({\it{state\/}}), \\ 
{\rm{all-vars}}\,(\=\+{\bf{t}}, \\ 
{\rm{subst}}\,(\=\+{\bf{t}}, \\ 
{\rm{invert}}\,({\it{sg\/}})\index{invert}, \\ 
{\rm{caar}}\,({\it{state\/}}))\-\index{subst})\-\index{all-vars})\-\index{gen-closure})\-\index{restrict}, \\ 
{\rm{apply-to-subst}}\,(\=\+{\rm{nullify-subst}}\,({\it{sg\/}})\index{nullify-subst}, \\ 
{\rm{co-restrict}}\,(\=\+{\rm{witnessing-instantiation}}\,({\rm{generalize}}\,(\=\+{\it{sg\/}}, \\ 
{\it{state\/}})\-\index{generalize})\index{witnessing-instantiation}, \\ 
{\rm{gen-closure}}\,(\=\+{\rm{cons}}\,(\=\+{\rm{subst}}\,(\=\+{\bf{t}}, \\ 
{\rm{invert}}\,({\it{sg\/}})\index{invert}, \\ 
{\rm{caar}}\,({\it{state\/}}))\-\index{subst}, \\ 
{\rm{cdar}}\,({\it{state\/}}))\-, \\ 
{\rm{cdr}}\,({\it{state\/}}), \\ 
{\rm{all-vars}}\,(\=\+{\bf{t}}, \\ 
{\rm{subst}}\,(\=\+{\bf{t}}, \\ 
{\rm{invert}}\,({\it{sg\/}})\index{invert}, \\ 
{\rm{caar}}\,({\it{state\/}}))\-\index{subst})\-\index{all-vars})\-\index{gen-closure})\-\index{co-restrict})\-\index{apply-to-subst}, \\ 
{\it{sg\/}}, \\ 
{\rm{caar}}\,({\it{state\/}}), \\ 
{\rm{cdar}}\,({\it{state\/}}))\-\index{main-hyps}\-
\end{tabbing}

\begin{verbatim};; << 62 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-theorem-1-case-4 \\ \index{main-theorem-1-case-4}
\=\+({\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} $\wedge$ {\rm{valid-state}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{valid-state}) \\ 
$\rightarrow$$\;\;\;\;${\rm{theorem-list}}\,({\rm{subst}}\,({\bf{f}}, {\rm{gen-inst}}\,({\it{sg\/}}, {\it{state\/}})\index{gen-inst}, {\rm{car}}\,({\it{state\/}}))\index{subst})\index{theorem-list}\-
\end{tabbing}

\begin{verbatim};; << 63 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  main-theorem-1 \\ \index{main-theorem-1}
\=\+{\bf let }\=\+{\it{wit\/}}{\bf $\;$ be$\;\;$}{\rm{gen-inst}}\,({\it{sg\/}}, {\it{state\/}})\index{gen-inst}\- \\ 
{\bf in} \\ 
\=\+({\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} $\wedge$ {\rm{valid-state}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{valid-state}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{statep}}\,({\it{state\/}})\index{statep} \\ 
$\wedge$$\;\;\;\;${\rm{var-substp}}\,({\it{wit\/}})\index{var-substp} \\ 
$\wedge$$\;\;\;\;${\rm{subsetp}}\,({\rm{domain}}\,({\it{wit\/}})\index{domain}, {\rm{cdr}}\,({\it{state\/}}))\index{subsetp} \\ 
$\wedge$$\;\;\;\;${\rm{theorem-list}}\,({\rm{subst}}\,({\bf{f}}, {\it{wit\/}}, {\rm{car}}\,({\it{state\/}}))\index{subst})\index{theorem-list})\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim};; << 64 >>
\end{verbatim}\begin{tabbing}{\sc Theorem}:  generalize-is-correct \\ \index{generalize-is-correct}
\=\+({\rm{generalize-okp}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize-okp} $\wedge$ {\rm{valid-state}}\,({\rm{generalize}}\,({\it{sg\/}}, {\it{state\/}})\index{generalize})\index{valid-state}) \\ 
$\rightarrow$$\;\;\;\;${\rm{valid-state}}\,({\it{state\/}})\index{valid-state}\-
\end{tabbing}


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