\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};; Requires sets and alists libraries.

\end{verbatim}
\noindent{\sc Event}:   Start with the library {\tt{"alists"}}.

\addvspace{18pt}

\begin{verbatim};; 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};; Later we may wish to prove correctness of one-way-unify
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{instance} \\  
\=\+{\rm{instance}}\,({\it{flg\/}}, {\it{term1\/}}, {\it{term2\/}})\index{instance} \\ 
$\leftrightarrow$$\;\;\;\;$$\exists\;${\it{one-way-unifier\/}}$\;$(\=\+{\rm{var-substp}}\,({\it{one-way-unifier\/}})\index{var-substp} \\ 
$\wedge$$\;\;\;\;$({\it{term1\/}} $=$ {\rm{subst}}\,({\it{flg\/}}, {\it{one-way-unifier\/}}, {\it{term2\/}})\index{subst}))\-\index{exists}\-
\end{tabbing}

\begin{verbatim};;;;; 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}


\noindent{\sc Event}:   Disable instance.

\addvspace{18pt}
\begin{verbatim};;;(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: instance,
var-substp,
compose,
apply-to-subst,
subst,
nullify-subst.\index{substitution-defns}

\addvspace{18pt}


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

\addvspace{18pt}

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