\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.

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

\addvspace{18pt}

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


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

\addvspace{18pt}

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