\documentstyle[makeidx]{article}
\makeindex
%\setlength{\oddsidemargin}{.5in}
%\setlength{\evensidemargin}{.5in}
%\setlength{\textwidth}{5.8in}
\begin{document}
%\setlength{\parindent}{0pt}
%\newcounter{bean}
%\begin{list}{\arabic{bean}.}{\usecounter{bean}\setlength{\leftmargin}{0pt}\setlength{\rightmargin}{0pt}\setlength{\listparindent}{20pt}\setlength{\parsep}{5pt}}
%\item[]


\noindent{\sc Event}:   Start with the library {\tt{"c3"}}.

\addvspace{18pt}
\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                           ;;
;;                    %CORRESPONDENCE BETWEEN MG AND P                       ;;
;;                                                                           ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{mg-to-p-simple-literal} \\  
\=\+{\rm{mg-to-p-simple-literal}}\,({\it{lit\/}})\index{mg-to-p-simple-literal} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{int-literalp}}\,({\it{lit\/}})\index{int-literalp}$\;\;${\bf then }{\rm{list}}\,({\tt{'}}{\tt{int}}, {\rm{cadr}}\,({\it{lit\/}})) \\ 
{\bf elseif }{\rm{boolean-literalp}}\,({\it{lit\/}})\index{boolean-literalp} \\ 
{\bf then }\=\+{\bf if }{\rm{cadr}}\,({\it{lit\/}}) $=$ {\tt{'}}{\tt{false-mg}}$\;\;${\bf then }{\rm{list}}\,({\tt{'}}{\tt{bool}}, {\tt{'}}{\tt{f}}) \\ 
{\bf else }{\rm{list}}\,({\tt{'}}{\tt{bool}}, {\tt{'}}{\tt{t}})$\;${\bf  endif}\- \\ 
{\bf elseif }{\rm{character-literalp}}\,({\it{lit\/}})\index{character-literalp}$\;\;${\bf then }{\rm{list}}\,({\tt{'}}{\tt{int}}, {\rm{cadr}}\,({\it{lit\/}})) \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable mg-to-p-simple-literal.

\addvspace{18pt}

\begin{verbatim};; An array value is a list of simple mg literals.  Recall that in the most common
;; case, the values will be reversed because they will be in contiguous locations 
;; on the stack, which is indexed from the bottom.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{mg-to-p-simple-literal-list} \\  
\=\+{\rm{mg-to-p-simple-literal-list}}\,({\it{lst\/}})\index{mg-to-p-simple-literal-list} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{lst\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{cons}}\,(\=\+{\rm{mg-to-p-simple-literal}}\,({\rm{car}}\,({\it{lst\/}}))\index{mg-to-p-simple-literal}, \\ 
{\rm{mg-to-p-simple-literal-list}}\,({\rm{cdr}}\,({\it{lst\/}}))\index{mg-to-p-simple-literal-list})\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mg-to-p-simple-literal-list-plistp \\ \index{mg-to-p-simple-literal-list-pli!stp}
{\rm{plistp}}\,({\rm{mg-to-p-simple-literal-list}}\,({\it{x\/}})\index{mg-to-p-simple-literal-list})\index{plistp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  length-mg-to-p-simple-literal-list \\ \index{length-mg-to-p-simple-literal-li!st}
{\rm{length}}\,({\rm{mg-to-p-simple-literal-list}}\,({\it{x\/}})\index{mg-to-p-simple-literal-list})\index{length} $=$ {\rm{length}}\,({\it{x\/}})\index{length}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-to-mg-simple-literal} \\  
\=\+{\rm{p-to-mg-simple-literal}}\,({\it{lit\/}}, {\it{typespec\/}})\index{p-to-mg-simple-literal} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{typespec\/}} $=$ {\tt{'}}{\tt{int-mg}}$\;\;${\bf then }{\rm{list}}\,({\tt{'}}{\tt{int-mg}}, {\rm{cadr}}\,({\it{lit\/}})) \\ 
{\bf elseif }{\it{typespec\/}} $=$ {\tt{'}}{\tt{boolean-mg}} \\ 
{\bf then }{\rm{list}}\,(\=\+{\tt{'}}{\tt{boolean-mg}}, \\ 
\=\+{\bf if }{\rm{cadr}}\,({\it{lit\/}}) $=$ {\tt{'}}{\tt{f}}$\;\;${\bf then }{\tt{'}}{\tt{false-mg}} \\ 
{\bf else }{\tt{'}}{\tt{true-mg}}$\;${\bf  endif}\-)\- \\ 
{\bf else }{\rm{list}}\,({\tt{'}}{\tt{character-mg}}, {\rm{cadr}}\,({\it{lit\/}}))$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-to-mg-simple-literal-list} \\  
\=\+{\rm{p-to-mg-simple-literal-list}}\,({\it{lst\/}}, {\it{typespec\/}})\index{p-to-mg-simple-literal-list} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{lst\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{cons}}\,(\=\+{\rm{p-to-mg-simple-literal}}\,({\rm{car}}\,({\it{lst\/}}), {\it{typespec\/}})\index{p-to-mg-simple-literal}, \\ 
{\rm{p-to-mg-simple-literal-list}}\,({\rm{cdr}}\,({\it{lst\/}}), {\it{typespec\/}})\index{p-to-mg-simple-literal-list})\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  p-to-mg-to-p-simple-literal \\ \index{p-to-mg-to-p-simple-literal}
\=\+{\rm{simple-typed-literalp}}\,({\it{lit\/}}, {\it{typespec\/}})\index{simple-typed-literalp} \\ 
$\rightarrow$$\;\;\;\;$({\rm{p-to-mg-simple-literal}}\,({\rm{mg-to-p-simple-literal}}\,({\it{lit\/}})\index{mg-to-p-simple-literal}, {\it{typespec\/}})\index{p-to-mg-simple-literal} $=$ {\it{lit\/}})\-
\end{tabbing}


\noindent{\sc Event}:   Disable p-to-mg-to-p-simple-literal.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  p-to-mg-to-p-simple-literal-list \\ \index{p-to-mg-to-p-simple-literal-list}
\=\+{\rm{simple-typed-literal-plistp}}\,({\it{lst\/}}, {\it{type\/}})\index{simple-typed-literal-plistp} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{p-to-mg-simple-literal-list}}\,({\rm{mg-to-p-simple-literal-list}}\,({\it{lst\/}})\index{mg-to-p-simple-literal-list}, {\it{type\/}})\index{p-to-mg-simple-literal-list} \\ 
$=$$\;\;\;\;${\it{lst\/}})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable p-to-mg-to-p-simple-literal-list.

\addvspace{18pt}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                    ;;
;;                        %Mapping Conditions                         ;;
;;                                                                    ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Each MG condition in the state is translated to a natural in the 
;; Piton state.  This is done by finding it's index in the cond-list,
;; except for 'normal, 'routineerror, 'leave, and 'timed-out which are computed
;; directly.

;; The assumption in the Piton world is that there is always an operative list of
;; conditions (which is really (append formal-conds local-conds) of the procedure
;; definition.  The Piton condition stored is the index of the MG condition into
;; this list.  However, there are potential conditions which are not in this list also.
;; These are 'timed-out, 'leave, 'routineerror, and 'normal and are computed specially.
;; These result is a Piton natural.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{condition-index} \\  
\=\+{\rm{condition-index}}\,({\it{cond\/}}, {\it{cond-list\/}})\index{condition-index} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{cond\/}} $=$ {\tt{'}}{\tt{leave}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{cond\/}} $=$ {\tt{'}}{\tt{routineerror}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{cond\/}} $=$ {\tt{'}}{\tt{normal}}$\;\;${\bf then }{\tt{2}} \\ 
{\bf else }$1\;+$ ($1\;+$ {\rm{index}}\,({\it{cond\/}}, {\it{cond-list\/}})\index{index})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  condition-index-append \\ \index{condition-index-append}
\=\+({\it{cc\/}} $\in$ {\it{lst1\/}}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{condition-index}}\,({\it{cc\/}}, {\rm{append}}\,({\it{lst1\/}}, {\it{lst2\/}}))\index{condition-index} $=$ {\rm{condition-index}}\,({\it{cc\/}}, {\it{lst1\/}})\index{condition-index})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  condition-index-append2 \\ \index{condition-index-append2}
\=\+(({\it{cc\/}} $\not\in$ {\it{lst1\/}}) $\wedge$ ({\it{cc\/}} $\not\in$ {\tt{'}}{\tt{(}}{\tt{normal}}{\tt{ }}{\tt{routineerror}}{\tt{ }}{\tt{leave}}{\tt{)}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{condition-index}}\,({\it{cc\/}}, {\rm{append}}\,({\it{lst1\/}}, {\it{lst2\/}}))\index{condition-index} \\ 
$=$$\;\;\;\;$({\rm{length}}\,({\it{lst1\/}})\index{length} $+$ {\rm{condition-index}}\,({\it{cc\/}}, {\it{lst2\/}})\index{condition-index}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{mg-cond-to-p-nat} \\  
{\rm{mg-cond-to-p-nat}}\,({\it{c\/}}, {\it{cond-list\/}})\index{mg-cond-to-p-nat} $=$ {\rm{list}}\,({\tt{'}}{\tt{nat}}, {\rm{condition-index}}\,({\it{c\/}}, {\it{cond-list\/}})\index{condition-index})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-nat-to-mg-cond} \\  
\=\+{\rm{p-nat-to-mg-cond}}\,({\it{p-nat\/}}, {\it{cond-list\/}})\index{p-nat-to-mg-cond} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{p-nat\/}} $=$ {\tt{'}}{\tt{(}}{\tt{nat}}{\tt{ }}{\tt{0}}{\tt{)}}$\;\;${\bf then }{\tt{'}}{\tt{leave}} \\ 
{\bf elseif }{\it{p-nat\/}} $=$ {\tt{'}}{\tt{(}}{\tt{nat}}{\tt{ }}{\tt{1}}{\tt{)}}$\;\;${\bf then }{\tt{'}}{\tt{routineerror}} \\ 
{\bf elseif }{\it{p-nat\/}} $=$ {\tt{'}}{\tt{(}}{\tt{nat}}{\tt{ }}{\tt{2}}{\tt{)}}$\;\;${\bf then }{\tt{'}}{\tt{normal}} \\ 
{\bf else }{\rm{car}}\,({\rm{nth}}\,({\it{cond-list\/}}, (({\rm{cadr}}\,({\it{p-nat\/}}) $-\;1$) $-\;1$) $-\;1$)\index{nth})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  condition-mapping-inverts \\ \index{condition-mapping-inverts}
\=\+{\rm{ok-cc}}\,({\it{c\/}}, {\it{cond-list\/}})\index{ok-cc} \\ 
$\rightarrow$$\;\;\;\;$({\rm{p-nat-to-mg-cond}}\,({\rm{mg-cond-to-p-nat}}\,({\it{c\/}}, {\it{cond-list\/}})\index{mg-cond-to-p-nat}, {\it{cond-list\/}})\index{p-nat-to-mg-cond} $=$ {\it{c\/}})\-
\end{tabbing}


\noindent{\sc Event}:   Disable condition-mapping-inverts.

\addvspace{18pt}


\noindent{\sc Event}:   Disable mg-cond-to-p-nat.

\addvspace{18pt}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                    ;;
;;                     %Depositing Array Values                       ;;
;;                                                                    ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; The hypothesis will be that each of the locals in bindings contains an address into the 
;; temp-stk.  This takes the values of the mg variables and puts them into those locations.

;; Given the values-list for an array, this maps them into successive values in the 
;; temp-stk starting at index nat.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{deposit-temp} \\  
{\rm{deposit-temp}}\,({\it{val\/}}, {\it{nat\/}}, {\it{temp-stk\/}})\index{deposit-temp} $=$ {\rm{rput}}\,({\it{val\/}}, {\rm{untag}}\,({\it{nat\/}})\index{untag}, {\it{temp-stk\/}})\index{rput}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{fetch-temp} \\  
{\rm{fetch-temp}}\,({\it{nat\/}}, {\it{temp-stk\/}})\index{fetch-temp} $=$ {\rm{rget}}\,({\rm{untag}}\,({\it{nat\/}})\index{untag}, {\it{temp-stk\/}})\index{rget}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  deposit-temp-preserves-length \\ \index{deposit-temp-preserves-length}
({\rm{untag}}\,({\it{y\/}})\index{untag} $<$ {\rm{length}}\,({\it{z\/}})\index{length}) $\rightarrow$ ({\rm{length}}\,({\rm{deposit-temp}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{deposit-temp})\index{length} $=$ {\rm{length}}\,({\it{z\/}})\index{length})
\end{tabbing}


\noindent{\sc Event}:   Disable deposit-temp.

\addvspace{18pt}

\noindent{\sc Event}:   Disable fetch-temp.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{fetch-n-temp-stk-elements} \\  
\=\+{\rm{fetch-n-temp-stk-elements}}\,({\it{temp-stk\/}}, {\it{nat\/}}, {\it{n\/}})\index{fetch-n-temp-stk-elements} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{cons}}\,(\=\+{\rm{fetch-temp}}\,({\it{nat\/}}, {\it{temp-stk\/}})\index{fetch-temp}, \\ 
{\rm{fetch-n-temp-stk-elements}}\,(\=\+{\it{temp-stk\/}}, \\ 
{\rm{add1-nat}}\,({\it{nat\/}})\index{add1-nat}, \\ 
{\it{n\/}} $-\;1$)\-\index{fetch-n-temp-stk-elements})\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{deposit-array-value} \\  
\=\+{\rm{deposit-array-value}}\,({\it{lit-list\/}}, {\it{nat\/}}, {\it{temp-stk\/}})\index{deposit-array-value} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{lit-list\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\it{temp-stk\/}} \\ 
{\bf else }{\rm{deposit-array-value}}\,(\=\+{\rm{cdr}}\,({\it{lit-list\/}}), \\ 
{\rm{add1-nat}}\,({\it{nat\/}})\index{add1-nat}, \\ 
{\rm{deposit-temp}}\,(\=\+{\rm{mg-to-p-simple-literal}}\,({\rm{car}}\,({\it{lit-list\/}}))\index{mg-to-p-simple-literal}, \\ 
{\it{nat\/}}, \\ 
{\it{temp-stk\/}})\-\index{deposit-temp})\-\index{deposit-array-value}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{deposit-alist-value} \\  
\=\+{\rm{deposit-alist-value}}\,({\it{mg-alist-element\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{deposit-alist-value} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{simple-mg-type-refp}}\,({\rm{m-type}}\,({\it{mg-alist-element\/}})\index{m-type})\index{simple-mg-type-refp} \\ 
{\bf then }{\rm{deposit-temp}}\,(\=\+{\rm{mg-to-p-simple-literal}}\,({\rm{m-value}}\,({\it{mg-alist-element\/}})\index{m-value})\index{mg-to-p-simple-literal}, \\ 
{\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{mg-alist-element\/}}), {\it{bindings\/}})), \\ 
{\it{temp-stk\/}})\-\index{deposit-temp} \\ 
{\bf else }{\rm{deposit-array-value}}\,(\=\+{\rm{m-value}}\,({\it{mg-alist-element\/}})\index{m-value}, \\ 
{\rm{cdr}}\,({\rm{assoc}}\,(\=\+{\rm{car}}\,({\it{mg-alist-element\/}}), \\ 
{\it{bindings\/}})\-), \\ 
{\it{temp-stk\/}})\-\index{deposit-array-value}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{map-down-values} \\  
\=\+{\rm{map-down-values}}\,({\it{mg-alist\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{map-down-values} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{mg-alist\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\it{temp-stk\/}} \\ 
{\bf else }{\rm{map-down-values}}\,(\=\+{\rm{cdr}}\,({\it{mg-alist\/}}), \\ 
{\it{bindings\/}}, \\ 
{\rm{deposit-alist-value}}\,(\=\+{\rm{car}}\,({\it{mg-alist\/}}), \\ 
{\it{bindings\/}}, \\ 
{\it{temp-stk\/}})\-\index{deposit-alist-value})\-\index{map-down-values}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  map-down-values-distributes \\ \index{map-down-values-distributes}
\=\+{\rm{map-down-values}}\,({\rm{append}}\,({\it{lst1\/}}, {\it{lst2\/}}), {\it{bindings\/}}, {\it{temp-stk\/}})\index{map-down-values} \\ 
$=$$\;\;\;\;${\rm{map-down-values}}\,({\it{lst2\/}}, {\it{bindings\/}}, {\rm{map-down-values}}\,({\it{lst1\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{map-down-values})\index{map-down-values}\-
\end{tabbing}


\noindent{\sc Event}:   Disable map-down-values-distributes.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  deposit-array-value-preserves-plistp \\ \index{deposit-array-value-preserves-p!listp}
{\rm{plistp}}\,({\it{temp-stk\/}})\index{plistp} $\rightarrow$ {\rm{plistp}}\,({\rm{deposit-array-value}}\,({\it{lst\/}}, {\it{nat\/}}, {\it{temp-stk\/}})\index{deposit-array-value})\index{plistp}
\end{tabbing}


\noindent{\sc Event}:   Disable deposit-array-value-preserves-plistp.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  map-down-values-preserves-plistp \\ \index{map-down-values-preserves-plistp}
{\rm{plistp}}\,({\it{temp-stk\/}})\index{plistp} $\rightarrow$ {\rm{plistp}}\,({\rm{map-down-values}}\,({\it{alist\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{map-down-values})\index{plistp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  extra-bindings-dont-affect-deposit-alist-value \\ \index{extra-bindings-dont-affect-depo!sit-alist-value}
\=\+({\rm{car}}\,({\it{x\/}}) $\not\in$ {\rm{listcars}}\,({\it{bindings1\/}})\index{listcars}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{deposit-alist-value}}\,({\it{x\/}}, {\rm{append}}\,({\it{bindings1\/}}, {\it{bindings2\/}}), {\it{temp-stk\/}})\index{deposit-alist-value} \\ 
$=$$\;\;\;\;${\rm{deposit-alist-value}}\,({\it{x\/}}, {\it{bindings2\/}}, {\it{temp-stk\/}})\index{deposit-alist-value})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  deposit-alist-value-not-affected-by-extra-element \\ \index{deposit-alist-value-not-affecte!d-by-extra-element}
\=\+({\rm{car}}\,({\it{y\/}}) $\not=$ {\rm{car}}\,({\it{x\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{deposit-alist-value}}\,({\it{y\/}}, {\rm{append}}\,({\it{lst1\/}}, {\rm{cons}}\,({\it{x\/}}, {\it{lst2\/}})), {\it{temp-stk\/}})\index{deposit-alist-value} \\ 
$=$$\;\;\;\;${\rm{deposit-alist-value}}\,({\it{y\/}}, {\rm{append}}\,({\it{lst1\/}}, {\it{lst2\/}}), {\it{temp-stk\/}})\index{deposit-alist-value})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  deposit-alist-value-not-affected-by-extra-element2 \\ \index{deposit-alist-value-not-affecte!d-by-extra-element2}
\=\+({\rm{car}}\,({\it{y\/}}) $\not=$ {\rm{car}}\,({\it{x\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{deposit-alist-value}}\,({\it{y\/}}, {\rm{cons}}\,({\it{x\/}}, {\it{lst2\/}}), {\it{temp-stk\/}})\index{deposit-alist-value} \\ 
$=$$\;\;\;\;${\rm{deposit-alist-value}}\,({\it{y\/}}, {\it{lst2\/}}, {\it{temp-stk\/}})\index{deposit-alist-value})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  map-down-values-not-affected-by-extra-binding \\ \index{map-down-values-not-affected-by!-extra-binding}
\=\+({\rm{car}}\,({\it{x\/}}) $\not\in$ {\rm{listcars}}\,({\it{lst\/}})\index{listcars}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{map-down-values}}\,({\it{lst\/}}, {\rm{append}}\,({\it{lst1\/}}, {\rm{cons}}\,({\it{x\/}}, {\it{lst2\/}})), {\it{temp-stk\/}})\index{map-down-values} \\ 
$=$$\;\;\;\;${\rm{map-down-values}}\,({\it{lst\/}}, {\rm{append}}\,({\it{lst1\/}}, {\it{lst2\/}}), {\it{temp-stk\/}})\index{map-down-values})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  new-binding-doesnt-disturb-map-down-values \\ \index{new-binding-doesnt-disturb-map-!down-values}
\=\+({\rm{car}}\,({\it{x\/}}) $\not\in$ {\rm{listcars}}\,({\it{lst1\/}})\index{listcars}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{map-down-values}}\,({\it{lst1\/}}, {\rm{cons}}\,({\it{x\/}}, {\it{bindings\/}}), {\it{temp-stk\/}})\index{map-down-values} \\ 
$=$$\;\;\;\;${\rm{map-down-values}}\,({\it{lst1\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{map-down-values})\-\-
\end{tabbing}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                    ;;
;;                       %Ok-Temp-Stk-Index                           ;;
;;                                                                    ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{ok-temp-stk-index} \\  
\=\+{\rm{ok-temp-stk-index}}\,({\it{nat\/}}, {\it{temp-stk\/}})\index{ok-temp-stk-index} \\ 
$=$$\;\;\;\;$(\=\+{\rm{length-plistp}}\,({\it{nat\/}}, {\tt{2}})\index{length-plistp} \\ 
$\wedge$$\;\;\;\;$({\rm{type}}\,({\it{nat\/}})\index{type} $=$ {\tt{'}}{\tt{nat}}) \\ 
$\wedge$$\;\;\;\;$({\rm{untag}}\,({\it{nat\/}})\index{untag} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\rm{untag}}\,({\it{nat\/}})\index{untag} $<$ {\rm{length}}\,({\it{temp-stk\/}})\index{length}))\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable ok-temp-stk-index.

\addvspace{18pt}

\begin{verbatim};; This in the hyps says that each of the piton local names in the piton bindings
;; points to a slot in temp-stk.  It DOESNT say that the value is the right one.
;; The function map-down-values puts the right value at that spot.  

;; This needs to also talk about the array case; the length of the temp-stk should be
;; such that not only is the temp-stk-index in the right range, but so are all of the 
;; indices of the array elements.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{ok-temp-stk-array-index} \\  
\=\+{\rm{ok-temp-stk-array-index}}\,({\it{nat\/}}, {\it{temp-stk\/}}, {\it{lngth\/}})\index{ok-temp-stk-array-index} \\ 
$=$$\;\;\;\;$(\=\+{\rm{length-plistp}}\,({\it{nat\/}}, {\tt{2}})\index{length-plistp} \\ 
$\wedge$$\;\;\;\;$({\rm{type}}\,({\it{nat\/}})\index{type} $=$ {\tt{'}}{\tt{nat}}) \\ 
$\wedge$$\;\;\;\;$({\rm{untag}}\,({\it{nat\/}})\index{untag} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$(({\rm{untag}}\,({\it{nat\/}})\index{untag} $+$ ({\it{lngth\/}} $-\;1$)) $<$ {\rm{length}}\,({\it{temp-stk\/}})\index{length}))\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable ok-temp-stk-array-index.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  ok-temp-stk-index-sensitive-to-length \\ \index{ok-temp-stk-index-sensitive-to-!length}
\=\+(\=\+{\rm{ok-temp-stk-index}}\,({\it{x\/}}, {\it{temp-stk1\/}})\index{ok-temp-stk-index} \\ 
$\wedge$$\;\;\;\;$({\rm{length}}\,({\it{temp-stk2\/}})\index{length} $\not<$ {\rm{length}}\,({\it{temp-stk1\/}})\index{length}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{ok-temp-stk-index}}\,({\it{x\/}}, {\it{temp-stk2\/}})\index{ok-temp-stk-index}\-
\end{tabbing}


\noindent{\sc Event}:   Disable ok-temp-stk-index-sensitive-to-length.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  ok-temp-stk-array-index-sensitive-to-length \\ \index{ok-temp-stk-array-index-sensitive!-to-length}
\=\+(\=\+{\rm{ok-temp-stk-array-index}}\,({\it{x\/}}, {\it{temp-stk1\/}}, {\it{n\/}})\index{ok-temp-stk-array-index} \\ 
$\wedge$$\;\;\;\;$({\rm{length}}\,({\it{temp-stk2\/}})\index{length} $\not<$ {\rm{length}}\,({\it{temp-stk1\/}})\index{length}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{ok-temp-stk-array-index}}\,({\it{x\/}}, {\it{temp-stk2\/}}, {\it{n\/}})\index{ok-temp-stk-array-index}\-
\end{tabbing}


\noindent{\sc Event}:   Disable ok-temp-stk-array-index-sensitive-to-length.

\addvspace{18pt}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                    ;;
;;             %Operations Preserve Temp-Stk Length                   ;;
;;                                                                    ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

\end{verbatim}\begin{tabbing}{\sc Theorem}:  deposit-temp-never-shrinks \\ \index{deposit-temp-never-shrinks}
({\rm{length}}\,({\rm{deposit-temp}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{deposit-temp})\index{length} $<$ {\rm{length}}\,({\it{z\/}})\index{length}) $=$ {\bf{f}}
\end{tabbing}


\noindent{\sc Event}:   Disable deposit-temp-never-shrinks.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  lessp-transitive2 \\ \index{lessp-transitive2}
(({\it{x\/}} $\not<$ {\it{y\/}}) $\wedge$ ({\it{y\/}} $\not<$ {\it{z\/}})) $\rightarrow$ (({\it{x\/}} $<$ {\it{z\/}}) $=$ {\bf{f}})
\end{tabbing}


\noindent{\sc Event}:   Disable lessp-transitive2.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  deposit-array-value-never-shrinks \\ \index{deposit-array-value-never-shrin!ks}
({\rm{length}}\,({\rm{deposit-array-value}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{deposit-array-value})\index{length} $<$ {\rm{length}}\,({\it{z\/}})\index{length}) $=$ {\bf{f}}
\end{tabbing}


\noindent{\sc Event}:   Disable deposit-array-value-never-shrinks.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  deposit-alist-value-never-shrinks \\ \index{deposit-alist-value-never-shrin!ks}
\=\+({\rm{length}}\,({\rm{deposit-alist-value}}\,({\it{y\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{deposit-alist-value})\index{length} $<$ {\rm{length}}\,({\it{temp-stk\/}})\index{length}) \\ 
$=$$\;\;\;\;${\bf{f}}\-
\end{tabbing}


\noindent{\sc Event}:   Disable deposit-alist-value-never-shrinks.

\addvspace{18pt}


\noindent{\sc Event}:   Disable deposit-alist-value.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  deposit-alist-value-never-shrinks2 \\ \index{deposit-alist-value-never-shrin!ks2}
\=\+({\it{u\/}} $<$ {\rm{length}}\,({\it{temp-stk\/}})\index{length}) \\ 
$\rightarrow$$\;\;\;\;$(({\it{u\/}} $<$ {\rm{length}}\,({\rm{deposit-alist-value}}\,({\it{y\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{deposit-alist-value})\index{length}) $=$ {\bf{t}})\-
\end{tabbing}


\noindent{\sc Event}:   Disable deposit-alist-value-never-shrinks2.

\addvspace{18pt}


\begin{tabbing}{\sc Theorem}:  map-down-values-never-shrinks \\ \index{map-down-values-never-shrinks}
({\rm{length}}\,({\rm{map-down-values}}\,({\it{y\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{map-down-values})\index{length} $<$ {\rm{length}}\,({\it{temp-stk\/}})\index{length}) $=$ {\bf{f}}
\end{tabbing}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                    ;;
;;                     %Mg-vars-ok-in-p-state                         ;;
;;                                                                    ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{mg-var-ok-in-p-state} \\  
\=\+{\rm{mg-var-ok-in-p-state}}\,({\it{mg-var\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-var-ok-in-p-state} \\ 
$=$$\;\;\;\;$(\=\+{\rm{definedp}}\,({\rm{car}}\,({\it{mg-var\/}}), {\it{bindings\/}})\index{definedp} \\ 
$\wedge$$\;\;\;\;$\=\+{\bf if }{\rm{simple-mg-type-refp}}\,({\rm{m-type}}\,({\it{mg-var\/}})\index{m-type})\index{simple-mg-type-refp} \\ 
{\bf then }{\rm{ok-temp-stk-index}}\,(\=\+{\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{mg-var\/}}), {\it{bindings\/}})), \\ 
{\it{temp-stk\/}})\-\index{ok-temp-stk-index} \\ 
{\bf else }{\rm{ok-temp-stk-array-index}}\,(\=\+{\rm{cdr}}\,({\rm{assoc}}\,(\=\+{\rm{car}}\,({\it{mg-var\/}}), \\ 
{\it{bindings\/}})\-), \\ 
{\it{temp-stk\/}}, \\ 
{\rm{array-length}}\,({\rm{m-type}}\,({\it{mg-var\/}})\index{m-type})\index{array-length})\-\index{ok-temp-stk-array-index}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{mg-vars-list-ok-in-p-state} \\  
\=\+{\rm{mg-vars-list-ok-in-p-state}}\,({\it{mg-vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{mg-vars\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }\=\+{\rm{mg-var-ok-in-p-state}}\,({\rm{car}}\,({\it{mg-vars\/}}), {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-var-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,(\=\+{\rm{cdr}}\,({\it{mg-vars\/}}), \\ 
{\it{bindings\/}}, \\ 
{\it{temp-stk\/}})\-\index{mg-vars-list-ok-in-p-state}\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mg-vars-list-ok-in-p-state-cdr \\ \index{mg-vars-list-ok-in-p-state-cdr}
\=\+({\rm{mg-vars-list-ok-in-p-state}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{mg-vars-list-ok-in-p-state} $\wedge$ {\rm{listp}}\,({\it{x\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\rm{cdr}}\,({\it{x\/}}), {\it{y\/}}, {\it{z\/}})\index{mg-vars-list-ok-in-p-state}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mg-var-ok-temp-stk-index \\ \index{mg-var-ok-temp-stk-index}
\=\+({\rm{mg-vars-list-ok-in-p-state}}\,({\it{lst\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} $\wedge$ {\rm{definedp}}\,({\it{b\/}}, {\it{lst\/}})\index{definedp}) \\ 
$\rightarrow$$\;\;\;\;$(({\rm{untag}}\,({\rm{value}}\,({\it{b\/}}, {\it{bindings\/}})\index{value})\index{untag} $<$ {\rm{length}}\,({\it{temp-stk\/}})\index{length}) $=$ {\bf{t}})\-
\end{tabbing}


\noindent{\sc Event}:   Disable mg-var-ok-temp-stk-index.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  mg-vars-list-ok-in-p-state-distributes \\ \index{mg-vars-list-ok-in-p-state-dist!ributes}
\=\+{\rm{mg-vars-list-ok-in-p-state}}\,({\rm{append}}\,({\it{lst1\/}}, {\it{lst2\/}}), {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$=$$\;\;\;\;$(\=\+{\rm{mg-vars-list-ok-in-p-state}}\,({\it{lst1\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{lst2\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mg-vars-list-ok-reorder-cars \\ \index{mg-vars-list-ok-reorder-cars}
\=\+{\rm{mg-vars-list-ok-in-p-state}}\,({\rm{cons}}\,({\it{x\/}}, {\rm{cons}}\,({\it{y\/}}, {\it{lst\/}})), {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\rightarrow$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\rm{cons}}\,({\it{y\/}}, {\rm{cons}}\,({\it{x\/}}, {\it{lst\/}})), {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mg-vars-list-ok-strip-off-car \\ \index{mg-vars-list-ok-strip-off-car}
\=\+({\rm{car}}\,({\it{x\/}}) $\not\in$ {\rm{listcars}}\,({\it{lst1\/}})\index{listcars}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{mg-vars-list-ok-in-p-state}}\,({\it{lst1\/}}, {\rm{cons}}\,({\it{x\/}}, {\it{lst2\/}}), {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$=$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{lst1\/}}, {\it{lst2\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable mg-vars-list-ok-strip-off-car.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  mg-vars-list-ok-sensitive-to-temp-stk-length2 \\ \index{mg-vars-list-ok-sensitive-to-te!mp-stk-length2}
\=\+(\=\+({\rm{length}}\,({\it{temp-stk2\/}})\index{length} $\not<$ {\rm{length}}\,({\it{temp-stk1\/}})\index{length}) \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{alist\/}}, {\it{bindings\/}}, {\it{temp-stk1\/}})\index{mg-vars-list-ok-in-p-state})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{alist\/}}, {\it{bindings\/}}, {\it{temp-stk2\/}})\index{mg-vars-list-ok-in-p-state}\-
\end{tabbing}


\noindent{\sc Event}:   Disable mg-vars-list-ok-sensitive-to-temp-stk-length2.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  append-bindings-doesnt-affect-mg-vars-list-ok \\ \index{append-bindings-doesnt-affect-m!g-vars-list-ok}
\=\+{\rm{mg-vars-list-ok-in-p-state}}\,({\it{alist\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\rightarrow$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{alist\/}}, {\rm{append}}\,({\it{bindings\/}}, {\it{lst\/}}), {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state}\-
\end{tabbing}


\noindent{\sc Event}:   Disable append-bindings-doesnt-affect-mg-vars-list-ok.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  append-bindings-left-doesnt-affect-mg-vars-list-ok \\ \index{append-bindings-left-doesnt-affe!ct-mg-vars-list-ok}
\=\+(\=\+{\rm{mg-vars-list-ok-in-p-state}}\,({\it{alist\/}}, {\it{bindings2\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{append}}\,({\it{bindings1\/}}, {\it{bindings2\/}}))\index{all-cars-unique})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{alist\/}}, {\rm{append}}\,({\it{bindings1\/}}, {\it{bindings2\/}}), {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mg-vars-list-members-ok-vars \\ \index{mg-vars-list-members-ok-vars}
\=\+({\rm{mg-vars-list-ok-in-p-state}}\,({\it{alist\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} $\wedge$ ({\it{x\/}} $\in$ {\it{alist\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{mg-var-ok-in-p-state}}\,({\it{x\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-var-ok-in-p-state}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mg-var-ok-value-lessp-length-temp-stk \\ \index{mg-var-ok-value-lessp-length-te!mp-stk}
\=\+({\rm{mg-vars-list-ok-in-p-state}}\,({\it{lst\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} $\wedge$ {\rm{definedp}}\,({\it{x\/}}, {\it{lst\/}})\index{definedp}) \\ 
$\rightarrow$$\;\;\;\;$(({\rm{untag}}\,({\rm{cdr}}\,({\rm{assoc}}\,({\it{x\/}}, {\it{bindings\/}})))\index{untag} $<$ {\rm{length}}\,({\it{temp-stk\/}})\index{length}) $=$ {\bf{t}})\-
\end{tabbing}


\noindent{\sc Event}:   Disable mg-var-ok-value-lessp-length-temp-stk.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  mg-var-ok-untag-value-numberp \\ \index{mg-var-ok-untag-value-numberp}
\=\+({\rm{mg-vars-list-ok-in-p-state}}\,({\it{lst\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} $\wedge$ {\rm{definedp}}\,({\it{x\/}}, {\it{lst\/}})\index{definedp}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{untag}}\,({\rm{cdr}}\,({\rm{assoc}}\,({\it{x\/}}, {\it{bindings\/}})))\index{untag} $\in\;${\bf{N}}${}$)\-
\end{tabbing}


\noindent{\sc Event}:   Disable mg-var-ok-untag-value-numberp.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  mg-var-ok-array-index-ok \\ \index{mg-var-ok-array-index-ok}
\=\+(\=\+{\rm{mg-vars-list-ok-in-p-state}}\,({\it{lst\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\it{lst\/}})\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;$({\it{y\/}} $\in$ {\it{lst\/}}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{simple-mg-type-refp}}\,({\rm{m-type}}\,({\it{y\/}})\index{m-type})\index{simple-mg-type-refp}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+({\rm{untag}}\,({\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{y\/}}), {\it{bindings\/}})))\index{untag} $+$ ({\rm{length}}\,({\rm{caddr}}\,({\it{y\/}}))\index{length} $-\;1$)) \\ 
$<$$\;\;\;\;${\rm{length}}\,({\it{temp-stk\/}})\index{length})\- \\ 
$=$$\;\;\;\;${\bf{t}})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable mg-var-ok-array-index-ok.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  mg-var-ok-array-index-ok2 \\ \index{mg-var-ok-array-index-ok2}
\=\+(\=\+{\rm{mg-vars-list-ok-in-p-state}}\,({\it{lst\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\it{lst\/}})\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;$({\it{y\/}} $\in$ {\it{lst\/}}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{simple-mg-type-refp}}\,({\rm{m-type}}\,({\it{y\/}})\index{m-type})\index{simple-mg-type-refp}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+({\rm{untag}}\,({\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{y\/}}), {\it{bindings\/}})))\index{untag} $+$ ({\rm{array-length}}\,({\rm{cadr}}\,({\it{y\/}}))\index{array-length} $-\;1$)) \\ 
$<$$\;\;\;\;${\rm{length}}\,({\it{temp-stk\/}})\index{length})\- \\ 
$=$$\;\;\;\;${\bf{t}})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable mg-var-ok-array-index-ok2.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  deposit-alist-value-preserves-mg-vars-list-ok \\ \index{deposit-alist-value-preserves-m!g-vars-list-ok}
\=\+{\rm{mg-vars-list-ok-in-p-state}}\,({\rm{cons}}\,({\it{x\/}}, {\it{lst\/}}), {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\rightarrow$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,(\=\+{\it{lst\/}}, \\ 
{\it{bindings\/}}, \\ 
{\rm{deposit-alist-value}}\,({\it{x\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{deposit-alist-value})\-\index{mg-vars-list-ok-in-p-state}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  deposit-array-value-preserves-length \\ \index{deposit-array-value-preserves-le!ngth}
\=\+(({\rm{untag}}\,({\it{nat\/}})\index{untag} $+$ ({\rm{length}}\,({\it{value\/}})\index{length} $-\;1$)) $<$ {\rm{length}}\,({\it{temp-stk\/}})\index{length}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{length}}\,({\rm{deposit-array-value}}\,({\it{value\/}}, {\it{nat\/}}, {\it{temp-stk\/}})\index{deposit-array-value})\index{length} $=$ {\rm{length}}\,({\it{temp-stk\/}})\index{length})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member-array-lengths-match \\ \index{member-array-lengths-match}
\=\+({\rm{mg-alistp}}\,({\it{lst\/}})\index{mg-alistp} $\wedge$ ({\it{x\/}} $\in$ {\it{lst\/}}) $\wedge$ ($\neg$ {\rm{simple-mg-type-refp}}\,({\rm{m-type}}\,({\it{x\/}})\index{m-type})\index{simple-mg-type-refp})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{length}}\,({\rm{caddr}}\,({\it{x\/}}))\index{length} $=$ {\rm{array-length}}\,({\rm{cadr}}\,({\it{x\/}}))\index{array-length})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  array-index-lessp \\ \index{array-index-lessp}
\=\+(\=\+{\rm{mg-alistp}}\,({\it{lst\/}})\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\in$ {\it{lst\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{lst\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{simple-mg-type-refp}}\,({\rm{m-type}}\,({\it{x\/}})\index{m-type})\index{simple-mg-type-refp}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+({\rm{untag}}\,({\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{x\/}}), {\it{bindings\/}})))\index{untag} $+$ ({\rm{length}}\,({\rm{caddr}}\,({\it{x\/}}))\index{length} $-\;1$)) \\ 
$<$$\;\;\;\;${\rm{length}}\,({\it{temp-stk\/}})\index{length})\- \\ 
$=$$\;\;\;\;${\bf{t}})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  deposit-alist-value-preserves-length \\ \index{deposit-alist-value-preserves-le!ngth}
\=\+(\=\+{\rm{mg-alistp}}\,({\it{lst\/}})\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\in$ {\it{lst\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{lst\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{length}}\,({\rm{deposit-alist-value}}\,({\it{x\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{deposit-alist-value})\index{length} \\ 
$=$$\;\;\;\;${\rm{length}}\,({\it{temp-stk\/}})\index{length})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  map-down-values-preserves-length \\ \index{map-down-values-preserves-lengt!h}
\=\+({\rm{mg-vars-list-ok-in-p-state}}\,({\it{x\/}}, {\it{y\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} $\wedge$ {\rm{mg-alistp}}\,({\it{x\/}})\index{mg-alistp}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{length}}\,({\rm{map-down-values}}\,({\it{x\/}}, {\it{y\/}}, {\it{temp-stk\/}})\index{map-down-values})\index{length} $=$ {\rm{length}}\,({\it{temp-stk\/}})\index{length})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  deposit-temp-append1 \\ \index{deposit-temp-append1}
\=\+(({\rm{untag}}\,({\it{nat\/}})\index{untag} $\in\;${\bf{N}}${}$) $\wedge$ ({\rm{untag}}\,({\it{nat\/}})\index{untag} $<$ {\rm{length}}\,({\it{temp-stk\/}})\index{length})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{deposit-temp}}\,({\it{x\/}}, {\it{nat\/}}, {\rm{append}}\,({\it{lst\/}}, {\it{temp-stk\/}}))\index{deposit-temp} \\ 
$=$$\;\;\;\;${\rm{append}}\,({\it{lst\/}}, {\rm{deposit-temp}}\,({\it{x\/}}, {\it{nat\/}}, {\it{temp-stk\/}})\index{deposit-temp}))\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable deposit-temp-append1.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  deposit-temp-append \\ \index{deposit-temp-append}
\=\+(\=\+({\it{x\/}} $\in$ {\it{vars\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\it{x\/}}))\index{simple-mg-type-refp} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{deposit-temp}}\,({\it{value\/}}, {\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{x\/}}), {\it{bindings\/}})), {\rm{append}}\,({\it{lst\/}}, {\it{temp-stk\/}}))\index{deposit-temp} \\ 
$=$$\;\;\;\;${\rm{append}}\,(\=\+{\it{lst\/}}, \\ 
{\rm{deposit-temp}}\,(\=\+{\it{value\/}}, \\ 
{\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{x\/}}), {\it{bindings\/}})), \\ 
{\it{temp-stk\/}})\-\index{deposit-temp})\-)\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable deposit-temp-append.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  map-down-values-doesnt-affect-mg-vars-list-ok \\ \index{map-down-values-doesnt-affect-m!g-vars-list-ok}
\=\+(\=\+{\rm{mg-alistp}}\,({\it{u\/}})\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\it{x\/}})\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{u\/}}, {\it{v\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{x\/}}, {\it{y\/}}, {\rm{append}}\,({\it{lst1\/}}, {\it{temp-stk\/}}))\index{mg-vars-list-ok-in-p-state})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,(\=\+{\it{x\/}}, \\ 
{\it{y\/}}, \\ 
{\rm{append}}\,({\it{lst1\/}}, {\rm{map-down-values}}\,({\it{u\/}}, {\it{v\/}}, {\it{temp-stk\/}})\index{map-down-values}))\-\index{mg-vars-list-ok-in-p-state}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  signatures-match-preserves-mg-vars-list-ok \\ \index{signatures-match-preserves-mg-v!ars-list-ok}
\=\+({\rm{signatures-match}}\,({\it{x\/}}, {\it{y\/}})\index{signatures-match} $\wedge$ {\rm{mg-vars-list-ok-in-p-state}}\,({\it{x\/}}, {\it{z\/}}, {\it{w\/}})\index{mg-vars-list-ok-in-p-state}) \\ 
$\rightarrow$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{y\/}}, {\it{z\/}}, {\it{w\/}})\index{mg-vars-list-ok-in-p-state}\-
\end{tabbing}


\noindent{\sc Event}:   Disable signatures-match-preserves-mg-vars-list-ok.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  ok-temp-stk-simple-member \\ \index{ok-temp-stk-simple-member}
\=\+(\=\+{\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\rm{assoc}}\,({\it{x\/}}, {\it{mg-vars\/}})))\index{simple-mg-type-refp} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{mg-vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{ok-temp-stk-index}}\,({\rm{cdr}}\,({\rm{assoc}}\,({\it{x\/}}, {\it{bindings\/}})), {\it{temp-stk\/}})\index{ok-temp-stk-index}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ok-temp-stk-index-actual \\ \index{ok-temp-stk-index-actual}
\=\+(\=\+{\rm{listp}}\,({\it{formals\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{plistp}}\,({\it{mg-vars\/}})\index{plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-actual-params-list}}\,({\it{actuals\/}}, {\it{mg-vars\/}})\index{ok-actual-params-list} \\ 
$\wedge$$\;\;\;\;${\rm{data-param-lists-match}}\,({\it{actuals\/}}, {\it{formals\/}}, {\it{mg-vars\/}})\index{data-param-lists-match} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-formal-data-params-plistp}}\,({\it{formals\/}})\index{ok-mg-formal-data-params-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{mg-vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{simple-mg-type-refp}}\,({\rm{cadar}}\,({\it{formals\/}}))\index{simple-mg-type-refp})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{ok-temp-stk-index}}\,({\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{actuals\/}}), {\it{bindings\/}})), {\it{temp-stk\/}})\index{ok-temp-stk-index}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ok-temp-stk-array-simple-member \\ \index{ok-temp-stk-array-simple-member}
\=\+(\=\+{\rm{array-mg-type-refp}}\,({\rm{cadr}}\,({\rm{assoc}}\,({\it{x\/}}, {\it{mg-vars\/}})))\index{array-mg-type-refp} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{mg-vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{ok-temp-stk-array-index}}\,(\=\+{\rm{cdr}}\,({\rm{assoc}}\,({\it{x\/}}, {\it{bindings\/}})), \\ 
{\it{temp-stk\/}}, \\ 
{\rm{array-length}}\,({\rm{cadr}}\,({\rm{assoc}}\,({\it{x\/}}, {\it{mg-vars\/}})))\index{array-length})\-\index{ok-temp-stk-array-index}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ok-temp-stk-index-array-actual \\ \index{ok-temp-stk-index-array-actual}
\=\+(\=\+{\rm{listp}}\,({\it{formals\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{plistp}}\,({\it{mg-vars\/}})\index{plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-actual-params-list}}\,({\it{actuals\/}}, {\it{mg-vars\/}})\index{ok-actual-params-list} \\ 
$\wedge$$\;\;\;\;${\rm{data-param-lists-match}}\,({\it{actuals\/}}, {\it{formals\/}}, {\it{mg-vars\/}})\index{data-param-lists-match} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-formal-data-params-plistp}}\,({\it{formals\/}})\index{ok-mg-formal-data-params-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{mg-vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{simple-mg-type-refp}}\,({\rm{cadar}}\,({\it{formals\/}}))\index{simple-mg-type-refp}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{ok-temp-stk-array-index}}\,(\=\+{\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{actuals\/}}), {\it{bindings\/}})), \\ 
{\it{temp-stk\/}}, \\ 
{\rm{array-length}}\,({\rm{cadar}}\,({\it{formals\/}}))\index{array-length})\-\index{ok-temp-stk-array-index}\-
\end{tabbing}

\begin{verbatim};; %mg-vars-list-ok-in-p-state
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                    ;;
;;                      %N-Successive-Pointers                        ;;
;;                                                                    ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{n-successive-pointers} \\  
\=\+{\rm{n-successive-pointers}}\,({\it{nat\/}}, {\it{n\/}})\index{n-successive-pointers} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{cons}}\,({\rm{untag}}\,({\it{nat\/}})\index{untag}, {\rm{n-successive-pointers}}\,({\rm{add1-nat}}\,({\it{nat\/}})\index{add1-nat}, {\it{n\/}} $-\;1$)\index{n-successive-pointers})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  n-successive-pointers-plistp \\ \index{n-successive-pointers-plistp}
{\rm{plistp}}\,({\rm{n-successive-pointers}}\,({\it{nat\/}}, {\it{n\/}})\index{n-successive-pointers})\index{plistp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lesser-number-not-member-n-successive-pointers \\ \index{lesser-number-not-member-n-succe!ssive-pointers}
({\it{i\/}} $<$ {\rm{untag}}\,({\it{nat\/}})\index{untag}) $\rightarrow$ ({\it{i\/}} $\not\in$ {\rm{n-successive-pointers}}\,({\it{nat\/}}, {\it{n\/}})\index{n-successive-pointers})
\end{tabbing}
		
\begin{tabbing}{\sc Theorem}:  no-duplicates-successive-pointers \\ \index{no-duplicates-successive-pointe!rs}
({\rm{untag}}\,({\it{nat\/}})\index{untag} $\in\;${\bf{N}}${}$) $\rightarrow$ {\rm{no-duplicates}}\,({\rm{n-successive-pointers}}\,({\it{nat\/}}, {\it{n\/}})\index{n-successive-pointers})\index{no-duplicates}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  car-member-n-successive-pointers \\ \index{car-member-n-successive-pointer!s}
({\it{n\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ ({\rm{untag}}\,({\it{nat\/}})\index{untag} $\in$ {\rm{n-successive-pointers}}\,({\it{nat\/}}, {\it{n\/}})\index{n-successive-pointers})
\end{tabbing}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                    ;;
;;                        %Collect-Pointers                           ;;
;;                                                                    ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{collect-pointers} \\  
\=\+{\rm{collect-pointers}}\,({\it{bindings\/}}, {\it{alist\/}})\index{collect-pointers} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{alist\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf elseif }{\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\rm{car}}\,({\it{alist\/}})))\index{simple-mg-type-refp} \\ 
{\bf then }{\rm{cons}}\,(\=\+{\rm{untag}}\,({\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\rm{car}}\,({\it{alist\/}})), {\it{bindings\/}})))\index{untag}, \\ 
{\rm{collect-pointers}}\,({\it{bindings\/}}, {\rm{cdr}}\,({\it{alist\/}}))\index{collect-pointers})\- \\ 
{\bf else }{\rm{append}}\,(\=\+{\rm{n-successive-pointers}}\,(\=\+{\rm{cdr}}\,({\rm{assoc}}\,(\=\+{\rm{car}}\,({\rm{car}}\,({\it{alist\/}})), \\ 
{\it{bindings\/}})\-), \\ 
{\rm{array-length}}\,({\rm{cadr}}\,({\rm{car}}\,({\it{alist\/}})))\index{array-length})\-\index{n-successive-pointers}, \\ 
{\rm{collect-pointers}}\,({\it{bindings\/}}, {\rm{cdr}}\,({\it{alist\/}}))\index{collect-pointers})\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  collect-pointers-plistp \\ \index{collect-pointers-plistp}
{\rm{plistp}}\,({\rm{collect-pointers}}\,({\it{bindings\/}}, {\it{alist\/}})\index{collect-pointers})\index{plistp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  collect-pointers-distributes \\ \index{collect-pointers-distributes}
\=\+{\rm{collect-pointers}}\,({\it{bindings\/}}, {\rm{append}}\,({\it{lst1\/}}, {\it{lst2\/}}))\index{collect-pointers} \\ 
$=$$\;\;\;\;${\rm{append}}\,(\=\+{\rm{collect-pointers}}\,({\it{bindings\/}}, {\it{lst1\/}})\index{collect-pointers}, \\ 
{\rm{collect-pointers}}\,({\it{bindings\/}}, {\it{lst2\/}})\index{collect-pointers})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  signatures-match-preserves-collect-pointers \\ \index{signatures-match-preserves-colle!ct-pointers}
\=\+{\rm{signatures-match}}\,({\it{alist2\/}}, {\it{alist1\/}})\index{signatures-match} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{collect-pointers}}\,({\it{bindings\/}}, {\it{alist1\/}})\index{collect-pointers} \\ 
$=$$\;\;\;\;${\rm{collect-pointers}}\,({\it{bindings\/}}, {\it{alist2\/}})\index{collect-pointers})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable signatures-match-preserves-collect-pointers.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  extra-bindings-dont-affect-collect-pointers \\ \index{extra-bindings-dont-affect-colle!ct-pointers}
\=\+{\rm{no-duplicates}}\,({\rm{listcars}}\,({\rm{append}}\,({\it{bindings1\/}}, {\it{lst\/}}))\index{listcars})\index{no-duplicates} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{collect-pointers}}\,({\rm{append}}\,({\it{bindings1\/}}, {\it{bindings2\/}}), {\it{lst\/}})\index{collect-pointers} \\ 
$=$$\;\;\;\;${\rm{collect-pointers}}\,({\it{bindings2\/}}, {\it{lst\/}})\index{collect-pointers})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable extra-bindings-dont-affect-collect-pointers.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  extra-bindings-dont-affect-collect-pointers2 \\ \index{extra-bindings-dont-affect-colle!ct-pointers2}
\=\+{\rm{no-duplicates}}\,({\rm{listcars}}\,({\rm{append}}\,({\it{bindings2\/}}, {\it{lst\/}}))\index{listcars})\index{no-duplicates} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{collect-pointers}}\,({\rm{append}}\,({\it{bindings1\/}}, {\it{bindings2\/}}), {\it{lst\/}})\index{collect-pointers} \\ 
$=$$\;\;\;\;${\rm{collect-pointers}}\,({\it{bindings1\/}}, {\it{lst\/}})\index{collect-pointers})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable extra-bindings-dont-affect-collect-pointers2.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  extra-binding-doesnt-affect-collect-pointers \\ \index{extra-binding-doesnt-affect-col!lect-pointers}
\=\+({\it{x\/}} $\not\in$ {\rm{listcars}}\,({\it{lst\/}})\index{listcars}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{collect-pointers}}\,({\rm{cons}}\,({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}), {\it{bindings\/}}), {\it{lst\/}})\index{collect-pointers} \\ 
$=$$\;\;\;\;${\rm{collect-pointers}}\,({\it{bindings\/}}, {\it{lst\/}})\index{collect-pointers})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable extra-binding-doesnt-affect-collect-pointers.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  defined-array-pointers-subset-collect-pointers \\ \index{defined-array-pointers-subset-c!ollect-pointers}
\=\+(\=\+{\rm{definedp}}\,({\it{x\/}}, {\it{lst\/}})\index{definedp} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\rm{assoc}}\,({\it{x\/}}, {\it{lst\/}})))\index{simple-mg-type-refp}) \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\it{lst\/}})\index{mg-alistp})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{subset}}\,(\=\+{\rm{n-successive-pointers}}\,(\=\+{\rm{cdr}}\,({\rm{assoc}}\,({\it{x\/}}, {\it{bindings\/}})), \\ 
{\rm{length}}\,({\rm{caddr}}\,({\rm{assoc}}\,({\it{x\/}}, {\it{lst\/}})))\index{length})\-\index{n-successive-pointers}, \\ 
{\rm{collect-pointers}}\,({\it{bindings\/}}, {\it{lst\/}})\index{collect-pointers})\-\index{subset}\-
\end{tabbing}


\noindent{\sc Event}:   Disable defined-array-pointers-subset-collect-pointers.

\addvspace{18pt}


\begin{verbatim};; %collect-pointers
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                    ;;
;;                          %No-P-Aliasing                            ;;
;;                                                                    ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; This says that none of the pointers in the variable list point to the same location.
;; This is much stricter than the Gypsy aliasing requirement since it doesn't make any
;; distinction between const and var parameters.  It is consistent with the restriction
;; made in mg-meaning, but both need to be relaxed.  

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{no-p-aliasing} \\  
\=\+{\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\it{alist\/}})\index{no-p-aliasing} \\ 
$=$$\;\;\;\;${\rm{no-duplicates}}\,({\rm{collect-pointers}}\,({\it{bindings\/}}, {\it{alist\/}})\index{collect-pointers})\index{no-duplicates}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  no-p-aliasing-cdr \\ \index{no-p-aliasing-cdr}
\=\+({\rm{listp}}\,({\it{lst\/}}) $\wedge$ {\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\it{lst\/}})\index{no-p-aliasing}) \\ 
$\rightarrow$$\;\;\;\;${\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\rm{cdr}}\,({\it{lst\/}}))\index{no-p-aliasing}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  no-p-aliasing-cdr2 \\ \index{no-p-aliasing-cdr2}
{\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\rm{cons}}\,({\it{x\/}}, {\it{lst\/}}))\index{no-p-aliasing} $\rightarrow$ {\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\it{lst\/}})\index{no-p-aliasing}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  no-p-aliasing-append-commutes \\ \index{no-p-aliasing-append-commutes}
{\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\rm{append}}\,({\it{x\/}}, {\it{y\/}}))\index{no-p-aliasing} $\rightarrow$ {\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\rm{append}}\,({\it{y\/}}, {\it{x\/}}))\index{no-p-aliasing}
\end{tabbing}


\noindent{\sc Event}:   Disable no-p-aliasing-append-commutes.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  cons-car-append-no-p-aliasing \\ \index{cons-car-append-no-p-aliasing}
\=\+({\rm{listp}}\,({\it{x\/}}) $\wedge$ {\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\rm{append}}\,({\it{x\/}}, {\it{y\/}}))\index{no-p-aliasing}) \\ 
$\rightarrow$$\;\;\;\;${\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\rm{cons}}\,({\rm{car}}\,({\it{x\/}}), {\it{y\/}}))\index{no-p-aliasing}\-
\end{tabbing}


\noindent{\sc Event}:   Disable cons-car-append-no-p-aliasing.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  no-p-aliasing-cdr-append \\ \index{no-p-aliasing-cdr-append}
\=\+({\rm{listp}}\,({\it{y\/}}) $\wedge$ {\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\rm{append}}\,({\it{x\/}}, {\it{y\/}}))\index{no-p-aliasing}) \\ 
$\rightarrow$$\;\;\;\;${\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\rm{append}}\,({\it{x\/}}, {\rm{cdr}}\,({\it{y\/}})))\index{no-p-aliasing}\-
\end{tabbing}


\noindent{\sc Event}:   Disable no-p-aliasing-cdr-append.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  no-p-aliasing-cons-cdr \\ \index{no-p-aliasing-cons-cdr}
\=\+{\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\rm{cons}}\,({\it{x\/}}, {\rm{cons}}\,({\it{y\/}}, {\it{lst\/}})))\index{no-p-aliasing} \\ 
$\rightarrow$$\;\;\;\;${\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\rm{cons}}\,({\it{x\/}}, {\it{lst\/}}))\index{no-p-aliasing}\-
\end{tabbing}


\noindent{\sc Event}:   Disable no-p-aliasing-cons-cdr.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  signatures-match-preserves-no-p-aliasing \\ \index{signatures-match-preserves-no-p!-aliasing}
\=\+({\rm{signatures-match}}\,({\it{alist1\/}}, {\it{alist2\/}})\index{signatures-match} $\wedge$ {\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\it{alist1\/}})\index{no-p-aliasing}) \\ 
$\rightarrow$$\;\;\;\;${\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\it{alist2\/}})\index{no-p-aliasing}\-
\end{tabbing}


\noindent{\sc Event}:   Disable signatures-match-preserves-no-p-aliasing.

\addvspace{18pt}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                    ;;
;;           %Distinct Variables Have Distinct Pointers               ;;
;;                                                                    ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

\end{verbatim}\begin{tabbing}{\sc Theorem}:  member-pointer-collect-pointers \\ \index{member-pointer-collect-pointers}
\=\+({\rm{definedp}}\,({\it{x\/}}, {\it{alist\/}})\index{definedp} $\wedge$ {\rm{mg-name-alistp}}\,({\it{alist\/}})\index{mg-name-alistp}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{untag}}\,({\rm{cdr}}\,({\rm{assoc}}\,({\it{x\/}}, {\it{bindings\/}})))\index{untag} $\in$ {\rm{collect-pointers}}\,({\it{bindings\/}}, {\it{alist\/}})\index{collect-pointers})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  no-p-aliasing-distinct-variables-base-case0 \\ \index{no-p-aliasing-distinct-variable!s-base-case0}
\=\+(\=\+{\rm{listp}}\,({\it{alist\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $=$ {\rm{caar}}\,({\it{alist\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{untag}}\,({\rm{cdr}}\,({\rm{assoc}}\,({\it{x\/}}, {\it{bindings\/}})))\index{untag} $=$ {\rm{untag}}\,({\rm{cdr}}\,({\rm{assoc}}\,({\it{y\/}}, {\it{bindings\/}})))\index{untag}) \\ 
$\wedge$$\;\;\;\;${\rm{mg-name-alistp}}\,({\it{alist\/}})\index{mg-name-alistp} \\ 
$\wedge$$\;\;\;\;${\rm{definedp}}\,({\it{y\/}}, {\it{alist\/}})\index{definedp} \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\not=$ {\it{y\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{no-duplicates}}\,({\rm{collect-pointers}}\,({\it{bindings\/}}, {\it{alist\/}})\index{collect-pointers})\index{no-duplicates})\-
\end{tabbing}


\noindent{\sc Event}:   Disable no-p-aliasing-distinct-variables-base-case0.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  no-p-aliasing-distinct-variables-base-case \\ \index{no-p-aliasing-distinct-variable!s-base-case}
\=\+(\=\+{\rm{listp}}\,({\it{alist\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $=$ {\rm{caar}}\,({\it{alist\/}})) \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\it{alist\/}})\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{mg-name-alistp}}\,({\it{alist\/}})\index{mg-name-alistp} \\ 
$\wedge$$\;\;\;\;${\rm{definedp}}\,({\it{x\/}}, {\it{alist\/}})\index{definedp} \\ 
$\wedge$$\;\;\;\;${\rm{definedp}}\,({\it{y\/}}, {\it{alist\/}})\index{definedp} \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\not=$ {\it{y\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{untag}}\,({\rm{cdr}}\,({\rm{assoc}}\,({\it{x\/}}, {\it{bindings\/}})))\index{untag} $\not=$ {\rm{untag}}\,({\rm{cdr}}\,({\rm{assoc}}\,({\it{y\/}}, {\it{bindings\/}})))\index{untag})\-
\end{tabbing}


\noindent{\sc Event}:   Disable no-p-aliasing-distinct-variables-base-case.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  no-p-aliasing-distinct-variables \\ \index{no-p-aliasing-distinct-variable!s}
\=\+(\=\+{\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\it{alist\/}})\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{mg-name-alistp}}\,({\it{alist\/}})\index{mg-name-alistp} \\ 
$\wedge$$\;\;\;\;${\rm{definedp}}\,({\it{x\/}}, {\it{alist\/}})\index{definedp} \\ 
$\wedge$$\;\;\;\;${\rm{definedp}}\,({\it{y\/}}, {\it{alist\/}})\index{definedp} \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\not=$ {\it{y\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{untag}}\,({\rm{cdr}}\,({\rm{assoc}}\,({\it{x\/}}, {\it{bindings\/}})))\index{untag} $\not=$ {\rm{untag}}\,({\rm{cdr}}\,({\rm{assoc}}\,({\it{y\/}}, {\it{bindings\/}})))\index{untag})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  distinct-variables-lemma2-base-case \\ \index{distinct-variables-lemma2-base-!case}
\=\+(\=\+{\rm{listp}}\,({\it{lst\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $=$ {\rm{caar}}\,({\it{lst\/}})) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{untag}}\,({\rm{cdr}}\,({\rm{assoc}}\,({\it{x\/}}, {\it{bindings\/}})))\index{untag} \\ 
$\in$$\;\;\;\;${\rm{n-successive-pointers}}\,(\=\+{\rm{cdr}}\,({\rm{assoc}}\,({\it{y\/}}, {\it{bindings\/}})), \\ 
{\rm{length}}\,({\rm{caddr}}\,({\rm{assoc}}\,({\it{y\/}}, {\it{lst\/}})))\index{length})\-\index{n-successive-pointers})\- \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\it{lst\/}})\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;${\rm{definedp}}\,({\it{x\/}}, {\it{lst\/}})\index{definedp} \\ 
$\wedge$$\;\;\;\;${\rm{definedp}}\,({\it{y\/}}, {\it{lst\/}})\index{definedp} \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\not=$ {\it{y\/}}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\rm{assoc}}\,({\it{y\/}}, {\it{lst\/}})))\index{simple-mg-type-refp}))\- \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\it{lst\/}})\index{no-p-aliasing})\-
\end{tabbing}


\noindent{\sc Event}:   Disable distinct-variables-lemma2-base-case.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  distinct-variables-lemma2 \\ \index{distinct-variables-lemma2}
\=\+(\=\+{\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\it{lst\/}})\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\it{lst\/}})\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;${\rm{definedp}}\,({\it{x\/}}, {\it{lst\/}})\index{definedp} \\ 
$\wedge$$\;\;\;\;${\rm{definedp}}\,({\it{y\/}}, {\it{lst\/}})\index{definedp} \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\not=$ {\it{y\/}}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\rm{assoc}}\,({\it{y\/}}, {\it{lst\/}})))\index{simple-mg-type-refp}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{untag}}\,({\rm{cdr}}\,({\rm{assoc}}\,({\it{x\/}}, {\it{bindings\/}})))\index{untag} \\ 
$\not\in$$\;\;\;\;${\rm{n-successive-pointers}}\,(\=\+{\rm{cdr}}\,({\rm{assoc}}\,({\it{y\/}}, {\it{bindings\/}})), \\ 
{\rm{length}}\,({\rm{caddr}}\,({\rm{assoc}}\,({\it{y\/}}, {\it{lst\/}})))\index{length})\-\index{n-successive-pointers})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  distinct-array-values-one-way-disjoint \\ \index{distinct-array-values-one-way-di!sjoint}
\=\+(\=\+{\rm{mg-vars-list-ok-in-p-state}}\,({\it{lst\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\it{lst\/}})\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\it{lst\/}})\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\it{lst\/}})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{definedp}}\,({\it{x\/}}, {\it{lst\/}})\index{definedp} \\ 
$\wedge$$\;\;\;\;${\rm{definedp}}\,({\it{y\/}}, {\it{lst\/}})\index{definedp} \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\not=$ {\it{y\/}}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\rm{assoc}}\,({\it{x\/}}, {\it{lst\/}})))\index{simple-mg-type-refp}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\rm{assoc}}\,({\it{y\/}}, {\it{lst\/}})))\index{simple-mg-type-refp}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{one-way-disjoint}}\,(\=\+{\rm{n-successive-pointers}}\,(\=\+{\rm{cdr}}\,({\rm{assoc}}\,({\it{x\/}}, {\it{bindings\/}})), \\ 
{\rm{length}}\,({\rm{caddr}}\,({\rm{assoc}}\,({\it{x\/}}, {\it{lst\/}})))\index{length})\-\index{n-successive-pointers}, \\ 
{\rm{n-successive-pointers}}\,(\=\+{\rm{cdr}}\,({\rm{assoc}}\,({\it{y\/}}, {\it{bindings\/}})), \\ 
{\rm{length}}\,({\rm{caddr}}\,({\rm{assoc}}\,({\it{y\/}}, {\it{lst\/}})))\index{length})\-\index{n-successive-pointers})\-\index{one-way-disjoint}\-
\end{tabbing}


\noindent{\sc Event}:   Disable distinct-array-values-one-way-disjoint.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  distinct-array-values-disjoint \\ \index{distinct-array-values-disjoint}
\=\+(\=\+{\rm{mg-vars-list-ok-in-p-state}}\,({\it{lst\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\it{lst\/}})\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\it{lst\/}})\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\it{lst\/}})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{definedp}}\,({\it{x\/}}, {\it{lst\/}})\index{definedp} \\ 
$\wedge$$\;\;\;\;${\rm{definedp}}\,({\it{y\/}}, {\it{lst\/}})\index{definedp} \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\not=$ {\it{y\/}}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\rm{assoc}}\,({\it{x\/}}, {\it{lst\/}})))\index{simple-mg-type-refp}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\rm{assoc}}\,({\it{y\/}}, {\it{lst\/}})))\index{simple-mg-type-refp}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{disjoint}}\,(\=\+{\rm{n-successive-pointers}}\,(\=\+{\rm{cdr}}\,({\rm{assoc}}\,({\it{x\/}}, {\it{bindings\/}})), \\ 
{\rm{array-length}}\,({\rm{cadr}}\,({\rm{assoc}}\,({\it{x\/}}, {\it{lst\/}})))\index{array-length})\-\index{n-successive-pointers}, \\ 
{\rm{n-successive-pointers}}\,(\=\+{\rm{cdr}}\,({\rm{assoc}}\,({\it{y\/}}, {\it{bindings\/}})), \\ 
{\rm{array-length}}\,({\rm{cadr}}\,({\rm{assoc}}\,({\it{y\/}}, {\it{lst\/}})))\index{array-length})\-\index{n-successive-pointers})\-\index{disjoint}\-
\end{tabbing}

\begin{verbatim};; %distinct variables
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                    ;;
;;                        %Deposits Commutes                          ;;
;;                                                                    ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

\end{verbatim}\begin{tabbing}{\sc Theorem}:  deposit-array-value-append1 \\ \index{deposit-array-value-append1}
\=\+(\=\+({\rm{untag}}\,({\it{nat\/}})\index{untag} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$(({\rm{untag}}\,({\it{nat\/}})\index{untag} $+$ ({\rm{length}}\,({\it{value\/}})\index{length} $-\;1$)) $<$ {\rm{length}}\,({\it{temp-stk\/}})\index{length}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{deposit-array-value}}\,({\it{value\/}}, {\it{nat\/}}, {\rm{append}}\,({\it{lst\/}}, {\it{temp-stk\/}}))\index{deposit-array-value} \\ 
$=$$\;\;\;\;${\rm{append}}\,({\it{lst\/}}, {\rm{deposit-array-value}}\,({\it{value\/}}, {\it{nat\/}}, {\it{temp-stk\/}})\index{deposit-array-value}))\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable deposit-array-value-append1.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  deposit-array-value-append \\ \index{deposit-array-value-append}
\=\+(\=\+({\it{x\/}} $\in$ {\it{vars\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\it{vars\/}})\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\it{x\/}}))\index{simple-mg-type-refp}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{deposit-array-value}}\,(\=\+{\rm{caddr}}\,({\it{x\/}}), \\ 
{\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{x\/}}), {\it{bindings\/}})), \\ 
{\rm{append}}\,({\it{lst\/}}, {\it{temp-stk\/}}))\-\index{deposit-array-value} \\ 
$=$$\;\;\;\;${\rm{append}}\,(\=\+{\it{lst\/}}, \\ 
{\rm{deposit-array-value}}\,(\=\+{\rm{caddr}}\,({\it{x\/}}), \\ 
{\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{x\/}}), {\it{bindings\/}})), \\ 
{\it{temp-stk\/}})\-\index{deposit-array-value})\-)\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable deposit-array-value-append.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  deposit-alist-value-append \\ \index{deposit-alist-value-append}
\=\+(\=\+({\it{x\/}} $\in$ {\it{vars\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\it{vars\/}})\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{deposit-alist-value}}\,({\it{x\/}}, {\it{bindings\/}}, {\rm{append}}\,({\it{lst\/}}, {\it{temp-stk\/}}))\index{deposit-alist-value} \\ 
$=$$\;\;\;\;${\rm{append}}\,({\it{lst\/}}, {\rm{deposit-alist-value}}\,({\it{x\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{deposit-alist-value}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  deposit-temp-commutes \\ \index{deposit-temp-commutes}
\=\+(\=\+({\rm{untag}}\,({\it{y\/}})\index{untag} $\not=$ {\rm{untag}}\,({\it{u\/}})\index{untag}) \\ 
$\wedge$$\;\;\;\;$({\rm{untag}}\,({\it{y\/}})\index{untag} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\rm{untag}}\,({\it{u\/}})\index{untag} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\rm{untag}}\,({\it{u\/}})\index{untag} $<$ {\rm{length}}\,({\it{v\/}})\index{length}) \\ 
$\wedge$$\;\;\;\;$({\rm{untag}}\,({\it{y\/}})\index{untag} $<$ {\rm{length}}\,({\it{v\/}})\index{length}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{deposit-temp}}\,({\it{x\/}}, {\it{y\/}}, {\rm{deposit-temp}}\,({\it{z\/}}, {\it{u\/}}, {\it{v\/}})\index{deposit-temp})\index{deposit-temp} \\ 
$=$$\;\;\;\;${\rm{deposit-temp}}\,({\it{z\/}}, {\it{u\/}}, {\rm{deposit-temp}}\,({\it{x\/}}, {\it{y\/}}, {\it{v\/}})\index{deposit-temp})\index{deposit-temp})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable deposit-temp-commutes.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  deposit-temp-commutes0 \\ \index{deposit-temp-commutes0}
\=\+(\=\+{\rm{mg-vars-list-ok-in-p-state}}\,({\it{lst\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\it{lst\/}})\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\it{lst\/}})\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\it{lst\/}})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\in$ {\it{lst\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{y\/}} $\in$ {\it{lst\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{x\/}}) $\not=$ {\rm{car}}\,({\it{y\/}})))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{deposit-temp}}\,(\=\+{\it{x-value\/}}, \\ 
{\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{x\/}}), {\it{bindings\/}})), \\ 
{\rm{deposit-temp}}\,(\=\+{\it{y-value\/}}, \\ 
{\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{y\/}}), {\it{bindings\/}})), \\ 
{\it{temp-stk\/}})\-\index{deposit-temp})\-\index{deposit-temp} \\ 
$=$$\;\;\;\;${\rm{deposit-temp}}\,(\=\+{\it{y-value\/}}, \\ 
{\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{y\/}}), {\it{bindings\/}})), \\ 
{\rm{deposit-temp}}\,(\=\+{\it{x-value\/}}, \\ 
{\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{x\/}}), {\it{bindings\/}})), \\ 
{\it{temp-stk\/}})\-\index{deposit-temp})\-\index{deposit-temp})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable deposit-temp-commutes0.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  deposit-temp-deposit-array-value-commute \\ \index{deposit-temp-deposit-array-value!-commute}
\=\+(\=\+({\rm{untag}}\,({\it{nat1\/}})\index{untag} $\not\in$ {\rm{n-successive-pointers}}\,({\it{nat2\/}}, {\rm{length}}\,({\it{value\/}})\index{length})\index{n-successive-pointers}) \\ 
$\wedge$$\;\;\;\;$({\rm{untag}}\,({\it{nat1\/}})\index{untag} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\rm{untag}}\,({\it{nat2\/}})\index{untag} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\rm{untag}}\,({\it{nat1\/}})\index{untag} $<$ {\rm{length}}\,({\it{temp-stk\/}})\index{length}) \\ 
$\wedge$$\;\;\;\;$(({\rm{untag}}\,({\it{nat2\/}})\index{untag} $+$ ({\rm{length}}\,({\it{value\/}})\index{length} $-\;1$)) $<$ {\rm{length}}\,({\it{temp-stk\/}})\index{length}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{deposit-temp}}\,({\it{z\/}}, {\it{nat1\/}}, {\rm{deposit-array-value}}\,({\it{value\/}}, {\it{nat2\/}}, {\it{temp-stk\/}})\index{deposit-array-value})\index{deposit-temp} \\ 
$=$$\;\;\;\;${\rm{deposit-array-value}}\,({\it{value\/}}, {\it{nat2\/}}, {\rm{deposit-temp}}\,({\it{z\/}}, {\it{nat1\/}}, {\it{temp-stk\/}})\index{deposit-temp})\index{deposit-array-value})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable deposit-temp-deposit-array-value-commute.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  deposit-temp-deposit-array-value-commute2 \\ \index{deposit-temp-deposit-array-value!-commute2}
\=\+(\=\+{\rm{mg-vars-list-ok-in-p-state}}\,({\it{lst\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\it{lst\/}})\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\it{lst\/}})\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\it{lst\/}})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\in$ {\it{lst\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{y\/}} $\in$ {\it{lst\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{x\/}}) $\not=$ {\rm{car}}\,({\it{y\/}})) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\it{y\/}}))\index{simple-mg-type-refp}) \\ 
$\wedge$$\;\;\;\;$({\rm{length}}\,({\it{y-value\/}})\index{length} $=$ {\rm{array-length}}\,({\rm{cadr}}\,({\it{y\/}}))\index{array-length}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{deposit-temp}}\,(\=\+{\it{z\/}}, \\ 
{\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{x\/}}), {\it{bindings\/}})), \\ 
{\rm{deposit-array-value}}\,(\=\+{\it{y-value\/}}, \\ 
{\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{y\/}}), {\it{bindings\/}})), \\ 
{\it{temp-stk\/}})\-\index{deposit-array-value})\-\index{deposit-temp} \\ 
$=$$\;\;\;\;${\rm{deposit-array-value}}\,(\=\+{\it{y-value\/}}, \\ 
{\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{y\/}}), {\it{bindings\/}})), \\ 
{\rm{deposit-temp}}\,(\=\+{\it{z\/}}, \\ 
{\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{x\/}}), {\it{bindings\/}})), \\ 
{\it{temp-stk\/}})\-\index{deposit-temp})\-\index{deposit-array-value})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable deposit-temp-deposit-array-value-commute2.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  one-way-disjoint-non-member-n-successive-pointers \\ \index{one-way-disjoint-non-member-n-s!uccessive-pointers}
\=\+(\=\+{\rm{one-way-disjoint}}\,(\=\+{\rm{n-successive-pointers}}\,({\it{x-nat\/}}, {\it{n\/}})\index{n-successive-pointers}, \\ 
{\rm{n-successive-pointers}}\,({\it{y-nat\/}}, {\it{m\/}})\index{n-successive-pointers})\-\index{one-way-disjoint} \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not\simeq {\tt{0}}$))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{untag}}\,({\it{x-nat\/}})\index{untag} $\not\in$ {\rm{n-successive-pointers}}\,({\it{y-nat\/}}, {\it{m\/}})\index{n-successive-pointers})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  deposit-array-value-commutes \\ \index{deposit-array-value-commutes}
\=\+(\=\+({\rm{untag}}\,({\it{x-nat\/}})\index{untag} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\rm{untag}}\,({\it{y-nat\/}})\index{untag} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$(({\rm{untag}}\,({\it{x-nat\/}})\index{untag} $+$ ({\rm{length}}\,({\it{x-value\/}})\index{length} $-\;1$)) $<$ {\rm{length}}\,({\it{temp-stk\/}})\index{length}) \\ 
$\wedge$$\;\;\;\;$(({\rm{untag}}\,({\it{y-nat\/}})\index{untag} $+$ ({\rm{length}}\,({\it{y-value\/}})\index{length} $-\;1$)) $<$ {\rm{length}}\,({\it{temp-stk\/}})\index{length}) \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,(\=\+{\rm{n-successive-pointers}}\,({\it{x-nat\/}}, {\rm{length}}\,({\it{x-value\/}})\index{length})\index{n-successive-pointers}, \\ 
{\rm{n-successive-pointers}}\,({\it{y-nat\/}}, {\rm{length}}\,({\it{y-value\/}})\index{length})\index{n-successive-pointers})\-\index{disjoint})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{deposit-array-value}}\,(\=\+{\it{x-value\/}}, \\ 
{\it{x-nat\/}}, \\ 
{\rm{deposit-array-value}}\,({\it{y-value\/}}, {\it{y-nat\/}}, {\it{temp-stk\/}})\index{deposit-array-value})\-\index{deposit-array-value} \\ 
$=$$\;\;\;\;${\rm{deposit-array-value}}\,(\=\+{\it{y-value\/}}, \\ 
{\it{y-nat\/}}, \\ 
{\rm{deposit-array-value}}\,(\=\+{\it{x-value\/}}, \\ 
{\it{x-nat\/}}, \\ 
{\it{temp-stk\/}})\-\index{deposit-array-value})\-\index{deposit-array-value})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable deposit-array-value-commutes.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  deposit-array-value-commutes2 \\ \index{deposit-array-value-commutes2}
\=\+(\=\+{\rm{mg-vars-list-ok-in-p-state}}\,({\it{lst\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\it{lst\/}})\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\it{lst\/}})\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\it{lst\/}})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\in$ {\it{lst\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{y\/}} $\in$ {\it{lst\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{x\/}}) $\not=$ {\rm{car}}\,({\it{y\/}})) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\it{x\/}}))\index{simple-mg-type-refp}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\it{y\/}}))\index{simple-mg-type-refp}) \\ 
$\wedge$$\;\;\;\;$({\rm{length}}\,({\it{x-value\/}})\index{length} $=$ {\rm{array-length}}\,({\rm{cadr}}\,({\it{x\/}}))\index{array-length}) \\ 
$\wedge$$\;\;\;\;$({\rm{length}}\,({\it{y-value\/}})\index{length} $=$ {\rm{array-length}}\,({\rm{cadr}}\,({\it{y\/}}))\index{array-length}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{deposit-array-value}}\,(\=\+{\it{x-value\/}}, \\ 
{\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{x\/}}), {\it{bindings\/}})), \\ 
{\rm{deposit-array-value}}\,(\=\+{\it{y-value\/}}, \\ 
{\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{y\/}}), {\it{bindings\/}})), \\ 
{\it{temp-stk\/}})\-\index{deposit-array-value})\-\index{deposit-array-value} \\ 
$=$$\;\;\;\;${\rm{deposit-array-value}}\,(\=\+{\it{y-value\/}}, \\ 
{\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{y\/}}), {\it{bindings\/}})), \\ 
{\rm{deposit-array-value}}\,(\=\+{\it{x-value\/}}, \\ 
{\rm{cdr}}\,({\rm{assoc}}\,(\=\+{\rm{car}}\,({\it{x\/}}), \\ 
{\it{bindings\/}})\-), \\ 
{\it{temp-stk\/}})\-\index{deposit-array-value})\-\index{deposit-array-value})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable deposit-array-value-commutes2.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  deposit-alist-value-commutes \\ \index{deposit-alist-value-commutes}
\=\+(\=\+{\rm{mg-vars-list-ok-in-p-state}}\,({\it{lst\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\it{lst\/}})\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\it{lst\/}})\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\it{lst\/}})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\in$ {\it{lst\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{y\/}} $\in$ {\it{lst\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{x\/}}) $\not=$ {\rm{car}}\,({\it{y\/}})))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{deposit-alist-value}}\,(\=\+{\it{x\/}}, \\ 
{\it{bindings\/}}, \\ 
{\rm{deposit-alist-value}}\,({\it{y\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{deposit-alist-value})\-\index{deposit-alist-value} \\ 
$=$$\;\;\;\;${\rm{deposit-alist-value}}\,(\=\+{\it{y\/}}, \\ 
{\it{bindings\/}}, \\ 
{\rm{deposit-alist-value}}\,({\it{x\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{deposit-alist-value})\-\index{deposit-alist-value})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  deposit-temp-deposit-array-value-commute3 \\ \index{deposit-temp-deposit-array-value!-commute3}
\=\+(\=\+({\rm{untag}}\,({\it{nat\/}})\index{untag} $<$ {\rm{untag}}\,({\it{nat1\/}})\index{untag}) \\ 
$\wedge$$\;\;\;\;$({\rm{untag}}\,({\it{nat\/}})\index{untag} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$(({\rm{untag}}\,({\it{nat1\/}})\index{untag} $+$ ({\rm{length}}\,({\it{lst\/}})\index{length} $-\;1$)) $<$ {\rm{length}}\,({\it{temp-stk\/}})\index{length}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{deposit-array-value}}\,({\it{lst\/}}, {\it{nat1\/}}, {\rm{deposit-temp}}\,({\it{x\/}}, {\it{nat\/}}, {\it{temp-stk\/}})\index{deposit-temp})\index{deposit-array-value} \\ 
$=$$\;\;\;\;${\rm{deposit-temp}}\,({\it{x\/}}, {\it{nat\/}}, {\rm{deposit-array-value}}\,({\it{lst\/}}, {\it{nat1\/}}, {\it{temp-stk\/}})\index{deposit-array-value})\index{deposit-temp})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable deposit-temp-deposit-array-value-commute3.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  multiple-rputs-cancel \\ \index{multiple-rputs-cancel}
{\rm{rput}}\,({\it{x\/}}, {\it{y\/}}, {\rm{rput}}\,({\it{u\/}}, {\it{y\/}}, {\it{z\/}})\index{rput})\index{rput} $=$ {\rm{rput}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{rput}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  multiple-deposit-temps-cancel \\ \index{multiple-deposit-temps-cancel}
\=\+{\rm{deposit-temp}}\,({\it{x\/}}, {\it{nat\/}}, {\rm{deposit-temp}}\,({\it{y\/}}, {\it{nat\/}}, {\it{temp-stk\/}})\index{deposit-temp})\index{deposit-temp} \\ 
$=$$\;\;\;\;${\rm{deposit-temp}}\,({\it{x\/}}, {\it{nat\/}}, {\it{temp-stk\/}})\index{deposit-temp}\-
\end{tabbing}


\noindent{\sc Event}:   Disable multiple-deposit-temps-cancel.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{double-cdr-induction2} \\  
\=\+{\rm{double-cdr-induction2}}\,({\it{x\/}}, {\it{y\/}}, {\it{nat\/}})\index{double-cdr-induction2} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{double-cdr-induction2}}\,({\rm{cdr}}\,({\it{x\/}}), {\rm{cdr}}\,({\it{y\/}}), {\rm{add1-nat}}\,({\it{nat\/}})\index{add1-nat})\index{double-cdr-induction2}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  multiple-deposit-array-values-cancel \\ \index{multiple-deposit-array-values-c!ancel}
\=\+(\=\+({\rm{length}}\,({\it{value1\/}})\index{length} $=$ {\rm{length}}\,({\it{value2\/}})\index{length}) \\ 
$\wedge$$\;\;\;\;$({\rm{untag}}\,({\it{nat\/}})\index{untag} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$(({\rm{untag}}\,({\it{nat\/}})\index{untag} $+$ ({\rm{length}}\,({\it{value1\/}})\index{length} $-\;1$)) $<$ {\rm{length}}\,({\it{temp-stk\/}})\index{length}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{deposit-array-value}}\,(\=\+{\it{value1\/}}, \\ 
{\it{nat\/}}, \\ 
{\rm{deposit-array-value}}\,({\it{value2\/}}, {\it{nat\/}}, {\it{temp-stk\/}})\index{deposit-array-value})\-\index{deposit-array-value} \\ 
$=$$\;\;\;\;${\rm{deposit-array-value}}\,({\it{value1\/}}, {\it{nat\/}}, {\it{temp-stk\/}})\index{deposit-array-value})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable multiple-deposit-array-values-cancel.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  mg-var-ok-car-definedp \\ \index{mg-var-ok-car-definedp}
\=\+(({\it{y\/}} $\in$ {\it{alist\/}}) $\wedge$ {\rm{mg-vars-list-ok-in-p-state}}\,({\it{alist\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state}) \\ 
$\rightarrow$$\;\;\;\;${\rm{definedp}}\,({\rm{car}}\,({\it{y\/}}), {\it{bindings\/}})\index{definedp}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  deposit-temp-deposit-temp-commute2 \\ \index{deposit-temp-deposit-temp-commute!2}
\=\+(\=\+{\rm{no-p-aliasing}}\,({\rm{append}}\,({\it{bindings1\/}}, {\it{bindings2\/}}), {\rm{append}}\,({\it{alist1\/}}, {\it{alist2\/}}))\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{alist1\/}}, {\it{bindings1\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{alist2\/}}, {\it{bindings2\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{append}}\,({\it{alist1\/}}, {\it{alist2\/}}))\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{append}}\,({\it{bindings1\/}}, {\it{bindings2\/}}))\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\rm{append}}\,({\it{alist1\/}}, {\it{alist2\/}}))\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\in$ {\it{alist1\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\it{x\/}}))\index{simple-mg-type-refp} \\ 
$\wedge$$\;\;\;\;$({\it{y\/}} $\in$ {\it{alist2\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\it{y\/}}))\index{simple-mg-type-refp})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{deposit-temp}}\,(\=\+{\it{x-value\/}}, \\ 
{\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{x\/}}), {\it{bindings1\/}})), \\ 
{\rm{deposit-temp}}\,(\=\+{\it{y-value\/}}, \\ 
{\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{y\/}}), {\it{bindings2\/}})), \\ 
{\it{temp-stk\/}})\-\index{deposit-temp})\-\index{deposit-temp} \\ 
$=$$\;\;\;\;${\rm{deposit-temp}}\,(\=\+{\it{y-value\/}}, \\ 
{\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{y\/}}), {\it{bindings2\/}})), \\ 
{\rm{deposit-temp}}\,(\=\+{\it{x-value\/}}, \\ 
{\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{x\/}}), {\it{bindings1\/}})), \\ 
{\it{temp-stk\/}})\-\index{deposit-temp})\-\index{deposit-temp})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable deposit-temp-deposit-temp-commute2.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  deposit-temp-deposit-array-value-commute5 \\ \index{deposit-temp-deposit-array-value!-commute5}
\=\+(\=\+{\rm{no-p-aliasing}}\,({\rm{append}}\,({\it{bindings1\/}}, {\it{bindings2\/}}), {\rm{append}}\,({\it{alist1\/}}, {\it{alist2\/}}))\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{alist1\/}}, {\it{bindings1\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{alist2\/}}, {\it{bindings2\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{append}}\,({\it{alist1\/}}, {\it{alist2\/}}))\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{append}}\,({\it{bindings1\/}}, {\it{bindings2\/}}))\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\rm{append}}\,({\it{alist1\/}}, {\it{alist2\/}}))\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\in$ {\it{alist1\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\it{x\/}}))\index{simple-mg-type-refp} \\ 
$\wedge$$\;\;\;\;$({\it{y\/}} $\in$ {\it{alist2\/}}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\it{y\/}}))\index{simple-mg-type-refp}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{deposit-temp}}\,(\=\+{\it{value\/}}, \\ 
{\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{x\/}}), {\it{bindings1\/}})), \\ 
{\rm{deposit-array-value}}\,(\=\+{\rm{caddr}}\,({\it{y\/}}), \\ 
{\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{y\/}}), {\it{bindings2\/}})), \\ 
{\it{temp-stk\/}})\-\index{deposit-array-value})\-\index{deposit-temp} \\ 
$=$$\;\;\;\;${\rm{deposit-array-value}}\,(\=\+{\rm{caddr}}\,({\it{y\/}}), \\ 
{\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{y\/}}), {\it{bindings2\/}})), \\ 
{\rm{deposit-temp}}\,(\=\+{\it{value\/}}, \\ 
{\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{x\/}}), {\it{bindings1\/}})), \\ 
{\it{temp-stk\/}})\-\index{deposit-temp})\-\index{deposit-array-value})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable deposit-temp-deposit-array-value-commute5.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  deposit-temp-deposit-alist-value-commute2 \\ \index{deposit-temp-deposit-alist-value!-commute2}
\=\+(\=\+{\rm{no-p-aliasing}}\,({\rm{append}}\,({\it{bindings1\/}}, {\it{bindings2\/}}), {\rm{append}}\,({\it{alist1\/}}, {\it{alist2\/}}))\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{alist1\/}}, {\it{bindings1\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{alist2\/}}, {\it{bindings2\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{append}}\,({\it{alist1\/}}, {\it{alist2\/}}))\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{append}}\,({\it{bindings1\/}}, {\it{bindings2\/}}))\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\rm{append}}\,({\it{alist1\/}}, {\it{alist2\/}}))\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\in$ {\it{alist1\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\it{x\/}}))\index{simple-mg-type-refp} \\ 
$\wedge$$\;\;\;\;$({\it{y\/}} $\in$ {\it{alist2\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{deposit-temp}}\,(\=\+{\it{value\/}}, \\ 
{\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{x\/}}), {\it{bindings1\/}})), \\ 
{\rm{deposit-alist-value}}\,({\it{y\/}}, {\it{bindings2\/}}, {\it{temp-stk\/}})\index{deposit-alist-value})\-\index{deposit-temp} \\ 
$=$$\;\;\;\;${\rm{deposit-alist-value}}\,(\=\+{\it{y\/}}, \\ 
{\it{bindings2\/}}, \\ 
{\rm{deposit-temp}}\,(\=\+{\it{value\/}}, \\ 
{\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{x\/}}), {\it{bindings1\/}})), \\ 
{\it{temp-stk\/}})\-\index{deposit-temp})\-\index{deposit-alist-value})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable deposit-temp-deposit-alist-value-commute2.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  deposit-array-value-deposit-array-value-commute2 \\ \index{deposit-array-value-deposit-arr!ay-value-commute2}
\=\+(\=\+{\rm{no-p-aliasing}}\,({\rm{append}}\,({\it{bindings1\/}}, {\it{bindings2\/}}), {\rm{append}}\,({\it{alist1\/}}, {\it{alist2\/}}))\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{alist1\/}}, {\it{bindings1\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{alist2\/}}, {\it{bindings2\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{append}}\,({\it{alist1\/}}, {\it{alist2\/}}))\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{append}}\,({\it{bindings1\/}}, {\it{bindings2\/}}))\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\rm{append}}\,({\it{alist1\/}}, {\it{alist2\/}}))\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\in$ {\it{alist1\/}}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\it{x\/}}))\index{simple-mg-type-refp}) \\ 
$\wedge$$\;\;\;\;$({\it{y\/}} $\in$ {\it{alist2\/}}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\it{y\/}}))\index{simple-mg-type-refp}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{deposit-array-value}}\,(\=\+{\rm{caddr}}\,({\it{x\/}}), \\ 
{\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{x\/}}), {\it{bindings1\/}})), \\ 
{\rm{deposit-array-value}}\,(\=\+{\rm{caddr}}\,({\it{y\/}}), \\ 
{\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{y\/}}), {\it{bindings2\/}})), \\ 
{\it{temp-stk\/}})\-\index{deposit-array-value})\-\index{deposit-array-value} \\ 
$=$$\;\;\;\;${\rm{deposit-array-value}}\,(\=\+{\rm{caddr}}\,({\it{y\/}}), \\ 
{\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{y\/}}), {\it{bindings2\/}})), \\ 
{\rm{deposit-array-value}}\,(\=\+{\rm{caddr}}\,({\it{x\/}}), \\ 
{\rm{cdr}}\,({\rm{assoc}}\,(\=\+{\rm{car}}\,({\it{x\/}}), \\ 
{\it{bindings1\/}})\-), \\ 
{\it{temp-stk\/}})\-\index{deposit-array-value})\-\index{deposit-array-value})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable deposit-array-value-deposit-array-value-commute2.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  deposit-array-value-deposit-temp-commute \\ \index{deposit-array-value-deposit-temp!-commute}
\=\+(\=\+{\rm{no-p-aliasing}}\,({\rm{append}}\,({\it{bindings1\/}}, {\it{bindings2\/}}), {\rm{append}}\,({\it{alist1\/}}, {\it{alist2\/}}))\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{alist1\/}}, {\it{bindings1\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{alist2\/}}, {\it{bindings2\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{append}}\,({\it{alist1\/}}, {\it{alist2\/}}))\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{append}}\,({\it{bindings1\/}}, {\it{bindings2\/}}))\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\rm{append}}\,({\it{alist1\/}}, {\it{alist2\/}}))\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\in$ {\it{alist1\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\it{y\/}}))\index{simple-mg-type-refp} \\ 
$\wedge$$\;\;\;\;$({\it{y\/}} $\in$ {\it{alist2\/}}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\it{x\/}}))\index{simple-mg-type-refp}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{deposit-array-value}}\,(\=\+{\rm{caddr}}\,({\it{x\/}}), \\ 
{\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{x\/}}), {\it{bindings1\/}})), \\ 
{\rm{deposit-temp}}\,(\=\+{\it{value\/}}, \\ 
{\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{y\/}}), {\it{bindings2\/}})), \\ 
{\it{temp-stk\/}})\-\index{deposit-temp})\-\index{deposit-array-value} \\ 
$=$$\;\;\;\;${\rm{deposit-temp}}\,(\=\+{\it{value\/}}, \\ 
{\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{y\/}}), {\it{bindings2\/}})), \\ 
{\rm{deposit-array-value}}\,(\=\+{\rm{caddr}}\,({\it{x\/}}), \\ 
{\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{x\/}}), {\it{bindings1\/}})), \\ 
{\it{temp-stk\/}})\-\index{deposit-array-value})\-\index{deposit-temp})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable deposit-array-value-deposit-temp-commute.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  deposit-array-value-deposit-alist-value-commute \\ \index{deposit-array-value-deposit-ali!st-value-commute}
\=\+(\=\+{\rm{no-p-aliasing}}\,({\rm{append}}\,({\it{bindings1\/}}, {\it{bindings2\/}}), {\rm{append}}\,({\it{alist1\/}}, {\it{alist2\/}}))\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{alist1\/}}, {\it{bindings1\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{alist2\/}}, {\it{bindings2\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{append}}\,({\it{alist1\/}}, {\it{alist2\/}}))\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{append}}\,({\it{bindings1\/}}, {\it{bindings2\/}}))\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\rm{append}}\,({\it{alist1\/}}, {\it{alist2\/}}))\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\in$ {\it{alist1\/}}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\it{x\/}}))\index{simple-mg-type-refp}) \\ 
$\wedge$$\;\;\;\;$({\it{y\/}} $\in$ {\it{alist2\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{deposit-array-value}}\,(\=\+{\rm{caddr}}\,({\it{x\/}}), \\ 
{\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{x\/}}), {\it{bindings1\/}})), \\ 
{\rm{deposit-alist-value}}\,({\it{y\/}}, {\it{bindings2\/}}, {\it{temp-stk\/}})\index{deposit-alist-value})\-\index{deposit-array-value} \\ 
$=$$\;\;\;\;${\rm{deposit-alist-value}}\,(\=\+{\it{y\/}}, \\ 
{\it{bindings2\/}}, \\ 
{\rm{deposit-array-value}}\,(\=\+{\rm{caddr}}\,({\it{x\/}}), \\ 
{\rm{cdr}}\,({\rm{assoc}}\,(\=\+{\rm{car}}\,({\it{x\/}}), \\ 
{\it{bindings1\/}})\-), \\ 
{\it{temp-stk\/}})\-\index{deposit-array-value})\-\index{deposit-alist-value})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable deposit-array-value-deposit-alist-value-commute.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  deposit-alist-value-commute2 \\ \index{deposit-alist-value-commute2}
\=\+(\=\+{\rm{no-p-aliasing}}\,({\rm{append}}\,({\it{bindings1\/}}, {\it{bindings2\/}}), {\rm{append}}\,({\it{alist1\/}}, {\it{alist2\/}}))\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{alist1\/}}, {\it{bindings1\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{alist2\/}}, {\it{bindings2\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{append}}\,({\it{alist1\/}}, {\it{alist2\/}}))\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{append}}\,({\it{bindings1\/}}, {\it{bindings2\/}}))\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\rm{append}}\,({\it{alist1\/}}, {\it{alist2\/}}))\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\in$ {\it{alist1\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{y\/}} $\in$ {\it{alist2\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{deposit-alist-value}}\,(\=\+{\it{x\/}}, \\ 
{\it{bindings1\/}}, \\ 
{\rm{deposit-alist-value}}\,({\it{y\/}}, {\it{bindings2\/}}, {\it{temp-stk\/}})\index{deposit-alist-value})\-\index{deposit-alist-value} \\ 
$=$$\;\;\;\;${\rm{deposit-alist-value}}\,(\=\+{\it{y\/}}, \\ 
{\it{bindings2\/}}, \\ 
{\rm{deposit-alist-value}}\,({\it{x\/}}, {\it{bindings1\/}}, {\it{temp-stk\/}})\index{deposit-alist-value})\-\index{deposit-alist-value})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable deposit-alist-value-commute2.

\addvspace{18pt}

\begin{verbatim};; %deposits commute
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                    ;;
;;                     %Map-Down-Values Commutes                      ;;
;;                                                                    ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

\end{verbatim}\begin{tabbing}{\sc Theorem}:  map-down-values-deposit-alist-value-commute \\ \index{map-down-values-deposit-alist-v!alue-commute}
\=\+(\=\+{\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\rm{cons}}\,({\it{x\/}}, {\it{lst\/}}))\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\rm{cons}}\,({\it{x\/}}, {\it{lst\/}}), {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\rm{cons}}\,({\it{x\/}}, {\it{lst\/}}))\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{cons}}\,({\it{x\/}}, {\it{lst\/}}))\index{all-cars-unique})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{map-down-values}}\,(\=\+{\it{lst\/}}, \\ 
{\it{bindings\/}}, \\ 
{\rm{deposit-alist-value}}\,({\it{x\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{deposit-alist-value})\-\index{map-down-values} \\ 
$=$$\;\;\;\;${\rm{deposit-alist-value}}\,(\=\+{\it{x\/}}, \\ 
{\it{bindings\/}}, \\ 
{\rm{map-down-values}}\,({\it{lst\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{map-down-values})\-\index{deposit-alist-value})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  deposit-temp-map-down-values-commute \\ \index{deposit-temp-map-down-values-co!mmute}
\=\+(\=\+{\rm{all-cars-unique}}\,({\rm{cons}}\,({\it{x\/}}, {\it{lst\/}}))\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\rm{cons}}\,({\it{x\/}}, {\it{lst\/}}))\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\rm{cons}}\,({\it{x\/}}, {\it{lst\/}}))\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\rm{cons}}\,({\it{x\/}}, {\it{lst\/}}), {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{deposit-temp}}\,(\=\+{\it{y\/}}, \\ 
{\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{x\/}}), {\it{bindings\/}})), \\ 
{\rm{map-down-values}}\,({\it{lst\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{map-down-values})\-\index{deposit-temp} \\ 
$=$$\;\;\;\;${\rm{map-down-values}}\,(\=\+{\it{lst\/}}, \\ 
{\it{bindings\/}}, \\ 
{\rm{deposit-temp}}\,(\=\+{\it{y\/}}, \\ 
{\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{x\/}}), {\it{bindings\/}})), \\ 
{\it{temp-stk\/}})\-\index{deposit-temp})\-\index{map-down-values})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable deposit-temp-map-down-values-commute.

\addvspace{18pt}


\noindent{\sc Event}:   Disable no-p-aliasing.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  deposit-temp-map-down-values-commute-2 \\ \index{deposit-temp-map-down-values-co!mmute-2}
\=\+(\=\+{\rm{all-cars-unique}}\,({\rm{cons}}\,({\it{x\/}}, {\it{lst\/}}))\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\rm{cons}}\,({\it{x\/}}, {\it{lst\/}}))\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\rm{cons}}\,({\it{x\/}}, {\it{lst\/}}))\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\rm{cons}}\,({\it{x\/}}, {\it{lst\/}}), {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{map-down-values}}\,(\=\+{\it{lst\/}}, \\ 
{\it{bindings\/}}, \\ 
{\rm{deposit-temp}}\,({\it{y\/}}, {\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{x\/}}), {\it{bindings\/}})), {\it{temp-stk\/}})\index{deposit-temp})\-\index{map-down-values} \\ 
$=$$\;\;\;\;${\rm{deposit-temp}}\,(\=\+{\it{y\/}}, \\ 
{\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{x\/}}), {\it{bindings\/}})), \\ 
{\rm{map-down-values}}\,({\it{lst\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{map-down-values})\-\index{deposit-temp})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable deposit-temp-map-down-values-commute-2.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  deposit-same-value-doesnt-disturb-map-down-values \\ \index{deposit-same-value-doesnt-distu!rb-map-down-values}
\=\+(\=\+{\rm{mg-vars-list-ok-in-p-state}}\,({\it{mg-vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\it{mg-vars\/}})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\it{mg-vars\/}})\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\it{mg-vars\/}})\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\in$ {\rm{listcars}}\,({\it{mg-vars\/}})\index{listcars}) \\ 
$\wedge$$\;\;\;\;${\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\rm{assoc}}\,({\it{x\/}}, {\it{mg-vars\/}})))\index{simple-mg-type-refp})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{rput}}\,(\=\+{\rm{mg-to-p-simple-literal}}\,({\rm{caddr}}\,({\rm{assoc}}\,({\it{x\/}}, {\it{mg-vars\/}})))\index{mg-to-p-simple-literal}, \\ 
{\rm{untag}}\,({\rm{cdr}}\,({\rm{assoc}}\,({\it{x\/}}, {\it{bindings\/}})))\index{untag}, \\ 
{\rm{map-down-values}}\,({\it{mg-vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{map-down-values})\-\index{rput} \\ 
$=$$\;\;\;\;${\rm{map-down-values}}\,({\it{mg-vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{map-down-values})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable deposit-same-value-doesnt-disturb-map-down-values.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  deposit-same-array-value-doesnt-disturb-map-down-values \\ \index{deposit-same-array-value-doesnt!-disturb-map-down-values}
\=\+(\=\+{\rm{mg-vars-list-ok-in-p-state}}\,({\it{mg-vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\it{mg-vars\/}})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\it{mg-vars\/}})\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\it{mg-vars\/}})\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\in$ {\rm{listcars}}\,({\it{mg-vars\/}})\index{listcars}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\rm{assoc}}\,({\it{x\/}}, {\it{mg-vars\/}})))\index{simple-mg-type-refp}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{deposit-array-value}}\,(\=\+{\rm{caddr}}\,({\rm{assoc}}\,({\it{x\/}}, {\it{mg-vars\/}})), \\ 
{\rm{cdr}}\,({\rm{assoc}}\,({\it{x\/}}, {\it{bindings\/}})), \\ 
{\rm{map-down-values}}\,({\it{mg-vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{map-down-values})\-\index{deposit-array-value} \\ 
$=$$\;\;\;\;${\rm{map-down-values}}\,({\it{mg-vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{map-down-values})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable deposit-same-array-value-doesnt-disturb-map-down-values.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  deposit-same-value-doesnt-disturb-map-down-values2 \\ \index{deposit-same-value-doesnt-distu!rb-map-down-values2}
\=\+(\=\+{\rm{mg-vars-list-ok-in-p-state}}\,({\it{mg-vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\it{mg-vars\/}})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\it{mg-vars\/}})\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\it{mg-vars\/}})\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\in$ {\rm{listcars}}\,({\it{mg-vars\/}})\index{listcars}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\rm{assoc}}\,({\it{x\/}}, {\it{mg-vars\/}})))\index{simple-mg-type-refp}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{rput}}\,(\=\+{\rm{mg-to-p-simple-literal}}\,({\rm{caaddr}}\,({\rm{assoc}}\,({\it{x\/}}, {\it{mg-vars\/}})))\index{mg-to-p-simple-literal}, \\ 
{\rm{untag}}\,({\rm{cdr}}\,({\rm{assoc}}\,({\it{x\/}}, {\it{bindings\/}})))\index{untag}, \\ 
{\rm{map-down-values}}\,({\it{mg-vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{map-down-values})\-\index{rput} \\ 
$=$$\;\;\;\;${\rm{map-down-values}}\,({\it{mg-vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{map-down-values})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  deposit-same-array-value-doesnt-disturb-map-down-values2 \\ \index{deposit-same-array-value-doesnt!-disturb-map-down-values2}
\=\+(\=\+{\rm{mg-vars-list-ok-in-p-state}}\,({\it{mg-vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\it{mg-vars\/}})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\it{mg-vars\/}})\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\it{mg-vars\/}})\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\in$ {\rm{listcars}}\,({\it{mg-vars\/}})\index{listcars}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\rm{assoc}}\,({\it{x\/}}, {\it{mg-vars\/}})))\index{simple-mg-type-refp}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{deposit-array-value}}\,(\=\+{\rm{cdr}}\,({\rm{caddr}}\,({\rm{assoc}}\,({\it{x\/}}, {\it{mg-vars\/}}))), \\ 
{\rm{add1-nat}}\,({\rm{cdr}}\,({\rm{assoc}}\,({\it{x\/}}, {\it{bindings\/}})))\index{add1-nat}, \\ 
{\rm{map-down-values}}\,({\it{mg-vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{map-down-values})\-\index{deposit-array-value} \\ 
$=$$\;\;\;\;${\rm{map-down-values}}\,({\it{mg-vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{map-down-values})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  map-down-values-commutes1 \\ \index{map-down-values-commutes1}
\=\+(\=\+{\rm{all-cars-unique}}\,({\rm{append}}\,({\it{alist1\/}}, {\it{alist2\/}}))\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\rm{append}}\,({\it{alist1\/}}, {\it{alist2\/}}))\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\rm{append}}\,({\it{alist1\/}}, {\it{alist2\/}}))\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\rm{append}}\,({\it{alist1\/}}, {\it{alist2\/}}), {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{map-down-values}}\,(\=\+{\it{alist1\/}}, \\ 
{\it{bindings\/}}, \\ 
{\rm{map-down-values}}\,({\it{alist2\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{map-down-values})\-\index{map-down-values} \\ 
$=$$\;\;\;\;${\rm{map-down-values}}\,(\=\+{\it{alist2\/}}, \\ 
{\it{bindings\/}}, \\ 
{\rm{map-down-values}}\,({\it{alist1\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{map-down-values})\-\index{map-down-values})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  listcars-restriction1 \\ \index{listcars-restriction1}
\=\+(\=\+({\rm{listcars}}\,({\it{alist\/}})\index{listcars} $=$ {\rm{append}}\,({\rm{listcars}}\,({\it{alist1\/}})\index{listcars}, {\rm{listcars}}\,({\it{alist2\/}})\index{listcars})) \\ 
$\wedge$$\;\;\;\;${\rm{plistp}}\,({\it{alist\/}})\index{plistp} \\ 
$\wedge$$\;\;\;\;${\rm{no-duplicates}}\,({\rm{listcars}}\,({\it{alist\/}})\index{listcars})\index{no-duplicates})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{append}}\,(\=\+{\rm{restrict}}\,({\it{alist\/}}, {\rm{listcars}}\,({\it{alist1\/}})\index{listcars})\index{restrict}, \\ 
{\rm{restrict}}\,({\it{alist\/}}, {\rm{listcars}}\,({\it{alist2\/}})\index{listcars})\index{restrict})\- \\ 
$=$$\;\;\;\;${\it{alist\/}})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable listcars-restriction1.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  meaning-restriction-append1 \\ \index{meaning-restriction-append1}
\=\+(\=\+({\rm{listcars}}\,({\it{alist\/}})\index{listcars} $=$ {\rm{append}}\,({\rm{listcars}}\,({\it{alist1\/}})\index{listcars}, {\rm{listcars}}\,({\it{alist2\/}})\index{listcars})) \\ 
$\wedge$$\;\;\;\;${\rm{no-duplicates}}\,({\rm{listcars}}\,({\it{alist\/}})\index{listcars})\index{no-duplicates} \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\it{alist\/}})\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\it{alist\/}})\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{alist\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{map-down-values}}\,({\it{alist\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{map-down-values} \\ 
$=$$\;\;\;\;${\rm{map-down-values}}\,(\=\+{\rm{restrict}}\,({\it{alist\/}}, {\rm{listcars}}\,({\it{alist1\/}})\index{listcars})\index{restrict}, \\ 
{\it{bindings\/}}, \\ 
{\rm{map-down-values}}\,(\=\+{\rm{restrict}}\,(\=\+{\it{alist\/}}, \\ 
{\rm{listcars}}\,({\it{alist2\/}})\index{listcars})\-\index{restrict}, \\ 
{\it{bindings\/}}, \\ 
{\it{temp-stk\/}})\-\index{map-down-values})\-\index{map-down-values})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable meaning-restriction-append1.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  deposit-alist-value-map-down-values-commute2 \\ \index{deposit-alist-value-map-down-va!lues-commute2}
\=\+(\=\+{\rm{no-p-aliasing}}\,({\rm{append}}\,({\it{bindings1\/}}, {\it{bindings2\/}}), {\rm{append}}\,({\it{alist1\/}}, {\it{alist2\/}}))\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{alist1\/}}, {\it{bindings1\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{alist2\/}}, {\it{bindings2\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{append}}\,({\it{alist1\/}}, {\it{alist2\/}}))\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{append}}\,({\it{bindings1\/}}, {\it{bindings2\/}}))\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{plistp}}\,({\it{alist1\/}})\index{plistp} \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\rm{append}}\,({\it{alist1\/}}, {\it{alist2\/}}))\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\in$ {\it{alist1\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{deposit-alist-value}}\,(\=\+{\it{x\/}}, \\ 
{\it{bindings1\/}}, \\ 
{\rm{map-down-values}}\,({\it{alist2\/}}, {\it{bindings2\/}}, {\it{temp-stk\/}})\index{map-down-values})\-\index{deposit-alist-value} \\ 
$=$$\;\;\;\;${\rm{map-down-values}}\,(\=\+{\it{alist2\/}}, \\ 
{\it{bindings2\/}}, \\ 
{\rm{deposit-alist-value}}\,({\it{x\/}}, {\it{bindings1\/}}, {\it{temp-stk\/}})\index{deposit-alist-value})\-\index{map-down-values})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable deposit-alist-value-map-down-values-commute2.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  map-down-values-commute \\ \index{map-down-values-commute}
\=\+(\=\+{\rm{all-cars-unique}}\,({\rm{append}}\,({\it{alist1\/}}, {\it{alist2\/}}))\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{append}}\,({\it{bindings1\/}}, {\it{bindings2\/}}))\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{plistp}}\,({\it{alist1\/}})\index{plistp} \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\rm{append}}\,({\it{alist1\/}}, {\it{alist2\/}}))\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\rm{append}}\,({\it{bindings1\/}}, {\it{bindings2\/}}), {\rm{append}}\,({\it{alist1\/}}, {\it{alist2\/}}))\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{alist1\/}}, {\it{bindings1\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{alist2\/}}, {\it{bindings2\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{map-down-values}}\,(\=\+{\it{alist1\/}}, \\ 
{\it{bindings1\/}}, \\ 
{\rm{map-down-values}}\,({\it{alist2\/}}, {\it{bindings2\/}}, {\it{temp-stk\/}})\index{map-down-values})\-\index{map-down-values} \\ 
$=$$\;\;\;\;${\rm{map-down-values}}\,(\=\+{\it{alist2\/}}, \\ 
{\it{bindings2\/}}, \\ 
{\rm{map-down-values}}\,({\it{alist1\/}}, {\it{bindings1\/}}, {\it{temp-stk\/}})\index{map-down-values})\-\index{map-down-values})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable map-down-values-commute.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  deposit-temp-doesnt-affect-map-down-values \\ \index{deposit-temp-doesnt-affect-map-!down-values}
\=\+(\=\+{\rm{mg-alistp}}\,({\rm{cons}}\,({\it{x\/}}, {\it{mg-vars\/}}))\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{cons}}\,({\it{x\/}}, {\it{mg-vars\/}}))\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\rm{cons}}\,({\it{x\/}}, {\it{mg-vars\/}}))\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\rm{cons}}\,({\it{x\/}}, {\it{mg-vars\/}}), {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{map-down-values}}\,(\=\+{\it{mg-vars\/}}, \\ 
{\it{bindings\/}}, \\ 
{\rm{deposit-temp}}\,(\=\+{\it{value\/}}, \\ 
{\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{x\/}}), {\it{bindings\/}})), \\ 
{\it{temp-stk\/}})\-\index{deposit-temp})\-\index{map-down-values} \\ 
$=$$\;\;\;\;${\rm{deposit-temp}}\,(\=\+{\it{value\/}}, \\ 
{\rm{cdr}}\,({\rm{assoc}}\,({\rm{car}}\,({\it{x\/}}), {\it{bindings\/}})), \\ 
{\rm{map-down-values}}\,({\it{mg-vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{map-down-values})\-\index{deposit-temp})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable deposit-temp-doesnt-affect-map-down-values.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{rget-array-mapping-induction-hi!nt} \\  
\=\+{\rm{rget-array-mapping-induction-hint}}\,({\it{value\/}}, {\it{index\/}}, {\it{nat\/}}, {\it{temp-stk\/}})\index{rget-array-mapping-induction-hi!nt} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{value\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\it{index\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{rget-array-mapping-induction-hint}}\,(\=\+{\rm{cdr}}\,({\it{value\/}}), \\ 
{\it{index\/}} $-\;1$, \\ 
{\rm{add1-nat}}\,({\it{nat\/}})\index{add1-nat}, \\ 
{\rm{deposit-temp}}\,(\=\+{\rm{mg-to-p-simple-literal}}\,({\rm{car}}\,({\it{value\/}}))\index{mg-to-p-simple-literal}, \\ 
{\it{nat\/}}, \\ 
{\it{temp-stk\/}})\-\index{deposit-temp})\-\index{rget-array-mapping-induction-hi!nt}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  rget-array-index-mapping0 \\ \index{rget-array-index-mapping0}
\=\+(\=\+(({\rm{untag}}\,({\it{nat\/}})\index{untag} $+$ ({\rm{length}}\,({\it{value\/}})\index{length} $-\;1$)) $<$ {\rm{length}}\,({\it{temp-stk\/}})\index{length}) \\ 
$\wedge$$\;\;\;\;$({\rm{untag}}\,({\it{nat\/}})\index{untag} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $<$ {\rm{length}}\,({\it{value\/}})\index{length}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{rget}}\,({\rm{untag}}\,({\it{nat\/}})\index{untag} $+$ {\it{index\/}}, {\rm{deposit-array-value}}\,({\it{value\/}}, {\it{nat\/}}, {\it{temp-stk\/}})\index{deposit-array-value})\index{rget} \\ 
$=$$\;\;\;\;${\rm{mg-to-p-simple-literal}}\,({\rm{get}}\,({\it{index\/}}, {\it{value\/}})\index{get})\index{mg-to-p-simple-literal})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  rget-array-index-mapping \\ \index{rget-array-index-mapping}
\=\+(\=\+{\rm{mg-alistp}}\,({\it{mg-vars\/}})\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\it{mg-vars\/}})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\it{mg-vars\/}})\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{array-identifierp}}\,({\it{a\/}}, {\it{mg-vars\/}})\index{array-identifierp} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{mg-vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $<$ {\rm{array-length}}\,({\rm{cadr}}\,({\rm{assoc}}\,({\it{a\/}}, {\it{mg-vars\/}})))\index{array-length}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{rget}}\,(\=\+{\rm{untag}}\,({\rm{value}}\,({\it{a\/}}, {\it{bindings\/}})\index{value})\index{untag} $+$ {\it{index\/}}, \\ 
{\rm{map-down-values}}\,({\it{mg-vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{map-down-values})\-\index{rget} \\ 
$=$$\;\;\;\;${\rm{mg-to-p-simple-literal}}\,({\rm{get}}\,({\it{index\/}}, {\rm{caddr}}\,({\rm{assoc}}\,({\it{a\/}}, {\it{mg-vars\/}})))\index{get})\index{mg-to-p-simple-literal})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable rget-array-index-mapping.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  append-doesnt-affect-rput \\ \index{append-doesnt-affect-rput}
\=\+({\it{i\/}} $<$ {\rm{length}}\,({\it{lst2\/}})\index{length}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{rput}}\,({\it{value\/}}, {\it{i\/}}, {\rm{append}}\,({\it{lst1\/}}, {\it{lst2\/}}))\index{rput} $=$ {\rm{append}}\,({\it{lst1\/}}, {\rm{rput}}\,({\it{value\/}}, {\it{i\/}}, {\it{lst2\/}})\index{rput}))\-
\end{tabbing}


\noindent{\sc Event}:   Disable append-doesnt-affect-rput.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  append-doesnt-affect-deposit-temp \\ \index{append-doesnt-affect-deposit-te!mp}
\=\+(\=\+{\rm{definedp}}\,({\it{b\/}}, {\it{mg-vars\/}})\index{definedp} \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\it{mg-vars\/}})\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{mg-vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{deposit-temp}}\,(\=\+{\it{value\/}}, \\ 
{\rm{cdr}}\,({\rm{assoc}}\,({\it{b\/}}, {\it{bindings\/}})), \\ 
{\rm{append}}\,({\it{lst\/}}, {\rm{map-down-values}}\,({\it{mg-vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{map-down-values}))\-\index{deposit-temp} \\ 
$=$$\;\;\;\;${\rm{append}}\,(\=\+{\it{lst\/}}, \\ 
{\rm{deposit-temp}}\,(\=\+{\it{value\/}}, \\ 
{\rm{cdr}}\,({\rm{assoc}}\,({\it{b\/}}, {\it{bindings\/}})), \\ 
{\rm{map-down-values}}\,({\it{mg-vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{map-down-values})\-\index{deposit-temp})\-)\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable append-doesnt-affect-deposit-temp.

\addvspace{18pt}


\begin{verbatim};; %map-down-values commutes
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                    ;;
;;                %Ascending-Local-Address-Sequence                   ;;
;;                                                                    ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; This function is used to describe the addresses pushed for the locals upon 
;; entry to a procedure call.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{ascending-local-address-sequence} \\  
\=\+{\rm{ascending-local-address-sequence}}\,({\it{locals\/}}, {\it{n\/}})\index{ascending-local-address-sequence} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{locals\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf elseif }{\rm{simple-mg-type-refp}}\,({\rm{formal-type}}\,({\rm{car}}\,({\it{locals\/}}))\index{formal-type})\index{simple-mg-type-refp} \\ 
{\bf then }{\rm{cons}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{nat}}, {\it{n\/}})\index{tag}, \\ 
{\rm{ascending-local-address-sequence}}\,({\rm{cdr}}\,({\it{locals\/}}), $1\;+$ {\it{n\/}})\index{ascending-local-address-sequence})\- \\ 
{\bf else }{\rm{cons}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{nat}}, {\it{n\/}})\index{tag}, \\ 
{\rm{ascending-local-address-sequence}}\,(\=\+{\rm{cdr}}\,({\it{locals\/}}), \\ 
\=\+{\rm{array-length}}\,({\rm{formal-type}}\,({\rm{car}}\,({\it{locals\/}}))\index{formal-type})\index{array-length} \\ 
$+$$\;\;\;\;${\it{n\/}}\-)\-\index{ascending-local-address-sequence})\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  length-ascending-local-address-sequence \\ \index{length-ascending-local-address-!sequence}
{\rm{length}}\,({\rm{ascending-local-address-sequence}}\,({\it{locals\/}}, {\it{k\/}})\index{ascending-local-address-sequence})\index{length} $=$ {\rm{length}}\,({\it{locals\/}})\index{length}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ascending-local-address-sequence-plistp \\ \index{ascending-local-address-sequence!-plistp}
{\rm{plistp}}\,({\rm{ascending-local-address-sequence}}\,({\it{x\/}}, {\it{y\/}})\index{ascending-local-address-sequence})\index{plistp}
\end{tabbing}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                    ;;
;;                   %All-Pointer-Smaller/Bigger                      ;;
;;                                                                    ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; These functions are used strictly in the proof that there is no-p-aliasing 
;; in the call environment.  
;; The previous version assumed that the pointers were still in the bindings.
;; This version assumes that we've applied the function collect-pointers and 
;; therefore have a list of numberp's.  

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{all-pointers-smaller} \\  
\=\+{\rm{all-pointers-smaller}}\,({\it{lst\/}}, {\it{n\/}})\index{all-pointers-smaller} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{lst\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }({\rm{car}}\,({\it{lst\/}}) $<$ {\it{n\/}}) $\wedge$ {\rm{all-pointers-smaller}}\,({\rm{cdr}}\,({\it{lst\/}}), {\it{n\/}})\index{all-pointers-smaller}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-pointers-smaller-distributes \\ \index{all-pointers-smaller-distribute!s}
\=\+{\rm{all-pointers-smaller}}\,({\rm{append}}\,({\it{lst1\/}}, {\it{lst2\/}}), {\it{n\/}})\index{all-pointers-smaller} \\ 
$=$$\;\;\;\;$({\rm{all-pointers-smaller}}\,({\it{lst1\/}}, {\it{n\/}})\index{all-pointers-smaller} $\wedge$ {\rm{all-pointers-smaller}}\,({\it{lst2\/}}, {\it{n\/}})\index{all-pointers-smaller})\-
\end{tabbing}


\noindent{\sc Event}:   Disable all-pointers-smaller-distributes.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{all-pointers-bigger} \\  
\=\+{\rm{all-pointers-bigger}}\,({\it{lst\/}}, {\it{n\/}})\index{all-pointers-bigger} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{lst\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }({\it{n\/}} $\leq$ {\rm{car}}\,({\it{lst\/}})) $\wedge$ {\rm{all-pointers-bigger}}\,({\rm{cdr}}\,({\it{lst\/}}), {\it{n\/}})\index{all-pointers-bigger}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-pointers-bigger-distributes \\ \index{all-pointers-bigger-distributes}
\=\+{\rm{all-pointers-bigger}}\,({\rm{append}}\,({\it{lst1\/}}, {\it{lst2\/}}), {\it{n\/}})\index{all-pointers-bigger} \\ 
$=$$\;\;\;\;$({\rm{all-pointers-bigger}}\,({\it{lst1\/}}, {\it{n\/}})\index{all-pointers-bigger} $\wedge$ {\rm{all-pointers-bigger}}\,({\it{lst2\/}}, {\it{n\/}})\index{all-pointers-bigger})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  pointers-bigger-monotonic \\ \index{pointers-bigger-monotonic}
(({\it{m\/}} $\not<$ {\it{n\/}}) $\wedge$ {\rm{all-pointers-bigger}}\,({\it{x\/}}, {\it{m\/}})\index{all-pointers-bigger}) $\rightarrow$ {\rm{all-pointers-bigger}}\,({\it{x\/}}, {\it{n\/}})\index{all-pointers-bigger}
\end{tabbing}


\noindent{\sc Event}:   Disable pointers-bigger-monotonic.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  all-pointers-smaller-member \\ \index{all-pointers-smaller-member}
(({\it{i\/}} $\not<$ {\it{n\/}}) $\wedge$ {\rm{all-pointers-smaller}}\,({\it{lst\/}}, {\it{n\/}})\index{all-pointers-smaller}) $\rightarrow$ ({\it{i\/}} $\not\in$ {\it{lst\/}})
\end{tabbing}


\noindent{\sc Event}:   Disable all-pointers-smaller-member.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  all-pointers-bigger-member \\ \index{all-pointers-bigger-member}
(({\it{i\/}} $<$ {\it{n\/}}) $\wedge$ {\rm{all-pointers-bigger}}\,({\it{lst\/}}, {\it{n\/}})\index{all-pointers-bigger}) $\rightarrow$ ({\it{i\/}} $\not\in$ {\it{lst\/}})
\end{tabbing}


\noindent{\sc Event}:   Disable all-pointers-bigger-member.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{successive-pointers-bigger-indu!ction-hint} \\  
\=\+{\rm{successive-pointers-bigger-induction-hint}}\,({\it{nat\/}}, {\it{n\/}}, {\it{m\/}})\index{successive-pointers-bigger-indu!ction-hint} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{m\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{successive-pointers-bigger-induction-hint}}\,(\=\+{\rm{add1-nat}}\,({\it{nat\/}})\index{add1-nat}, \\ 
$1\;+$ {\it{n\/}}, \\ 
{\it{m\/}} $-\;1$)\-\index{successive-pointers-bigger-indu!ction-hint}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  successive-pointers-bigger0 \\ \index{successive-pointers-bigger0}
\=\+({\it{nat\/}} $=$ {\rm{tag}}\,({\tt{'}}{\tt{nat}}, {\it{n\/}})\index{tag}) \\ 
$\rightarrow$$\;\;\;\;${\rm{all-pointers-bigger}}\,({\rm{n-successive-pointers}}\,({\it{nat\/}}, {\it{m\/}})\index{n-successive-pointers}, {\it{n\/}})\index{all-pointers-bigger}\-
\end{tabbing}


\noindent{\sc Event}:   Disable successive-pointers-bigger0.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  successive-pointers-bigger \\ \index{successive-pointers-bigger}
{\rm{all-pointers-bigger}}\,({\rm{n-successive-pointers}}\,({\rm{tag}}\,({\tt{'}}{\tt{nat}}, {\it{n\/}})\index{tag}, {\it{m\/}})\index{n-successive-pointers}, {\it{n\/}})\index{all-pointers-bigger}
\end{tabbing}


\noindent{\sc Event}:   Disable successive-pointers-bigger.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  no-duplicates-all-pointers-disjoint \\ \index{no-duplicates-all-pointers-disj!oint}
\=\+(\=\+{\rm{no-duplicates}}\,({\it{lst1\/}})\index{no-duplicates} \\ 
$\wedge$$\;\;\;\;${\rm{no-duplicates}}\,({\it{lst2\/}})\index{no-duplicates} \\ 
$\wedge$$\;\;\;\;${\rm{all-pointers-smaller}}\,({\it{lst2\/}}, {\it{n\/}})\index{all-pointers-smaller} \\ 
$\wedge$$\;\;\;\;${\rm{all-pointers-bigger}}\,({\it{lst1\/}}, {\it{n\/}})\index{all-pointers-bigger})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{no-duplicates}}\,({\rm{append}}\,({\it{lst1\/}}, {\it{lst2\/}}))\index{no-duplicates}\-
\end{tabbing}


\noindent{\sc Event}:   Disable no-duplicates-all-pointers-disjoint.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  no-duplicates-all-pointers-disjoint2 \\ \index{no-duplicates-all-pointers-disj!oint2}
\=\+(\=\+{\rm{no-duplicates}}\,({\it{lst1\/}})\index{no-duplicates} \\ 
$\wedge$$\;\;\;\;${\rm{no-duplicates}}\,({\it{lst2\/}})\index{no-duplicates} \\ 
$\wedge$$\;\;\;\;${\rm{all-pointers-smaller}}\,({\it{lst1\/}}, {\it{n\/}})\index{all-pointers-smaller} \\ 
$\wedge$$\;\;\;\;${\rm{all-pointers-bigger}}\,({\it{lst2\/}}, {\it{n\/}})\index{all-pointers-bigger})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{no-duplicates}}\,({\rm{append}}\,({\it{lst1\/}}, {\it{lst2\/}}))\index{no-duplicates}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  successive-pointers-smaller2 \\ \index{successive-pointers-smaller2}
\=\+(({\rm{untag}}\,({\it{nat\/}})\index{untag} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{k\/}} $\not<$ ({\rm{untag}}\,({\it{nat\/}})\index{untag} $+$ {\it{m\/}}))) \\ 
$\rightarrow$$\;\;\;\;${\rm{all-pointers-smaller}}\,({\rm{n-successive-pointers}}\,({\it{nat\/}}, {\it{m\/}})\index{n-successive-pointers}, {\it{k\/}})\index{all-pointers-smaller}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  no-p-aliasing-append1 \\ \index{no-p-aliasing-append1}
\=\+(\=\+{\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\it{lst1\/}})\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\it{lst2\/}})\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{all-pointers-bigger}}\,({\rm{collect-pointers}}\,({\it{bindings\/}}, {\it{lst1\/}})\index{collect-pointers}, {\it{n\/}})\index{all-pointers-bigger} \\ 
$\wedge$$\;\;\;\;${\rm{all-pointers-smaller}}\,({\rm{collect-pointers}}\,({\it{bindings\/}}, {\it{lst2\/}})\index{collect-pointers}, {\it{n\/}})\index{all-pointers-smaller})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\rm{append}}\,({\it{lst1\/}}, {\it{lst2\/}}))\index{no-p-aliasing}\-
\end{tabbing}


\noindent{\sc Event}:   Disable no-p-aliasing-append1.

\addvspace{18pt}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                    ;;
;;                        %Mapping Data Up                            ;;
;;                                                                    ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; The list of mg-vars is of the form (... (cons name (cons value type)) ...)
;; and the p-vars of the form (... (cons name value) ...).  This takes the
;; p-vars and maps them up to the corresponding mg-vars list.  Using the types
;; to give the value-value mapping.

;; In mapping up from the Piton to the MG world, I need to know the signatures of
;; the variables at the lower level but not their values.  This returns a value 
;; which is just like the variable alist but has all of the values set to (false).

;; The map up from Piton to MG world now has a layer of indirection.  That is, 
;; the variable in the Piton world contains an address to the value in the 
;; my-stack array.

;; Notice that the other stuff which may appear on an alist entry is 
;; not preserved.
;; Notice that the value of the Piton variable is actually on the
;; my-stack data structure.  Consequently, we require a "fetch" into
;; that data structure to get it.  Thus, we must have the Piton state
;; p-data-segment as a parameter to the map-up-vars functions.

;; Every local in the bindings of the top frame contains a natural which is
;; an index into the temp-stk where the actual value is stored.

;; This should be removed when I have the opportunity to redo the events and 
;; adjust for this difference.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{map-up-vars-list-array} \\  
\=\+{\rm{map-up-vars-list-array}}\,({\it{p-var\/}}, {\it{temp-stk\/}}, {\it{var-signature\/}})\index{map-up-vars-list-array} \\ 
$=$$\;\;\;\;${\rm{list}}\,(\=\+{\rm{car}}\,({\it{var-signature\/}}), \\ 
{\rm{cadr}}\,({\it{var-signature\/}}), \\ 
{\rm{p-to-mg-simple-literal-list}}\,(\=\+{\rm{fetch-n-temp-stk-elements}}\,(\=\+{\it{temp-stk\/}}, \\ 
{\rm{cdr}}\,({\it{p-var\/}}), \\ 
{\rm{array-length}}\,({\rm{cadr}}\,({\it{var-signature\/}}))\index{array-length})\-\index{fetch-n-temp-stk-elements}, \\ 
{\rm{array-elemtype}}\,({\rm{cadr}}\,({\it{var-signature\/}}))\index{array-elemtype})\-\index{p-to-mg-simple-literal-list})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable map-up-vars-list-array.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{map-up-vars-list-simple-element} \\  
\=\+{\rm{map-up-vars-list-simple-element}}\,({\it{p-var\/}}, {\it{temp-stk\/}}, {\it{var-signature\/}})\index{map-up-vars-list-simple-element} \\ 
$=$$\;\;\;\;${\rm{list}}\,(\=\+{\rm{car}}\,({\it{var-signature\/}}), \\ 
{\rm{cadr}}\,({\it{var-signature\/}}), \\ 
{\rm{p-to-mg-simple-literal}}\,(\=\+{\rm{fetch-temp}}\,({\rm{cdr}}\,({\it{p-var\/}}), {\it{temp-stk\/}})\index{fetch-temp}, \\ 
{\rm{cadr}}\,({\it{var-signature\/}}))\-\index{p-to-mg-simple-literal})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable map-up-vars-list-simple-element.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{map-up-vars-list-element} \\  
\=\+{\rm{map-up-vars-list-element}}\,({\it{p-var\/}}, {\it{temp-stk\/}}, {\it{var-signature\/}})\index{map-up-vars-list-element} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\it{var-signature\/}}))\index{simple-mg-type-refp} \\ 
{\bf then }{\rm{map-up-vars-list-simple-element}}\,({\it{p-var\/}}, {\it{temp-stk\/}}, {\it{var-signature\/}})\index{map-up-vars-list-simple-element} \\ 
{\bf else }{\rm{map-up-vars-list-array}}\,({\it{p-var\/}}, {\it{temp-stk\/}}, {\it{var-signature\/}})\index{map-up-vars-list-array}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};; p-vars here is the bindings component from the topmost frame of the
;; P-CTRL-STK.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{map-up-vars-list} \\  
\=\+{\rm{map-up-vars-list}}\,({\it{p-vars\/}}, {\it{temp-stk\/}}, {\it{signature\/}})\index{map-up-vars-list} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{signature\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{cons}}\,(\=\+{\rm{map-up-vars-list-element}}\,(\=\+{\rm{assoc}}\,({\rm{caar}}\,({\it{signature\/}}), {\it{p-vars\/}}), \\ 
{\it{temp-stk\/}}, \\ 
{\rm{car}}\,({\it{signature\/}}))\-\index{map-up-vars-list-element}, \\ 
{\rm{map-up-vars-list}}\,({\it{p-vars\/}}, {\it{temp-stk\/}}, {\rm{cdr}}\,({\it{signature\/}}))\index{map-up-vars-list})\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};; The mg-state is computed from the p-state by tranforming the value of the
;; global int variable 'c-c to an mg condition.  The vars are mapped up and 
;; given the corresponding values in the mg-state.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{piton-cc} \\  
{\rm{piton-cc}}\,({\it{p\/}})\index{piton-cc} $=$ {\rm{fetch-adp}}\,({\tt{'}}{\tt{(}}{\tt{c-c}}{\tt{ .\ }}{\tt{0}}{\tt{)}}, {\rm{p-data-segment}}\,({\it{p\/}})\index{p-data-segment})\index{fetch-adp}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{map-up} \\  
\=\+{\rm{map-up}}\,({\it{p-state\/}}, {\it{mg-signature\/}}, {\it{cond-list\/}})\index{map-up} \\ 
$=$$\;\;\;\;${\rm{mg-state}}\,(\=\+{\rm{p-nat-to-mg-cond}}\,({\rm{piton-cc}}\,({\it{p-state\/}})\index{piton-cc}, {\it{cond-list\/}})\index{p-nat-to-mg-cond}, \\ 
{\rm{map-up-vars-list}}\,(\=\+{\rm{bindings}}\,({\rm{top}}\,({\rm{p-ctrl-stk}}\,({\it{p-state\/}})\index{p-ctrl-stk})\index{top})\index{bindings}, \\ 
{\rm{p-temp-stk}}\,({\it{p-state\/}})\index{p-temp-stk}, \\ 
{\it{mg-signature\/}})\-\index{map-up-vars-list}, \\ 
{\tt{'}}{\tt{run}})\-\index{mg-state}\-
\end{tabbing}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                    ;;
;;                     %Map Up Inverts Map Down                       ;;
;;                                                                    ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

\end{verbatim}\begin{tabbing}{\sc Theorem}:  definedp-car-cons2 \\ \index{definedp-car-cons2}
{\rm{listp}}\,({\it{y\/}}) $\rightarrow$ {\rm{definedp}}\,({\rm{caar}}\,({\it{y\/}}), {\rm{cons}}\,({\it{x\/}}, {\it{y\/}}))\index{definedp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  put-doesnt-affect-get \\ \index{put-doesnt-affect-get}
\=\+(\=\+({\it{n\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{m\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $<$ {\rm{length}}\,({\it{z\/}})\index{length}) \\ 
$\wedge$$\;\;\;\;$({\it{m\/}} $<$ {\rm{length}}\,({\it{z\/}})\index{length}) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not=$ {\it{m\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{get}}\,({\it{n\/}}, {\rm{put}}\,({\it{x\/}}, {\it{m\/}}, {\it{z\/}})\index{put})\index{get} $=$ {\rm{get}}\,({\it{n\/}}, {\it{z\/}})\index{get})\-
\end{tabbing}


\noindent{\sc Event}:   Disable put-doesnt-affect-get.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  rput-doesnt-affect-rget \\ \index{rput-doesnt-affect-rget}
\=\+(\=\+({\it{n\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{m\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $<$ {\rm{length}}\,({\it{z\/}})\index{length}) \\ 
$\wedge$$\;\;\;\;$({\it{m\/}} $<$ {\rm{length}}\,({\it{z\/}})\index{length}) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not=$ {\it{m\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{rget}}\,({\it{n\/}}, {\rm{rput}}\,({\it{x\/}}, {\it{m\/}}, {\it{z\/}})\index{rput})\index{rget} $=$ {\rm{rget}}\,({\it{n\/}}, {\it{z\/}})\index{rget})\-
\end{tabbing}


\noindent{\sc Event}:   Disable rput-doesnt-affect-rget.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  deposit-temp-doesnt-affect-fetch-temp \\ \index{deposit-temp-doesnt-affect-fetc!h-temp}
\=\+(\=\+({\rm{untag}}\,({\it{nat1\/}})\index{untag} $\not=$ {\rm{untag}}\,({\it{nat2\/}})\index{untag}) \\ 
$\wedge$$\;\;\;\;$({\rm{untag}}\,({\it{nat1\/}})\index{untag} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\rm{untag}}\,({\it{nat2\/}})\index{untag} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\rm{untag}}\,({\it{nat1\/}})\index{untag} $<$ {\rm{length}}\,({\it{temp-stk\/}})\index{length}) \\ 
$\wedge$$\;\;\;\;$({\rm{untag}}\,({\it{nat2\/}})\index{untag} $<$ {\rm{length}}\,({\it{temp-stk\/}})\index{length}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{fetch-temp}}\,({\it{nat1\/}}, {\rm{deposit-temp}}\,({\it{value\/}}, {\it{nat2\/}}, {\it{temp-stk\/}})\index{deposit-temp})\index{fetch-temp} \\ 
$=$$\;\;\;\;${\rm{fetch-temp}}\,({\it{nat1\/}}, {\it{temp-stk\/}})\index{fetch-temp})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable deposit-temp-doesnt-affect-fetch-temp.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  deposit-array-value-doesnt-affect-fetch-temp \\ \index{deposit-array-value-doesnt-affe!ct-fetch-temp}
\=\+(\=\+({\rm{untag}}\,({\it{nat1\/}})\index{untag} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\rm{untag}}\,({\it{nat2\/}})\index{untag} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\rm{untag}}\,({\it{nat1\/}})\index{untag} $\not\in$ {\rm{n-successive-pointers}}\,({\it{nat2\/}}, {\rm{length}}\,({\it{value\/}})\index{length})\index{n-successive-pointers}) \\ 
$\wedge$$\;\;\;\;$({\rm{untag}}\,({\it{nat1\/}})\index{untag} $<$ {\rm{length}}\,({\it{temp-stk\/}})\index{length}) \\ 
$\wedge$$\;\;\;\;$(({\rm{untag}}\,({\it{nat2\/}})\index{untag} $+$ ({\rm{length}}\,({\it{value\/}})\index{length} $-\;1$)) $<$ {\rm{length}}\,({\it{temp-stk\/}})\index{length}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{fetch-temp}}\,({\it{nat1\/}}, {\rm{deposit-array-value}}\,({\it{value\/}}, {\it{nat2\/}}, {\it{temp-stk\/}})\index{deposit-array-value})\index{fetch-temp} \\ 
$=$$\;\;\;\;${\rm{fetch-temp}}\,({\it{nat1\/}}, {\it{temp-stk\/}})\index{fetch-temp})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable deposit-array-value-doesnt-affect-fetch-temp.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  deposit-temp-doesnt-affect-fetch-n-temp-stk-elements \\ \index{deposit-temp-doesnt-affect-fetc!h-n-temp-stk-elements}
\=\+(\=\+({\rm{untag}}\,({\it{nat1\/}})\index{untag} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\rm{untag}}\,({\it{nat2\/}})\index{untag} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\rm{untag}}\,({\it{nat2\/}})\index{untag} $\not\in$ {\rm{n-successive-pointers}}\,({\it{nat1\/}}, {\it{n\/}})\index{n-successive-pointers}) \\ 
$\wedge$$\;\;\;\;$({\rm{untag}}\,({\it{nat2\/}})\index{untag} $<$ {\rm{length}}\,({\it{temp-stk\/}})\index{length}) \\ 
$\wedge$$\;\;\;\;$(({\rm{untag}}\,({\it{nat1\/}})\index{untag} $+$ ({\it{n\/}} $-\;1$)) $<$ {\rm{length}}\,({\it{temp-stk\/}})\index{length}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{fetch-n-temp-stk-elements}}\,({\rm{deposit-temp}}\,({\it{x\/}}, {\it{nat2\/}}, {\it{temp-stk\/}})\index{deposit-temp}, {\it{nat1\/}}, {\it{n\/}})\index{fetch-n-temp-stk-elements} \\ 
$=$$\;\;\;\;${\rm{fetch-n-temp-stk-elements}}\,({\it{temp-stk\/}}, {\it{nat1\/}}, {\it{n\/}})\index{fetch-n-temp-stk-elements})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable deposit-temp-doesnt-affect-fetch-n-temp-stk-elements.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  deposit-array-value-doesnt-affect-fetch-n-temp-stk-elements \\ \index{deposit-array-value-doesnt-affe!ct-fetch-n-temp-stk-elements}
\=\+(\=\+({\rm{untag}}\,({\it{nat1\/}})\index{untag} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\rm{untag}}\,({\it{nat2\/}})\index{untag} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$(({\rm{untag}}\,({\it{nat2\/}})\index{untag} $+$ ({\it{n\/}} $-\;1$)) $<$ {\rm{length}}\,({\it{temp-stk\/}})\index{length}) \\ 
$\wedge$$\;\;\;\;$(({\rm{untag}}\,({\it{nat1\/}})\index{untag} $+$ ({\rm{length}}\,({\it{value\/}})\index{length} $-\;1$)) $<$ {\rm{length}}\,({\it{temp-stk\/}})\index{length}) \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,(\=\+{\rm{n-successive-pointers}}\,({\it{nat1\/}}, {\rm{length}}\,({\it{value\/}})\index{length})\index{n-successive-pointers}, \\ 
{\rm{n-successive-pointers}}\,({\it{nat2\/}}, {\it{n\/}})\index{n-successive-pointers})\-\index{disjoint})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{fetch-n-temp-stk-elements}}\,(\=\+{\rm{deposit-array-value}}\,({\it{value\/}}, {\it{nat1\/}}, {\it{temp-stk\/}})\index{deposit-array-value}, \\ 
{\it{nat2\/}}, \\ 
{\it{n\/}})\-\index{fetch-n-temp-stk-elements} \\ 
$=$$\;\;\;\;${\rm{fetch-n-temp-stk-elements}}\,({\it{temp-stk\/}}, {\it{nat2\/}}, {\it{n\/}})\index{fetch-n-temp-stk-elements})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable deposit-array-value-doesnt-affect-fetch-n-temp-stk-elements.

\addvspace{18pt}


\begin{tabbing}{\sc Theorem}:  deposit-at-lesser-index-doesnt-affect-fetch \\ \index{deposit-at-lesser-index-doesnt-!affect-fetch}
\=\+(\=\+({\rm{untag}}\,({\it{nat1\/}})\index{untag} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\rm{untag}}\,({\it{nat1\/}})\index{untag} $<$ {\rm{untag}}\,({\it{nat2\/}})\index{untag}) \\ 
$\wedge$$\;\;\;\;$(({\rm{untag}}\,({\it{nat2\/}})\index{untag} $+$ ({\it{n\/}} $-\;1$)) $<$ {\rm{length}}\,({\it{temp-stk\/}})\index{length}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{fetch-n-temp-stk-elements}}\,({\rm{deposit-temp}}\,({\it{x\/}}, {\it{nat1\/}}, {\it{temp-stk\/}})\index{deposit-temp}, {\it{nat2\/}}, {\it{n\/}})\index{fetch-n-temp-stk-elements} \\ 
$=$$\;\;\;\;${\rm{fetch-n-temp-stk-elements}}\,({\it{temp-stk\/}}, {\it{nat2\/}}, {\it{n\/}})\index{fetch-n-temp-stk-elements})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable deposit-at-lesser-index-doesnt-affect-fetch.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  append-doesnt-affect-rget \\ \index{append-doesnt-affect-rget}
\=\+({\it{n\/}} $<$ {\rm{length}}\,({\it{temp-stk\/}})\index{length}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{rget}}\,({\it{n\/}}, {\rm{append}}\,({\it{lst\/}}, {\it{temp-stk\/}}))\index{rget} $=$ {\rm{rget}}\,({\it{n\/}}, {\it{temp-stk\/}})\index{rget})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  append-doesnt-affect-rget-corollary \\ \index{append-doesnt-affect-rget-corol!lary}
\=\+({\it{n\/}} $<$ {\rm{length}}\,({\it{temp-stk\/}})\index{length}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{rget}}\,({\it{n\/}}, {\rm{push}}\,({\it{x\/}}, {\it{temp-stk\/}})\index{push})\index{rget} $=$ {\rm{rget}}\,({\it{n\/}}, {\it{temp-stk\/}})\index{rget})\-
\end{tabbing}


\begin{tabbing}{\sc Definition}:\index{fetch-temp-stk-elements-inducti!on-hint} \\  
\=\+{\rm{fetch-temp-stk-elements-induction-hint}}\,({\it{value\/}}, {\it{temp-stk\/}}, {\it{nat\/}}, {\it{n\/}})\index{fetch-temp-stk-elements-inducti!on-hint} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{value\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{fetch-temp-stk-elements-induction-hint}}\,(\=\+{\rm{cdr}}\,({\it{value\/}}), \\ 
{\it{temp-stk\/}}, \\ 
{\rm{add1-nat}}\,({\it{nat\/}})\index{add1-nat}, \\ 
{\it{n\/}} $-\;1$)\-\index{fetch-temp-stk-elements-inducti!on-hint}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  fetch-n-temp-stk-elements-inverts-deposit-array-value \\ \index{fetch-n-temp-stk-elements-invert!s-deposit-array-value}
\=\+(\=\+({\it{n\/}} $=$ {\rm{length}}\,({\it{value\/}})\index{length}) \\ 
$\wedge$$\;\;\;\;$({\rm{untag}}\,({\it{nat\/}})\index{untag} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$(({\rm{untag}}\,({\it{nat\/}})\index{untag} $+$ ({\rm{length}}\,({\it{value\/}})\index{length} $-\;1$)) $<$ {\rm{length}}\,({\it{temp-stk\/}})\index{length}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{fetch-n-temp-stk-elements}}\,(\=\+{\rm{deposit-array-value}}\,({\it{value\/}}, {\it{nat\/}}, {\it{temp-stk\/}})\index{deposit-array-value}, \\ 
{\it{nat\/}}, \\ 
{\it{n\/}})\-\index{fetch-n-temp-stk-elements} \\ 
$=$$\;\;\;\;${\rm{mg-to-p-simple-literal-list}}\,({\it{value\/}})\index{mg-to-p-simple-literal-list})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable fetch-n-temp-stk-elements-inverts-deposit-array-value.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  simple-vars-have-simple-values \\ \index{simple-vars-have-simple-values}
\=\+({\rm{mg-alist-elementp}}\,({\it{x\/}})\index{mg-alist-elementp} $\wedge$ {\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\it{x\/}}))\index{simple-mg-type-refp}) \\ 
$\rightarrow$$\;\;\;\;${\rm{simple-typed-literalp}}\,({\rm{caddr}}\,({\it{x\/}}), {\rm{cadr}}\,({\it{x\/}}))\index{simple-typed-literalp}\-
\end{tabbing}


\noindent{\sc Event}:   Disable simple-vars-have-simple-values.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  array-vars-have-simple-plistp-values \\ \index{array-vars-have-simple-plistp-v!alues}
\=\+({\rm{mg-alist-elementp}}\,({\it{x\/}})\index{mg-alist-elementp} $\wedge$ ($\neg$ {\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\it{x\/}}))\index{simple-mg-type-refp})) \\ 
$\rightarrow$$\;\;\;\;${\rm{simple-typed-literal-plistp}}\,({\rm{caddr}}\,({\it{x\/}}), {\rm{array-elemtype}}\,({\rm{cadr}}\,({\it{x\/}}))\index{array-elemtype})\index{simple-typed-literal-plistp}\-
\end{tabbing}


\noindent{\sc Event}:   Disable array-vars-have-simple-plistp-values.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  map-up-map-down-preserves-mg-alist-elements-equal \\ \index{map-up-map-down-preserves-mg-ali!st-elements-equal}
\=\+(\=\+({\it{mg-vars\/}} $\not\simeq\;${{\bf{nil}}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\it{mg-vars\/}})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\it{mg-vars\/}})\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\it{mg-vars\/}})\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{mg-vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{map-up-vars-list-element}}\,(\=\+{\rm{assoc}}\,({\rm{caar}}\,({\it{mg-vars\/}}), {\it{bindings\/}}), \\ 
{\rm{map-down-values}}\,({\it{mg-vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{map-down-values}, \\ 
{\rm{list}}\,({\rm{caar}}\,({\it{mg-vars\/}}), {\rm{cadar}}\,({\it{mg-vars\/}})))\-\index{map-up-vars-list-element} \\ 
$=$$\;\;\;\;${\rm{car}}\,({\it{mg-vars\/}}))\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable map-up-map-down-preserves-mg-alist-elements-equal.

\addvspace{18pt}

\begin{verbatim};; The proof of this should really be "packaged" up into the four
;; cases depending on which of x and (car mg-vars) are simple or not.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  deposit-alist-value-doesnt-affect-map-up-vars-list0 \\ \index{deposit-alist-value-doesnt-affe!ct-map-up-vars-list0}
\=\+(\=\+{\rm{all-cars-unique}}\,({\rm{cons}}\,({\it{x\/}}, {\it{mg-vars\/}}))\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\rm{cons}}\,({\it{x\/}}, {\it{mg-vars\/}}))\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\rm{cons}}\,({\it{x\/}}, {\it{mg-vars\/}}), {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\rm{cons}}\,({\it{x\/}}, {\it{mg-vars\/}}))\index{no-p-aliasing})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{map-up-vars-list}}\,(\=\+{\it{bindings\/}}, \\ 
{\rm{deposit-alist-value}}\,({\it{x\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{deposit-alist-value}, \\ 
{\rm{signature}}\,({\it{mg-vars\/}})\index{signature})\-\index{map-up-vars-list} \\ 
$=$$\;\;\;\;${\rm{map-up-vars-list}}\,({\it{bindings\/}}, {\it{temp-stk\/}}, {\rm{signature}}\,({\it{mg-vars\/}})\index{signature})\index{map-up-vars-list})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable deposit-alist-value-doesnt-affect-map-up-vars-list0.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  deposit-alist-value-doesnt-affect-map-up-vars-list \\ \index{deposit-alist-value-doesnt-affe!ct-map-up-vars-list}
\=\+(\=\+{\rm{all-cars-unique}}\,({\rm{cons}}\,({\it{x\/}}, {\it{mg-vars\/}}))\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\rm{cons}}\,({\it{x\/}}, {\it{mg-vars\/}}))\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\rm{cons}}\,({\it{x\/}}, {\it{mg-vars\/}}), {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\rm{cons}}\,({\it{x\/}}, {\it{mg-vars\/}}))\index{no-p-aliasing})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{map-up-vars-list}}\,(\=\+{\it{bindings\/}}, \\ 
{\rm{map-down-values}}\,(\=\+{\it{mg-vars\/}}, \\ 
{\it{bindings\/}}, \\ 
{\rm{deposit-alist-value}}\,(\=\+{\it{x\/}}, \\ 
{\it{bindings\/}}, \\ 
{\it{temp-stk\/}})\-\index{deposit-alist-value})\-\index{map-down-values}, \\ 
{\rm{signature}}\,({\it{mg-vars\/}})\index{signature})\-\index{map-up-vars-list} \\ 
$=$$\;\;\;\;${\rm{map-up-vars-list}}\,(\=\+{\it{bindings\/}}, \\ 
{\rm{map-down-values}}\,({\it{mg-vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{map-down-values}, \\ 
{\rm{signature}}\,({\it{mg-vars\/}})\index{signature})\-\index{map-up-vars-list})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable deposit-alist-value-doesnt-affect-map-up-vars-list.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  rget-rewrite1 \\ \index{rget-rewrite1}
\=\+(\=\+{\rm{mg-alistp}}\,({\it{mg-vars\/}})\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\it{mg-vars\/}})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\it{mg-vars\/}})\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{simple-identifierp}}\,({\it{y\/}}, {\it{mg-vars\/}})\index{simple-identifierp} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{mg-vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{rget}}\,(\=\+{\rm{untag}}\,({\rm{value}}\,({\it{y\/}}, {\it{bindings\/}})\index{value})\index{untag}, \\ 
{\rm{map-down-values}}\,({\it{mg-vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{map-down-values})\-\index{rget} \\ 
$=$$\;\;\;\;${\rm{mg-to-p-simple-literal}}\,({\rm{caddr}}\,({\rm{assoc}}\,({\it{y\/}}, {\it{mg-vars\/}})))\index{mg-to-p-simple-literal})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  set-alist-value-deposit-temp-relation \\ \index{set-alist-value-deposit-temp-re!lation}
\=\+(\=\+{\rm{mg-alistp}}\,({\it{mg-vars\/}})\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\it{mg-vars\/}})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\it{mg-vars\/}})\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{simple-identifierp}}\,({\it{y\/}}, {\it{mg-vars\/}})\index{simple-identifierp} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{mg-vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-valuep}}\,({\it{value\/}}, {\rm{cadr}}\,({\rm{assoc}}\,({\it{y\/}}, {\it{mg-vars\/}})))\index{ok-mg-valuep})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{map-down-values}}\,({\rm{set-alist-value}}\,({\it{y\/}}, {\it{value\/}}, {\it{mg-vars\/}})\index{set-alist-value}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{map-down-values} \\ 
$=$$\;\;\;\;${\rm{rput}}\,(\=\+{\rm{mg-to-p-simple-literal}}\,({\it{value\/}})\index{mg-to-p-simple-literal}, \\ 
{\rm{untag}}\,({\rm{value}}\,({\it{y\/}}, {\it{bindings\/}})\index{value})\index{untag}, \\ 
{\rm{map-down-values}}\,({\it{mg-vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{map-down-values})\-\index{rput})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable set-alist-value-deposit-temp-relation.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  set-alist-value-deposit-array-value-relation \\ \index{set-alist-value-deposit-array-v!alue-relation}
\=\+(\=\+{\rm{mg-alistp}}\,({\it{mg-vars\/}})\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\it{mg-vars\/}})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\it{mg-vars\/}})\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{array-identifierp}}\,({\it{a\/}}, {\it{mg-vars\/}})\index{array-identifierp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-array-value}}\,({\it{lst\/}}, {\rm{cadr}}\,({\rm{assoc}}\,({\it{a\/}}, {\it{mg-vars\/}})))\index{ok-mg-array-value} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{mg-vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{map-down-values}}\,({\rm{set-alist-value}}\,({\it{a\/}}, {\it{lst\/}}, {\it{mg-vars\/}})\index{set-alist-value}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{map-down-values} \\ 
$=$$\;\;\;\;${\rm{deposit-array-value}}\,(\=\+{\it{lst\/}}, \\ 
{\rm{value}}\,({\it{a\/}}, {\it{bindings\/}})\index{value}, \\ 
{\rm{map-down-values}}\,({\it{mg-vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{map-down-values})\-\index{deposit-array-value})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable set-alist-value-deposit-array-value-relation.

\addvspace{18pt}


\begin{tabbing}{\sc Theorem}:  append-doesnt-affect-deposit-alist-value \\ \index{append-doesnt-affect-deposit-ali!st-value}
\=\+({\rm{car}}\,({\it{x\/}}) $\in$ {\rm{listcars}}\,({\it{bindings1\/}})\index{listcars}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{deposit-alist-value}}\,({\it{x\/}}, {\rm{append}}\,({\it{bindings1\/}}, {\it{bindings2\/}}), {\it{temp-stk\/}})\index{deposit-alist-value} \\ 
$=$$\;\;\;\;${\rm{deposit-alist-value}}\,({\it{x\/}}, {\it{bindings1\/}}, {\it{temp-stk\/}})\index{deposit-alist-value})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  deposit-temp-length-cons \\ \index{deposit-temp-length-cons}
\=\+{\rm{plistp}}\,({\it{temp-stk\/}})\index{plistp} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{deposit-temp}}\,({\it{x\/}}, {\rm{tag}}\,({\tt{'}}{\tt{nat}}, {\rm{length}}\,({\it{temp-stk\/}})\index{length})\index{tag}, {\rm{cons}}\,({\it{y\/}}, {\it{temp-stk\/}}))\index{deposit-temp} \\ 
$=$$\;\;\;\;${\rm{cons}}\,({\it{x\/}}, {\it{temp-stk\/}}))\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable deposit-temp-length-cons.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{deposit-array-value-same-value-i!nduction-hint} \\  
\=\+{\rm{deposit-array-value-same-value-induction-hint}}\,({\it{array-value\/}}, {\it{temp-stk\/}})\index{deposit-array-value-same-value-i!nduction-hint} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{array-value\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{deposit-array-value-same-value-induction-hint}}\,(\=\+{\rm{cdr}}\,({\it{array-value\/}}), \\ 
{\rm{deposit-temp}}\,(\=\+{\rm{mg-to-p-simple-literal}}\,({\rm{car}}\,({\it{array-value\/}}))\index{mg-to-p-simple-literal}, \\ 
{\rm{tag}}\,(\=\+{\tt{'}}{\tt{nat}}, \\ 
{\rm{length}}\,({\it{temp-stk\/}})\index{length})\-\index{tag}, \\ 
{\rm{cons}}\,(\=\+{\rm{mg-to-p-simple-literal}}\,({\rm{car}}\,({\it{array-value\/}}))\index{mg-to-p-simple-literal}, \\ 
{\it{temp-stk\/}})\-)\-\index{deposit-temp})\-\index{deposit-array-value-same-value-i!nduction-hint}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  deposit-temp-preserves-plistp \\ \index{deposit-temp-preserves-plistp}
{\rm{plistp}}\,({\it{z\/}})\index{plistp} $\rightarrow$ {\rm{plistp}}\,({\rm{deposit-temp}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{deposit-temp})\index{plistp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  deposit-array-value-same-value-doesnt-disturb-temp-stk \\ \index{deposit-array-value-same-value-!doesnt-disturb-temp-stk}
\=\+{\rm{plistp}}\,({\it{temp-stk\/}})\index{plistp} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{deposit-array-value}}\,(\=\+{\it{array-value\/}}, \\ 
{\rm{tag}}\,({\tt{'}}{\tt{nat}}, {\rm{length}}\,({\it{temp-stk\/}})\index{length})\index{tag}, \\ 
{\rm{append}}\,(\=\+{\it{lst\/}}, \\ 
{\rm{append}}\,(\=\+{\rm{reverse}}\,({\rm{mg-to-p-simple-literal-list}}\,({\it{array-value\/}})\index{mg-to-p-simple-literal-list})\index{reverse}, \\ 
{\it{temp-stk\/}})\-)\-)\-\index{deposit-array-value} \\ 
$=$$\;\;\;\;${\rm{append}}\,(\=\+{\it{lst\/}}, \\ 
{\rm{append}}\,(\=\+{\rm{reverse}}\,({\rm{mg-to-p-simple-literal-list}}\,({\it{array-value\/}})\index{mg-to-p-simple-literal-list})\index{reverse}, \\ 
{\it{temp-stk\/}})\-)\-)\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable deposit-array-value-same-value-doesnt-disturb-temp-stk.

\addvspace{18pt}


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

\addvspace{18pt}

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