\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{"c-predefined4"}}.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  fetch-label-0-case-2 \\ \index{fetch-label-0-case-2}
\=\+{\rm{cdr}}\,({\rm{assoc}}\,({\it{cc\/}}, {\rm{cons}}\,({\tt{'}}{\tt{(}}{\tt{routineerror}}{\tt{ .\ }}{\tt{0}}{\tt{)}}, {\rm{make-label-alist}}\,({\it{lst\/}}, {\tt{0}})\index{make-label-alist}))) \\ 
$=$$\;\;\;\;${\tt{0}}\-
\end{tabbing}


\noindent{\sc Event}:   Disable fetch-label-0-case-2.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  mg-cond-to-p-nat-p-objectp-type-nat \\ \index{mg-cond-to-p-nat-p-objectp-type!-nat}
\=\+(\=\+({\rm{length}}\,({\it{cond-list\/}})\index{length} $<$ ((({\rm{exp}}\,({\tt{2}}, {\sc{mg-word-size}}\index{mg-word-size})\index{exp} $-\;1$) $-\;1$) $-\;1$)) \\ 
$\wedge$$\;\;\;\;$({\rm{p-word-size}}\,({\it{state\/}})\index{p-word-size} $=$ {\sc{mg-word-size}}\index{mg-word-size}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{p-objectp-type}}\,({\tt{'}}{\tt{nat}}, {\rm{mg-cond-to-p-nat}}\,({\it{cc\/}}, {\it{cond-list\/}})\index{mg-cond-to-p-nat}, {\it{state\/}})\index{p-objectp-type}\-
\end{tabbing}


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

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  mg-cond-to-p-nat-index-lessp \\ \index{mg-cond-to-p-nat-index-lessp}
\=\+({\rm{length}}\,({\it{lst\/}})\index{length} $<$ {\it{n\/}}) \\ 
$\rightarrow$$\;\;\;\;$(({\rm{untag}}\,({\rm{mg-cond-to-p-nat}}\,({\it{c\/}}, {\it{lst\/}})\index{mg-cond-to-p-nat})\index{untag} $<$ ($1\;+$ ($1\;+$ {\it{n\/}}))) $=$ {\bf{t}})\-
\end{tabbing}


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

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  set-alist-value-map-down-values-length-doesnt-shrink \\ \index{set-alist-value-map-down-values!-length-doesnt-shrink}
\=\+({\rm{mg-vars-list-ok-in-p-state}}\,({\it{x\/}}, {\it{bindings\/}}, {\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}}\,(\=\+{\rm{set-alist-value}}\,({\it{name\/}}, {\it{value\/}}, {\it{x\/}})\index{set-alist-value}, \\ 
{\it{bindings\/}}, \\ 
{\it{temp-stk\/}})\-\index{map-down-values})\index{length} \\ 
$<$$\;\;\;\;${\rm{length}}\,({\rm{map-down-values}}\,({\it{x\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{map-down-values})\index{length})\- \\ 
$=$$\;\;\;\;${\bf{f}})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable set-alist-value-map-down-values-length-doesnt-shrink.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  extra-bindings-doesnt-affect-formal-types-preserved \\ \index{extra-bindings-doesnt-affect-fo!rmal-types-preserved}
\=\+({\rm{car}}\,({\it{x\/}}) $\not\in$ {\rm{listcars}}\,({\it{y\/}})\index{listcars}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{formal-types-preserved}}\,({\it{y\/}}, {\rm{cons}}\,({\it{x\/}}, {\it{z\/}}))\index{formal-types-preserved} $=$ {\rm{formal-types-preserved}}\,({\it{y\/}}, {\it{z\/}})\index{formal-types-preserved})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  not-simple-identifiers-array-identifiers \\ \index{not-simple-identifiers-array-ide!ntifiers}
\=\+(\=\+{\rm{definedp}}\,({\it{x\/}}, {\it{alist\/}})\index{definedp} \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\it{alist\/}})\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{simple-identifierp}}\,({\it{x\/}}, {\it{alist\/}})\index{simple-identifierp}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{array-identifierp}}\,({\it{x\/}}, {\it{alist\/}})\index{array-identifierp}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mg-meaning-preserves-signatures-match2 \\ \index{mg-meaning-preserves-signatures!-match2}
\=\+{\rm{plistp}}\,({\it{alist\/}})\index{plistp} \\ 
$\rightarrow$$\;\;\;\;${\rm{signatures-match}}\,(\=\+{\it{alist\/}}, \\ 
{\rm{mg-alist}}\,({\rm{mg-meaning}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{mg-state}}\,({\it{cc\/}}, {\it{alist\/}}, {\it{psw\/}})\index{mg-state}, \\ 
{\it{n\/}})\-\index{mg-meaning})\index{mg-alist})\-\index{signatures-match}\-
\end{tabbing}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                           ;;
;;                             PROCEDURE CALLS                               ;;
;;                                                                           ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

\end{verbatim}
\noindent{\sc Event}:   Disable make-cond-list.

\addvspace{18pt}

\noindent{\sc Event}:   Disable make-call-var-alist.

\addvspace{18pt}

\noindent{\sc Event}:   Disable mg-var-ok-in-p-state.

\addvspace{18pt}

\noindent{\sc Event}:   Enable proc-call-code.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  proc-call-meaning-r-2 \\ \index{proc-call-meaning-r-2}
\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{proc-call-mg}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{mg-meaning-r}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}}, {\it{sizes\/}})\index{mg-meaning-r} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{signal-system-error}}\,({\it{mg-state\/}}, {\tt{'}}{\tt{timed-out}})\index{signal-system-error} \\ 
{\bf elseif }$\neg$ {\rm{normal}}\,({\it{mg-state\/}})\index{normal}$\;\;${\bf then }{\it{mg-state\/}} \\ 
{\bf elseif }{\rm{resources-inadequatep}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{sizes\/}})\index{resources-inadequatep} \\ 
{\bf then }{\rm{signal-system-error}}\,({\it{mg-state\/}}, {\tt{'}}{\tt{resource-error}})\index{signal-system-error} \\ 
{\bf else }{\rm{map-call-effects}}\,(\=\+{\rm{mg-meaning-r}}\,(\=\+{\rm{def-body}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-body}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{make-call-environment}}\,(\=\+{\it{mg-state\/}}, \\ 
{\it{stmt\/}}, \\ 
{\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\-\index{make-call-environment}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\rm{list}}\,(\=\+\=\+{\rm{t-size}}\,({\it{sizes\/}})\index{t-size} \\ 
$+$$\;\;\;\;${\rm{data-length}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{data-length}\-, \\ 
\=\+{\rm{c-size}}\,({\it{sizes\/}})\index{c-size} \\ 
$+$$\;\;\;\;$(\=\+{\tt{2}} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{length} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\rm{def-formals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-formals})\index{length})\-\-)\-)\-\index{mg-meaning-r}, \\ 
{\rm{fetch-called-def}}\,({\it{stmt\/}}, {\it{proc-list\/}})\index{fetch-called-def}, \\ 
{\it{stmt\/}}, \\ 
{\it{mg-state\/}})\-\index{map-call-effects}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  call-translation-2 \\ \index{call-translation-2}
\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{proc-call-mg}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{translate}}\,({\it{cinfo\/}}, {\it{cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}})\index{translate} \\ 
$=$$\;\;\;\;${\rm{make-cinfo}}\,(\=\+{\rm{append}}\,(\=\+{\rm{code}}\,({\it{cinfo\/}})\index{code}, \\ 
{\rm{proc-call-code}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{stmt\/}}, \\ 
{\it{cond-list\/}}, \\ 
{\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals}, \\ 
{\rm{length}}\,({\rm{def-cond-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-cond-locals})\index{length})\-\index{proc-call-code})\-, \\ 
{\rm{label-alist}}\,({\it{cinfo\/}})\index{label-alist}, \\ 
\=\+{\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt} \\ 
$+$$\;\;\;\;$($1\;+$ ($1\;+$ {\rm{length}}\,({\rm{call-conds}}\,({\it{stmt\/}})\index{call-conds})\index{length}))\-)\-\index{make-cinfo})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  locals-pointers-bigger0 \\ \index{locals-pointers-bigger0}
\=\+{\rm{all-cars-unique}}\,({\it{locals\/}})\index{all-cars-unique} \\ 
$\rightarrow$$\;\;\;\;${\rm{all-pointers-bigger}}\,(\=\+{\rm{collect-pointers}}\,({\rm{map-call-locals}}\,({\it{locals\/}}, {\it{n\/}})\index{map-call-locals}, {\it{locals\/}})\index{collect-pointers}, \\ 
{\it{n\/}})\-\index{all-pointers-bigger}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  no-p-aliasing-locals \\ \index{no-p-aliasing-locals}
\=\+(({\it{n\/}} $\in\;${\bf{N}}${}$) $\wedge$ {\rm{all-cars-unique}}\,({\it{locals\/}})\index{all-cars-unique}) \\ 
$\rightarrow$$\;\;\;\;${\rm{no-p-aliasing}}\,({\rm{map-call-locals}}\,({\it{locals\/}}, {\it{n\/}})\index{map-call-locals}, {\it{locals\/}})\index{no-p-aliasing}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  map-call-formals-all-pointers-smaller3 \\ \index{map-call-formals-all-pointers-s!maller3}
\=\+(\=\+{\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{all-cars-unique}}\,({\it{formals\/}})\index{all-cars-unique} \\ 
$\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{all-pointers-smaller}}\,(\=\+{\rm{collect-pointers}}\,(\=\+{\rm{map-call-formals}}\,(\=\+{\it{formals\/}}, \\ 
{\it{actuals\/}}, \\ 
{\it{bindings\/}})\-\index{map-call-formals}, \\ 
{\rm{make-call-param-alist}}\,(\=\+{\it{formals\/}}, \\ 
{\it{actuals\/}}, \\ 
{\it{mg-vars\/}})\-\index{make-call-param-alist})\-\index{collect-pointers}, \\ 
{\rm{length}}\,({\it{temp-stk\/}})\index{length})\-\index{all-pointers-smaller}\-
\end{tabbing}

\begin{verbatim};; These got lost somewhere

\end{verbatim}\begin{tabbing}{\sc Theorem}:  array-alist-element-lengths-match \\ \index{array-alist-element-lengths-mat!ch}
\=\+(\=\+{\rm{mg-alistp}}\,({\it{mg-vars\/}})\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;${\rm{definedp}}\,({\it{x\/}}, {\it{mg-vars\/}})\index{definedp} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\rm{assoc}}\,({\it{x\/}}, {\it{mg-vars\/}})))\index{simple-mg-type-refp}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{length}}\,({\rm{caddr}}\,({\rm{assoc}}\,({\it{x\/}}, {\it{mg-vars\/}})))\index{length} \\ 
$=$$\;\;\;\;${\rm{array-length}}\,({\rm{cadr}}\,({\rm{assoc}}\,({\it{x\/}}, {\it{mg-vars\/}})))\index{array-length})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable array-alist-element-lengths-match.

\addvspace{18pt}


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

\addvspace{18pt}

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

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

\begin{tabbing}{\sc Theorem}:  actual-pointers-distinct \\ \index{actual-pointers-distinct}
\=\+(\=\+{\rm{ok-actual-params-list}}\,({\it{actuals\/}}, {\it{mg-vars\/}})\index{ok-actual-params-list} \\ 
$\wedge$$\;\;\;\;${\rm{defined-identifierp}}\,({\it{x\/}}, {\it{mg-vars\/}})\index{defined-identifierp} \\ 
$\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{all-cars-unique}}\,({\it{mg-vars\/}})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{no-duplicates}}\,({\rm{cons}}\,({\it{x\/}}, {\it{actuals\/}}))\index{no-duplicates} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\it{mg-vars\/}})\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\it{formals\/}})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\it{mg-vars\/}})\index{mg-alistp})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{untag}}\,({\rm{cdr}}\,({\rm{assoc}}\,({\it{x\/}}, {\it{bindings\/}})))\index{untag} \\ 
$\not\in$$\;\;\;\;${\rm{collect-pointers}}\,(\=\+{\rm{map-call-formals}}\,({\it{formals\/}}, {\it{actuals\/}}, {\it{bindings\/}})\index{map-call-formals}, \\ 
{\rm{make-call-param-alist}}\,(\=\+{\it{formals\/}}, \\ 
{\it{actuals\/}}, \\ 
{\it{mg-vars\/}})\-\index{make-call-param-alist})\-\index{collect-pointers})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  actual-pointers-distinct2 \\ \index{actual-pointers-distinct2}
\=\+(\=\+{\rm{ok-actual-params-list}}\,({\it{actuals\/}}, {\it{mg-vars\/}})\index{ok-actual-params-list} \\ 
$\wedge$$\;\;\;\;${\rm{defined-identifierp}}\,({\it{x\/}}, {\it{mg-vars\/}})\index{defined-identifierp} \\ 
$\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{all-cars-unique}}\,({\it{mg-vars\/}})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{no-duplicates}}\,({\rm{cons}}\,({\it{x\/}}, {\it{actuals\/}}))\index{no-duplicates} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\it{mg-vars\/}})\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\it{formals\/}})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\it{mg-vars\/}})\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\rm{assoc}}\,({\it{x\/}}, {\it{mg-vars\/}})))\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{mg-vars\/}})))\index{array-length})\-\index{n-successive-pointers}, \\ 
{\rm{collect-pointers}}\,(\=\+{\rm{map-call-formals}}\,({\it{formals\/}}, {\it{actuals\/}}, {\it{bindings\/}})\index{map-call-formals}, \\ 
{\rm{make-call-param-alist}}\,(\=\+{\it{formals\/}}, \\ 
{\it{actuals\/}}, \\ 
{\it{mg-vars\/}})\-\index{make-call-param-alist})\-\index{collect-pointers})\-\index{disjoint}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  no-p-aliasing-formals \\ \index{no-p-aliasing-formals}
\=\+(\=\+{\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{all-cars-unique}}\,({\it{mg-vars\/}})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{no-duplicates}}\,({\it{actuals\/}})\index{no-duplicates} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\it{mg-vars\/}})\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\it{formals\/}})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\it{mg-vars\/}})\index{mg-alistp})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{no-p-aliasing}}\,(\=\+{\rm{map-call-formals}}\,({\it{formals\/}}, {\it{actuals\/}}, {\it{bindings\/}})\index{map-call-formals}, \\ 
{\rm{make-call-param-alist}}\,({\it{formals\/}}, {\it{actuals\/}}, {\it{mg-vars\/}})\index{make-call-param-alist})\-\index{no-p-aliasing}\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  actual-params-list-ok-in-mg-alist \\ \index{actual-params-list-ok-in-mg-ali!st}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{r-cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statep}}\,({\it{mg-state\/}}, {\it{r-cond-list\/}})\index{ok-mg-statep} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{ok-actual-params-list}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}, {\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{ok-actual-params-list}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  data-param-lists-match-in-mg-alist \\ \index{data-param-lists-match-in-mg-ali!st}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{r-cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statep}}\,({\it{mg-state\/}}, {\it{r-cond-list\/}})\index{ok-mg-statep} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{data-param-lists-match}}\,(\=\+{\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}, \\ 
{\rm{def-formals}}\,({\rm{fetch-called-def}}\,({\it{stmt\/}}, {\it{proc-list\/}})\index{fetch-called-def})\index{def-formals}, \\ 
{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\-\index{data-param-lists-match}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  call-local-names-unique \\ \index{call-local-names-unique}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{r-cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{no-duplicates}}\,({\rm{append}}\,(\=\+{\rm{listcars}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{listcars}, \\ 
{\rm{listcars}}\,({\rm{def-formals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-formals})\index{listcars})\-)\index{no-duplicates}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  no-p-aliasing-in-call-environment \\ \index{no-p-aliasing-in-call-environme!nt}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{r-cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statep}}\,({\it{mg-state\/}}, {\it{r-cond-list\/}})\index{ok-mg-statep} \\ 
$\wedge$$\;\;\;\;${\rm{user-defined-procp}}\,({\it{subr\/}}, {\it{proc-list\/}})\index{user-defined-procp} \\ 
$\wedge$$\;\;\;\;${\rm{plistp}}\,({\it{temp-stk\/}})\index{plistp} \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\it{ctrl-stk\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,(\=\+{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, \\ 
{\it{temp-stk\/}})\-\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, {\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{no-p-aliasing}}\,(\=\+{\rm{make-frame-alist}}\,(\=\+{\rm{fetch-called-def}}\,({\it{stmt\/}}, {\it{proc-list\/}})\index{fetch-called-def}, \\ 
{\it{stmt\/}}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\it{temp-stk\/}})\-\index{make-frame-alist}, \\ 
{\rm{make-call-var-alist}}\,(\=\+{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, \\ 
{\it{stmt\/}}, \\ 
{\rm{fetch-called-def}}\,({\it{stmt\/}}, {\it{proc-list\/}})\index{fetch-called-def})\-\index{make-call-var-alist})\-\index{no-p-aliasing}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  call-exact-time-translation-parameters-ok \\ \index{call-exact-time-translation-par!ameters-ok}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{r-cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-translation-parameters}}\,({\it{cinfo\/}}, {\it{t-cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}}, {\it{code2\/}})\index{ok-translation-parameters} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statep}}\,({\it{mg-state\/}}, {\it{r-cond-list\/}})\index{ok-mg-statep})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{ok-translation-parameters}}\,(\=\+{\rm{make-cinfo}}\,(\=\+{\bf{nil}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{routineerror}}{\tt{ .\ }}{\tt{0}}{\tt{)}}, \\ 
{\rm{make-label-alist}}\,(\=\+{\rm{make-cond-list}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{make-cond-list}, \\ 
{\tt{0}})\-\index{make-label-alist})\-, \\ 
{\tt{1}})\-\index{make-cinfo}, \\ 
{\rm{make-cond-list}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{make-cond-list}, \\ 
{\rm{def-body}}\,({\rm{fetch-called-def}}\,({\it{stmt\/}}, {\it{proc-list\/}})\index{fetch-called-def})\index{def-body}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{dl}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{nil}}{\tt{ }}{\tt{(}}{\tt{no-op}}{\tt{)}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\rm{list}}\,(\=\+{\tt{'}}{\tt{pop*}}, \\ 
{\rm{data-length}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{data-length})\-, \\ 
{\tt{'}}{\tt{(}}{\tt{(}}{\tt{ret}}{\tt{)}}{\tt{)}})\-)\-)\-\index{ok-translation-parameters}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  call-body-rewrite \\ \index{call-body-rewrite}
\=\+{\rm{code}}\,({\rm{translate-def-body}}\,({\rm{assoc}}\,({\rm{call-name}}\,({\it{stmt\/}})\index{call-name}, {\it{proc-list\/}}), {\it{proc-list\/}})\index{translate-def-body})\index{code} \\ 
$=$$\;\;\;\;${\rm{append}}\,(\=\+{\rm{code}}\,({\rm{translate}}\,(\=\+{\rm{make-cinfo}}\,(\=\+{\bf{nil}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{routineerror}}{\tt{ .\ }}{\tt{0}}{\tt{)}}, \\ 
{\rm{make-label-alist}}\,(\=\+{\rm{make-cond-list}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{make-cond-list}, \\ 
{\tt{0}})\-\index{make-label-alist})\-, \\ 
{\tt{1}})\-\index{make-cinfo}, \\ 
{\rm{make-cond-list}}\,({\rm{fetch-called-def}}\,({\it{stmt\/}}, {\it{proc-list\/}})\index{fetch-called-def})\index{make-cond-list}, \\ 
{\rm{def-body}}\,({\rm{fetch-called-def}}\,({\it{stmt\/}}, {\it{proc-list\/}})\index{fetch-called-def})\index{def-body}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{dl}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{nil}}{\tt{ }}{\tt{(}}{\tt{no-op}}{\tt{)}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\rm{list}}\,(\=\+{\tt{'}}{\tt{pop*}}, \\ 
{\rm{data-length}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{data-length})\-, \\ 
{\tt{'}}{\tt{(}}{\tt{(}}{\tt{ret}}{\tt{)}}{\tt{)}})\-)\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{mg-locals-list-ok-induction-hint} \\  
\=\+{\rm{mg-locals-list-ok-induction-hint}}\,({\it{locals\/}}, {\it{temp-stk\/}})\index{mg-locals-list-ok-induction-hint} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{locals\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\rm{simple-mg-type-refp}}\,({\rm{cadar}}\,({\it{locals\/}}))\index{simple-mg-type-refp} \\ 
{\bf then }{\rm{mg-locals-list-ok-induction-hint}}\,(\=\+{\rm{cdr}}\,({\it{locals\/}}), \\ 
{\rm{cons}}\,(\=\+{\rm{mg-to-p-simple-literal}}\,({\rm{caddar}}\,({\it{locals\/}}))\index{mg-to-p-simple-literal}, \\ 
{\it{temp-stk\/}})\-)\-\index{mg-locals-list-ok-induction-hint} \\ 
{\bf else }{\rm{mg-locals-list-ok-induction-hint}}\,(\=\+{\rm{cdr}}\,({\it{locals\/}}), \\ 
{\rm{append}}\,(\=\+{\rm{reverse}}\,({\rm{mg-to-p-simple-literal-list}}\,({\rm{caddar}}\,({\it{locals\/}}))\index{mg-to-p-simple-literal-list})\index{reverse}, \\ 
{\it{temp-stk\/}})\-)\-\index{mg-locals-list-ok-induction-hint}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  definedp-caar \\ \index{definedp-caar}
{\rm{definedp}}\,({\it{x\/}}, {\rm{cons}}\,({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}), {\it{z\/}}))\index{definedp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  tag-length-plistp-2 \\ \index{tag-length-plistp-2}
{\rm{length-plistp}}\,({\rm{tag}}\,({\it{x\/}}, {\it{y\/}})\index{tag}, {\tt{2}})\index{length-plistp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mg-locals-list-ok-in-call-environment \\ \index{mg-locals-list-ok-in-call-envir!onment}
\=\+({\rm{all-cars-unique}}\,({\it{locals\/}})\index{all-cars-unique} $\wedge$ {\rm{ok-mg-local-data-plistp}}\,({\it{locals\/}})\index{ok-mg-local-data-plistp}) \\ 
$\rightarrow$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,(\=\+{\it{locals\/}}, \\ 
{\rm{append}}\,(\=\+{\rm{map-call-locals}}\,(\=\+{\it{locals\/}}, \\ 
{\rm{length}}\,({\it{temp-stk\/}})\index{length})\-\index{map-call-locals}, \\ 
{\it{lst\/}})\-, \\ 
{\rm{append}}\,(\=\+{\rm{reverse}}\,({\rm{mg-to-p-local-values}}\,({\it{locals\/}})\index{mg-to-p-local-values})\index{reverse}, \\ 
{\it{temp-stk\/}})\-)\-\index{mg-vars-list-ok-in-p-state}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  simple-formal-ok-for-actual2 \\ \index{simple-formal-ok-for-actual2}
\=\+(\=\+{\rm{definedp}}\,({\it{actual\/}}, {\it{mg-alist\/}})\index{definedp} \\ 
$\wedge$$\;\;\;\;${\rm{data-params-match}}\,({\it{actual\/}}, {\it{formal\/}}, {\it{mg-alist\/}})\index{data-params-match} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{mg-alist\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\it{formal\/}}))\index{simple-mg-type-refp})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{ok-temp-stk-index}}\,({\rm{cdr}}\,({\rm{assoc}}\,({\it{actual\/}}, {\it{bindings\/}})), {\it{temp-stk\/}})\index{ok-temp-stk-index}\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{mg-formals-list-ok-induction-hi!nt} \\  
\=\+{\rm{mg-formals-list-ok-induction-hint}}\,({\it{formals\/}}, {\it{actuals\/}})\index{mg-formals-list-ok-induction-hi!nt} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{formals\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{mg-formals-list-ok-induction-hint}}\,(\=\+{\rm{cdr}}\,({\it{formals\/}}), \\ 
{\rm{cdr}}\,({\it{actuals\/}}))\-\index{mg-formals-list-ok-induction-hi!nt}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  array-formal-ok-for-actual \\ \index{array-formal-ok-for-actual}
\=\+(\=\+{\rm{defined-identifierp}}\,({\it{actual\/}}, {\it{mg-alist\/}})\index{defined-identifierp} \\ 
$\wedge$$\;\;\;\;${\rm{data-params-match}}\,({\it{actual\/}}, {\it{formal\/}}, {\it{mg-alist\/}})\index{data-params-match} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{mg-alist\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\it{formal\/}}))\index{simple-mg-type-refp}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{ok-temp-stk-array-index}}\,(\=\+{\rm{cdr}}\,({\rm{assoc}}\,({\it{actual\/}}, {\it{bindings\/}})), \\ 
{\rm{append}}\,({\it{local-values\/}}, {\it{temp-stk\/}}), \\ 
{\rm{array-length}}\,({\rm{cadr}}\,({\it{formal\/}}))\index{array-length})\-\index{ok-temp-stk-array-index}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mg-formals-list-ok-in-call-environment0 \\ \index{mg-formals-list-ok-in-call-envi!ronment0}
\=\+(\=\+{\rm{all-cars-unique}}\,({\it{formals\/}})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{ok-actual-params-list}}\,({\it{actuals\/}}, {\it{mg-alist\/}})\index{ok-actual-params-list} \\ 
$\wedge$$\;\;\;\;${\rm{data-param-lists-match}}\,({\it{actuals\/}}, {\it{formals\/}}, {\it{mg-alist\/}})\index{data-param-lists-match} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{mg-alist\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,(\=\+{\rm{make-call-param-alist}}\,(\=\+{\it{formals\/}}, \\ 
{\it{actuals\/}}, \\ 
{\it{mg-alist\/}})\-\index{make-call-param-alist}, \\ 
{\rm{map-call-formals}}\,({\it{formals\/}}, {\it{actuals\/}}, {\it{bindings\/}})\index{map-call-formals}, \\ 
{\rm{append}}\,({\it{local-values\/}}, {\it{temp-stk\/}}))\-\index{mg-vars-list-ok-in-p-state}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mg-formals-list-ok-in-call-environment1 \\ \index{mg-formals-list-ok-in-call-envi!ronment1}
\=\+(\=\+{\rm{all-cars-unique}}\,({\it{formals\/}})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\it{mg-alist\/}})\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-actual-params-list}}\,({\it{actuals\/}}, {\it{mg-alist\/}})\index{ok-actual-params-list} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-formal-data-params-plistp}}\,({\it{formals\/}})\index{ok-mg-formal-data-params-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{data-param-lists-match}}\,({\it{actuals\/}}, {\it{formals\/}}, {\it{mg-alist\/}})\index{data-param-lists-match} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{mg-alist\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,(\=\+{\rm{make-call-param-alist}}\,(\=\+{\it{formals\/}}, \\ 
{\it{actuals\/}}, \\ 
{\it{mg-alist\/}})\-\index{make-call-param-alist}, \\ 
{\rm{map-call-formals}}\,({\it{formals\/}}, {\it{actuals\/}}, {\it{bindings\/}})\index{map-call-formals}, \\ 
{\rm{append}}\,(\=\+{\it{local-values\/}}, \\ 
{\rm{map-down-values}}\,(\=\+{\it{mg-alist\/}}, \\ 
{\it{bindings\/}}, \\ 
{\it{temp-stk\/}})\-\index{map-down-values})\-)\-\index{mg-vars-list-ok-in-p-state}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mg-vars-list-ok-in-call-environment \\ \index{mg-vars-list-ok-in-call-environ!ment}
\=\+(\=\+({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resources-inadequatep}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{resources-inadequatep}) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{r-cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-translation-parameters}}\,({\it{cinfo\/}}, {\it{t-cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}}, {\it{code2\/}})\index{ok-translation-parameters} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statep}}\,({\it{mg-state\/}}, {\it{r-cond-list\/}})\index{ok-mg-statep} \\ 
$\wedge$$\;\;\;\;${\rm{cond-subsetp}}\,({\it{r-cond-list\/}}, {\it{t-cond-list\/}})\index{cond-subsetp} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{code}}\,({\rm{translate-def-body}}\,({\rm{assoc}}\,({\it{subr\/}}, {\it{proc-list\/}}), {\it{proc-list\/}})\index{translate-def-body})\index{code} \\ 
$=$$\;\;\;\;${\rm{append}}\,(\=\+{\rm{code}}\,({\rm{translate}}\,({\it{cinfo\/}}, {\it{t-cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}})\index{translate})\index{code}, \\ 
{\it{code2\/}})\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{user-defined-procp}}\,({\it{subr\/}}, {\it{proc-list\/}})\index{user-defined-procp} \\ 
$\wedge$$\;\;\;\;${\rm{plistp}}\,({\it{temp-stk\/}})\index{plistp} \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\it{ctrl-stk\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,(\=\+{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, \\ 
{\it{temp-stk\/}})\-\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, {\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match} \\ 
$\wedge$$\;\;\;\;${\rm{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,(\=\+{\rm{make-call-var-alist}}\,(\=\+{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, \\ 
{\it{stmt\/}}, \\ 
{\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\-\index{make-call-var-alist}, \\ 
{\rm{append}}\,(\=\+{\rm{map-call-locals}}\,(\=\+{\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals}, \\ 
{\rm{length}}\,({\it{temp-stk\/}})\index{length})\-\index{map-call-locals}, \\ 
{\rm{map-call-formals}}\,(\=\+{\rm{def-formals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-formals}, \\ 
{\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{map-call-formals})\-, \\ 
{\rm{append}}\,(\=\+{\rm{reverse}}\,({\rm{mg-to-p-local-values}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{mg-to-p-local-values})\index{reverse}, \\ 
{\rm{map-down-values}}\,(\=\+{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, \\ 
{\it{temp-stk\/}})\-\index{map-down-values})\-)\-\index{mg-vars-list-ok-in-p-state}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  proc-call-doesnt-halt \\ \index{proc-call-doesnt-halt}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{r-cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statep}}\,({\it{mg-state\/}}, {\it{r-cond-list\/}})\index{ok-mg-statep} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,(\=\+{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, \\ 
{\it{temp-stk\/}})\-\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resource-errorp}}\,({\rm{mg-meaning-r}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{resource-errorp}))\- \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{resource-errorp}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{def-body}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-body}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{make-call-environment}}\,(\=\+{\it{mg-state\/}}, \\ 
{\it{stmt\/}}, \\ 
{\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\-\index{make-call-environment}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\rm{append}}\,(\=\+{\rm{reverse}}\,({\rm{mg-to-p-local-values}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{mg-to-p-local-values})\index{reverse}, \\ 
{\rm{map-down-values}}\,(\=\+{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, \\ 
{\it{temp-stk\/}})\-\index{map-down-values})\-)\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\rm{cons}}\,(\=\+{\rm{p-frame}}\,(\=\+{\rm{make-frame-alist}}\,(\=\+{\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def}, \\ 
{\it{stmt\/}}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\it{temp-stk\/}})\-\index{make-frame-alist}, \\ 
{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,(\=\+{\it{subr\/}}, \\ 
$1\;+$ (\=\+{\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} \\ 
$+$$\;\;\;\;${\rm{data-length}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{data-length} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{length} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals})\index{length})\-)\-)\-\index{tag})\-\index{p-frame}, \\ 
{\it{ctrl-stk\/}})\-)\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{resource-errorp})\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  proc-call-doesnt-halt2 \\ \index{proc-call-doesnt-halt2}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{r-cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statep}}\,({\it{mg-state\/}}, {\it{r-cond-list\/}})\index{ok-mg-statep} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,(\=\+{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, \\ 
{\it{temp-stk\/}})\-\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resource-errorp}}\,({\rm{mg-meaning-r}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{resource-errorp}))\- \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{resource-errorp}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{def-body}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-body}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{make-call-environment}}\,(\=\+{\it{mg-state\/}}, \\ 
{\it{stmt\/}}, \\ 
{\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\-\index{make-call-environment}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\rm{list}}\,(\=\+\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length} \\ 
$+$$\;\;\;\;${\rm{data-length}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{data-length}\-, \\ 
\=\+{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size} \\ 
$+$$\;\;\;\;${\tt{2}} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{length} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\rm{def-formals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-formals})\index{length}\-)\-)\-\index{mg-meaning-r})\index{resource-errorp})\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  proc-call-exact-time-hyps \\ \index{proc-call-exact-time-hyps}
\=\+(\=\+({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resources-inadequatep}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{resources-inadequatep}) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{r-cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-translation-parameters}}\,({\it{cinfo\/}}, {\it{t-cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}}, {\it{code2\/}})\index{ok-translation-parameters} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statep}}\,({\it{mg-state\/}}, {\it{r-cond-list\/}})\index{ok-mg-statep} \\ 
$\wedge$$\;\;\;\;${\rm{cond-subsetp}}\,({\it{r-cond-list\/}}, {\it{t-cond-list\/}})\index{cond-subsetp} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{code}}\,({\rm{translate-def-body}}\,({\rm{assoc}}\,({\it{subr\/}}, {\it{proc-list\/}}), {\it{proc-list\/}})\index{translate-def-body})\index{code} \\ 
$=$$\;\;\;\;${\rm{append}}\,(\=\+{\rm{code}}\,({\rm{translate}}\,({\it{cinfo\/}}, {\it{t-cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}})\index{translate})\index{code}, \\ 
{\it{code2\/}})\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{user-defined-procp}}\,({\it{subr\/}}, {\it{proc-list\/}})\index{user-defined-procp} \\ 
$\wedge$$\;\;\;\;${\rm{plistp}}\,({\it{temp-stk\/}})\index{plistp} \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\it{ctrl-stk\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,(\=\+{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, \\ 
{\it{temp-stk\/}})\-\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, {\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match} \\ 
$\wedge$$\;\;\;\;${\rm{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resource-errorp}}\,({\rm{mg-meaning-r}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{resource-errorp}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{ok-mg-statement}}\,(\=\+{\rm{def-body}}\,({\rm{fetch-called-def}}\,({\it{stmt\/}}, {\it{proc-list\/}})\index{fetch-called-def})\index{def-body}, \\ 
{\rm{make-cond-list}}\,({\rm{fetch-called-def}}\,({\it{stmt\/}}, {\it{proc-list\/}})\index{fetch-called-def})\index{make-cond-list}, \\ 
{\rm{make-name-alist}}\,({\rm{fetch-called-def}}\,({\it{stmt\/}}, {\it{proc-list\/}})\index{fetch-called-def})\index{make-name-alist}, \\ 
{\it{proc-list\/}})\-\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{ok-translation-parameters}}\,(\=\+{\rm{make-cinfo}}\,(\=\+{\bf{nil}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}\=\+{\tt{routineerror}} \\ 
{\tt{.\ }}{\tt{0}}{\tt{)}}\-, \\ 
{\rm{make-label-alist}}\,(\=\+{\rm{make-cond-list}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{make-cond-list}, \\ 
{\tt{0}})\-\index{make-label-alist})\-, \\ 
{\tt{1}})\-\index{make-cinfo}, \\ 
{\rm{make-cond-list}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{make-cond-list}, \\ 
{\rm{def-body}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-body}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{dl}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{nil}}{\tt{ }}{\tt{(}}{\tt{no-op}}{\tt{)}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\rm{list}}\,(\=\+{\tt{'}}{\tt{pop*}}, \\ 
{\rm{data-length}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{data-length})\-, \\ 
{\tt{'}}{\tt{(}}{\tt{(}}{\tt{ret}}{\tt{)}}{\tt{)}})\-)\-)\-\index{ok-translation-parameters} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statep}}\,(\=\+{\rm{make-call-environment}}\,(\=\+{\it{mg-state\/}}, \\ 
{\it{stmt\/}}, \\ 
{\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\-\index{make-call-environment}, \\ 
{\rm{make-cond-list}}\,({\rm{fetch-called-def}}\,({\it{stmt\/}}, {\it{proc-list\/}})\index{fetch-called-def})\index{make-cond-list})\-\index{ok-mg-statep} \\ 
$\wedge$$\;\;\;\;${\rm{cond-subsetp}}\,(\=\+{\rm{make-cond-list}}\,({\rm{fetch-called-def}}\,({\it{stmt\/}}, {\it{proc-list\/}})\index{fetch-called-def})\index{make-cond-list}, \\ 
{\rm{make-cond-list}}\,({\rm{fetch-called-def}}\,({\it{stmt\/}}, {\it{proc-list\/}})\index{fetch-called-def})\index{make-cond-list})\-\index{cond-subsetp} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{code}}\,({\rm{translate-def-body}}\,(\=\+{\rm{assoc}}\,({\rm{call-name}}\,({\it{stmt\/}})\index{call-name}, {\it{proc-list\/}}), \\ 
{\it{proc-list\/}})\-\index{translate-def-body})\index{code} \\ 
$=$$\;\;\;\;${\rm{append}}\,(\=\+{\rm{code}}\,({\rm{translate}}\,(\=\+{\rm{make-cinfo}}\,(\=\+{\bf{nil}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}\=\+{\tt{routineerror}} \\ 
{\tt{.\ }}{\tt{0}}{\tt{)}}\-, \\ 
{\rm{make-label-alist}}\,(\=\+{\rm{make-cond-list}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{make-cond-list}, \\ 
{\tt{0}})\-\index{make-label-alist})\-, \\ 
{\tt{1}})\-\index{make-cinfo}, \\ 
{\rm{make-cond-list}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{make-cond-list}, \\ 
{\rm{def-body}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-body}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{dl}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{nil}}{\tt{ }}{\tt{(}}{\tt{no-op}}{\tt{)}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\rm{list}}\,(\=\+{\tt{'}}{\tt{pop*}}, \\ 
{\rm{data-length}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{data-length})\-, \\ 
{\tt{'}}{\tt{(}}{\tt{(}}{\tt{ret}}{\tt{)}}{\tt{)}})\-)\-)\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{user-defined-procp}}\,({\rm{call-name}}\,({\it{stmt\/}})\index{call-name}, {\it{proc-list\/}})\index{user-defined-procp} \\ 
$\wedge$$\;\;\;\;${\rm{plistp}}\,({\rm{append}}\,(\=\+{\rm{reverse}}\,({\rm{mg-to-p-local-values}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{mg-to-p-local-values})\index{reverse}, \\ 
{\rm{map-down-values}}\,(\=\+{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, \\ 
{\it{temp-stk\/}})\-\index{map-down-values})\-)\index{plistp} \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\rm{cons}}\,(\=\+{\rm{p-frame}}\,(\=\+{\rm{make-frame-alist}}\,(\=\+{\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def}, \\ 
{\it{stmt\/}}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\it{temp-stk\/}})\-\index{make-frame-alist}, \\ 
{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,(\=\+{\it{subr\/}}, \\ 
$1\;+$ (\=\+{\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} \\ 
$+$$\;\;\;\;${\rm{data-length}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{data-length} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{length} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals})\index{length})\-)\-)\-\index{tag})\-\index{p-frame}, \\ 
{\it{ctrl-stk\/}})\-) \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,(\=\+{\rm{mg-alist}}\,({\rm{make-call-environment}}\,(\=\+{\it{mg-state\/}}, \\ 
{\it{stmt\/}}, \\ 
{\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\-\index{make-call-environment})\index{mg-alist}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\rm{cons}}\,(\=\+{\rm{p-frame}}\,(\=\+{\rm{make-frame-alist}}\,(\=\+{\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def}, \\ 
{\it{stmt\/}}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\it{temp-stk\/}})\-\index{make-frame-alist}, \\ 
{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,(\=\+{\it{subr\/}}, \\ 
$1\;+$ (\=\+{\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} \\ 
$+$$\;\;\;\;${\rm{data-length}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{data-length} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{length} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals})\index{length})\-)\-)\-\index{tag})\-\index{p-frame}, \\ 
{\it{ctrl-stk\/}})\-)\index{top})\index{bindings}, \\ 
{\rm{append}}\,(\=\+{\rm{reverse}}\,({\rm{mg-to-p-local-values}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{mg-to-p-local-values})\index{reverse}, \\ 
{\rm{map-down-values}}\,(\=\+{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, \\ 
{\it{temp-stk\/}})\-\index{map-down-values})\-)\-\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,(\=\+{\rm{bindings}}\,({\rm{top}}\,({\rm{cons}}\,(\=\+{\rm{p-frame}}\,(\=\+{\rm{make-frame-alist}}\,(\=\+{\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def}, \\ 
{\it{stmt\/}}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\it{temp-stk\/}})\-\index{make-frame-alist}, \\ 
{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,(\=\+{\it{subr\/}}, \\ 
$1\;+$ (\=\+{\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} \\ 
$+$$\;\;\;\;${\rm{data-length}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{data-length} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{length} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals})\index{length})\-)\-)\-\index{tag})\-\index{p-frame}, \\ 
{\it{ctrl-stk\/}})\-)\index{top})\index{bindings}, \\ 
{\rm{mg-alist}}\,({\rm{make-call-environment}}\,(\=\+{\it{mg-state\/}}, \\ 
{\it{stmt\/}}, \\ 
{\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\-\index{make-call-environment})\index{mg-alist})\-\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,(\=\+{\rm{mg-alist}}\,({\rm{make-call-environment}}\,(\=\+{\it{mg-state\/}}, \\ 
{\it{stmt\/}}, \\ 
{\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\-\index{make-call-environment})\index{mg-alist}, \\ 
{\rm{make-name-alist}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{make-name-alist})\-\index{signatures-match} \\ 
$\wedge$$\;\;\;\;${\rm{normal}}\,({\rm{make-call-environment}}\,(\=\+{\it{mg-state\/}}, \\ 
{\it{stmt\/}}, \\ 
{\rm{fetch-called-def}}\,({\it{stmt\/}}, {\it{proc-list\/}})\index{fetch-called-def})\-\index{make-call-environment})\index{normal} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\rm{make-call-environment}}\,(\=\+{\it{mg-state\/}}, \\ 
{\it{stmt\/}}, \\ 
{\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\-\index{make-call-environment})\index{mg-alist})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resource-errorp}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{def-body}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-body}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{make-call-environment}}\,(\=\+{\it{mg-state\/}}, \\ 
{\it{stmt\/}}, \\ 
{\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\-\index{make-call-environment}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\rm{append}}\,(\=\+{\rm{reverse}}\,({\rm{mg-to-p-local-values}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{mg-to-p-local-values})\index{reverse}, \\ 
{\rm{map-down-values}}\,(\=\+{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, \\ 
{\it{temp-stk\/}})\-\index{map-down-values})\-)\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\rm{cons}}\,(\=\+{\rm{p-frame}}\,(\=\+{\rm{make-frame-alist}}\,(\=\+{\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def}, \\ 
{\it{stmt\/}}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\it{temp-stk\/}})\-\index{make-frame-alist}, \\ 
{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,(\=\+{\it{subr\/}}, \\ 
$1\;+$ (\=\+{\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} \\ 
$+$$\;\;\;\;${\rm{data-length}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{data-length} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{length} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals})\index{length})\-)\-)\-\index{tag})\-\index{p-frame}, \\ 
{\it{ctrl-stk\/}})\-)\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{resource-errorp}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  simple-typed-literal-listp \\ \index{simple-typed-literal-listp}
{\rm{simple-typed-literalp}}\,({\it{exp\/}}, {\it{type\/}})\index{simple-typed-literalp} $\rightarrow$ {\rm{listp}}\,({\rm{mg-to-p-simple-literal}}\,({\it{exp\/}})\index{mg-to-p-simple-literal})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{push-array-value-induction-hint} \\  
\=\+{\rm{push-array-value-induction-hint}}\,({\it{array-value\/}}, {\it{code\/}}, {\it{temp-stk\/}})\index{push-array-value-induction-hint} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{array-value\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{push-array-value-induction-hint}}\,(\=\+{\rm{cdr}}\,({\it{array-value\/}}), \\ 
{\rm{append}}\,(\=\+{\it{code\/}}, \\ 
{\rm{list}}\,({\rm{list}}\,(\=\+{\tt{'}}{\tt{push-constant}}, \\ 
{\rm{mg-to-p-simple-literal}}\,({\rm{car}}\,({\it{array-value\/}}))\index{mg-to-p-simple-literal})\-))\-, \\ 
{\rm{push}}\,(\=\+{\rm{mg-to-p-simple-literal}}\,({\rm{car}}\,({\it{array-value\/}}))\index{mg-to-p-simple-literal}, \\ 
{\it{temp-stk\/}})\-\index{push})\-\index{push-array-value-induction-hint}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  push-local-array-values-code-effect \\ \index{push-local-array-values-code-ef!fect}
\=\+(\=\+(({\rm{length}}\,({\it{temp-stk\/}})\index{length} $+$ {\rm{length}}\,({\it{array-value\/}})\index{length}) $<$ {\sc{mg-max-temp-stk-size}}\index{mg-max-temp-stk-size}) \\ 
$\wedge$$\;\;\;\;${\rm{simple-mg-type-refp}}\,({\it{array-elemtype\/}})\index{simple-mg-type-refp} \\ 
$\wedge$$\;\;\;\;${\rm{simple-typed-literal-plistp}}\,({\it{array-value\/}}, {\it{array-elemtype\/}})\index{simple-typed-literal-plistp} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{cdddr}}\,({\rm{assoc}}\,({\it{subr\/}}, {\it{proc-list-code\/}})) \\ 
$=$$\;\;\;\;${\rm{append}}\,(\=\+{\it{code\/}}, \\ 
{\rm{append}}\,(\=\+{\rm{push-local-array-values-code}}\,({\it{array-value\/}})\index{push-local-array-values-code}, \\ 
{\it{code2\/}})\-)\-)\-)\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{p}}\,(\=\+{\rm{p-state}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{pc}}, {\rm{cons}}\,({\it{subr\/}}, {\rm{length}}\,({\it{code\/}})\index{length}))\index{tag}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\it{temp-stk\/}}, \\ 
{\it{proc-list-code\/}}, \\ 
{\it{data-segment\/}}, \\ 
{\it{max-ctrl\/}}, \\ 
{\sc{mg-max-temp-stk-size}}\index{mg-max-temp-stk-size}, \\ 
{\it{word-size\/}}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state}, \\ 
{\rm{length}}\,({\it{array-value\/}})\index{length})\-\index{p} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,({\it{subr\/}}, {\rm{length}}\,({\it{code\/}})\index{length} $+$ {\rm{length}}\,({\it{array-value\/}})\index{length}))\-\index{tag}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\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\/}})\-, \\ 
{\it{proc-list-code\/}}, \\ 
{\it{data-segment\/}}, \\ 
{\it{max-ctrl\/}}, \\ 
{\sc{mg-max-temp-stk-size}}\index{mg-max-temp-stk-size}, \\ 
{\it{word-size\/}}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state})\-\-
\end{tabbing}


\noindent{\sc Event}:   Enable length-cons.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{locals-values-induction-hint} \\  
\=\+{\rm{locals-values-induction-hint}}\,({\it{locals\/}}, {\it{code\/}}, {\it{temp-stk\/}})\index{locals-values-induction-hint} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{locals\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\rm{car}}\,({\it{locals\/}})))\index{simple-mg-type-refp} \\ 
{\bf then }{\rm{locals-values-induction-hint}}\,(\=\+{\rm{cdr}}\,({\it{locals\/}}), \\ 
{\rm{append}}\,(\=\+{\it{code\/}}, \\ 
{\rm{list}}\,({\rm{list}}\,(\=\+{\tt{'}}{\tt{push-constant}}, \\ 
{\rm{mg-to-p-simple-literal}}\,({\rm{caddar}}\,({\it{locals\/}}))\index{mg-to-p-simple-literal})\-))\-, \\ 
{\rm{push}}\,(\=\+{\rm{mg-to-p-simple-literal}}\,({\rm{caddr}}\,({\rm{car}}\,({\it{locals\/}})))\index{mg-to-p-simple-literal}, \\ 
{\it{temp-stk\/}})\-\index{push})\-\index{locals-values-induction-hint} \\ 
{\bf else }{\rm{locals-values-induction-hint}}\,(\=\+{\rm{cdr}}\,({\it{locals\/}}), \\ 
{\rm{append}}\,(\=\+{\it{code\/}}, \\ 
{\rm{push-local-array-values-code}}\,({\rm{caddr}}\,({\rm{car}}\,({\it{locals\/}})))\index{push-local-array-values-code})\-, \\ 
{\rm{append}}\,(\=\+{\rm{reverse}}\,({\rm{mg-to-p-simple-literal-list}}\,({\rm{caddr}}\,({\rm{car}}\,({\it{locals\/}})))\index{mg-to-p-simple-literal-list})\index{reverse}, \\ 
{\it{temp-stk\/}})\-)\-\index{locals-values-induction-hint}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  call-push-locals-values-effect \\ \index{call-push-locals-values-effect}
\=\+(\=\+(({\rm{length}}\,({\it{temp-stk\/}})\index{length} $+$ {\rm{data-length}}\,({\it{locals\/}})\index{data-length}) $<$ {\sc{mg-max-temp-stk-size}}\index{mg-max-temp-stk-size}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-local-data-plistp}}\,({\it{locals\/}})\index{ok-mg-local-data-plistp} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{cdddr}}\,({\rm{assoc}}\,({\it{subr\/}}, {\it{proc-list-code\/}})) \\ 
$=$$\;\;\;\;${\rm{append}}\,({\it{code\/}}, {\rm{append}}\,({\rm{push-locals-values-code}}\,({\it{locals\/}})\index{push-locals-values-code}, {\it{code2\/}})))\-)\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{p}}\,(\=\+{\rm{p-state}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{pc}}, {\rm{cons}}\,({\it{subr\/}}, {\rm{length}}\,({\it{code\/}})\index{length}))\index{tag}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\it{temp-stk\/}}, \\ 
{\it{proc-list-code\/}}, \\ 
{\it{data-segment\/}}, \\ 
{\it{max-ctrl\/}}, \\ 
{\sc{mg-max-temp-stk-size}}\index{mg-max-temp-stk-size}, \\ 
{\it{word-size\/}}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state}, \\ 
{\rm{data-length}}\,({\it{locals\/}})\index{data-length})\-\index{p} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,({\it{subr\/}}, {\rm{data-length}}\,({\it{locals\/}})\index{data-length} $+$ {\rm{length}}\,({\it{code\/}})\index{length}))\-\index{tag}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\rm{append}}\,({\rm{reverse}}\,({\rm{mg-to-p-local-values}}\,({\it{locals\/}})\index{mg-to-p-local-values})\index{reverse}, {\it{temp-stk\/}}), \\ 
{\it{proc-list-code\/}}, \\ 
{\it{data-segment\/}}, \\ 
{\it{max-ctrl\/}}, \\ 
{\sc{mg-max-temp-stk-size}}\index{mg-max-temp-stk-size}, \\ 
{\it{word-size\/}}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state})\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{locals-addresses-induction-hint} \\  
\=\+{\rm{locals-addresses-induction-hint}}\,({\it{locals\/}}, {\it{code\/}}, {\it{temp-stk\/}}, {\it{n\/}})\index{locals-addresses-induction-hint} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{locals\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\rm{car}}\,({\it{locals\/}})))\index{simple-mg-type-refp} \\ 
{\bf then }{\rm{locals-addresses-induction-hint}}\,(\=\+{\rm{cdr}}\,({\it{locals\/}}), \\ 
{\rm{append}}\,(\=\+{\it{code\/}}, \\ 
{\rm{list}}\,({\rm{list}}\,(\=\+{\tt{'}}{\tt{push-temp-stk-index}}, \\ 
{\it{n\/}})\-))\-, \\ 
{\rm{push}}\,(\=\+{\rm{tag}}\,(\=\+{\tt{'}}{\tt{nat}}, \\ 
({\rm{length}}\,({\it{temp-stk\/}})\index{length} $-$ {\it{n\/}}) $-\;1$)\-\index{tag}, \\ 
{\it{temp-stk\/}})\-\index{push}, \\ 
{\it{n\/}})\-\index{locals-addresses-induction-hint} \\ 
{\bf else }{\rm{locals-addresses-induction-hint}}\,(\=\+{\rm{cdr}}\,({\it{locals\/}}), \\ 
{\rm{append}}\,(\=\+{\it{code\/}}, \\ 
{\rm{list}}\,({\rm{list}}\,(\=\+{\tt{'}}{\tt{push-temp-stk-index}}, \\ 
{\it{n\/}})\-))\-, \\ 
{\rm{push}}\,(\=\+{\rm{tag}}\,(\=\+{\tt{'}}{\tt{nat}}, \\ 
(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length} \\ 
$-$$\;\;\;\;${\it{n\/}})\- $-\;1$)\-\index{tag}, \\ 
{\it{temp-stk\/}})\-\index{push}, \\ 
$1\;+$ ({\it{n\/}} $-$ {\rm{array-length}}\,({\rm{cadr}}\,({\rm{car}}\,({\it{locals\/}})))\index{array-length}))\-\index{locals-addresses-induction-hint}$\;${\bf  endif}\-\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  call-push-locals-addresses-effect \\ \index{call-push-locals-addresses-effe!ct}
\=\+(\=\+(({\rm{length}}\,({\it{temp-stk\/}})\index{length} $+$ {\rm{length}}\,({\it{locals\/}})\index{length}) $<$ {\sc{mg-max-temp-stk-size}}\index{mg-max-temp-stk-size}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-local-data-plistp}}\,({\it{locals\/}})\index{ok-mg-local-data-plistp} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{cdddr}}\,({\rm{assoc}}\,({\it{subr\/}}, {\it{proc-list-code\/}})) \\ 
$=$$\;\;\;\;${\rm{append}}\,(\=\+{\it{code\/}}, \\ 
{\rm{append}}\,({\rm{push-locals-addresses-code}}\,({\it{locals\/}}, {\it{n\/}})\index{push-locals-addresses-code}, {\it{code2\/}}))\-)\- \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $<$ {\rm{length}}\,({\it{temp-stk\/}})\index{length}) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not<$ ({\rm{data-length}}\,({\it{locals\/}})\index{data-length} $-\;1$)))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{p}}\,(\=\+{\rm{p-state}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{pc}}, {\rm{cons}}\,({\it{subr\/}}, {\rm{length}}\,({\it{code\/}})\index{length}))\index{tag}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\it{temp-stk\/}}, \\ 
{\it{proc-list-code\/}}, \\ 
{\it{data-segment\/}}, \\ 
{\it{max-ctrl\/}}, \\ 
{\sc{mg-max-temp-stk-size}}\index{mg-max-temp-stk-size}, \\ 
{\it{word-size\/}}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state}, \\ 
{\rm{length}}\,({\it{locals\/}})\index{length})\-\index{p} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{pc}}, {\rm{cons}}\,({\it{subr\/}}, {\rm{length}}\,({\it{code\/}})\index{length} $+$ {\rm{length}}\,({\it{locals\/}})\index{length}))\index{tag}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\rm{append}}\,(\=\+{\rm{reverse}}\,({\rm{ascending-local-address-sequence}}\,(\=\+{\it{locals\/}}, \\ 
(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length} \\ 
$-$$\;\;\;\;${\it{n\/}})\- $-\;1$)\-\index{ascending-local-address-sequence})\index{reverse}, \\ 
{\it{temp-stk\/}})\-, \\ 
{\it{proc-list-code\/}}, \\ 
{\it{data-segment\/}}, \\ 
{\it{max-ctrl\/}}, \\ 
{\sc{mg-max-temp-stk-size}}\index{mg-max-temp-stk-size}, \\ 
{\it{word-size\/}}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state})\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{call-push-actuals-induction-hint} \\  
\=\+{\rm{call-push-actuals-induction-hint}}\,({\it{actuals\/}}, {\it{code\/}}, {\it{temp-stk\/}}, {\it{ctrl-stk\/}})\index{call-push-actuals-induction-hint} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{actuals\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{call-push-actuals-induction-hint}}\,(\=\+{\rm{cdr}}\,({\it{actuals\/}}), \\ 
{\rm{append}}\,(\=\+{\it{code\/}}, \\ 
{\rm{list}}\,({\rm{list}}\,(\=\+{\tt{'}}{\tt{push-local}}, \\ 
{\rm{car}}\,({\it{actuals\/}}))\-))\-, \\ 
{\rm{cons}}\,(\=\+{\rm{cdr}}\,({\rm{assoc}}\,(\=\+{\rm{car}}\,({\it{actuals\/}}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-), \\ 
{\it{temp-stk\/}})\-, \\ 
{\it{ctrl-stk\/}})\-\index{call-push-actuals-induction-hint}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  call-push-actuals-effect \\ \index{call-push-actuals-effect}
\=\+(\=\+(({\rm{length}}\,({\it{temp-stk\/}})\index{length} $+$ {\rm{length}}\,({\it{actuals\/}})\index{length}) $<$ {\sc{mg-max-temp-stk-size}}\index{mg-max-temp-stk-size}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{cdddr}}\,({\rm{assoc}}\,({\it{subr\/}}, {\it{proc-list-code\/}})) \\ 
$=$$\;\;\;\;${\rm{append}}\,({\it{code\/}}, {\rm{append}}\,({\rm{push-actuals-code}}\,({\it{actuals\/}})\index{push-actuals-code}, {\it{code2\/}})))\-)\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{p}}\,(\=\+{\rm{p-state}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{pc}}, {\rm{cons}}\,({\it{subr\/}}, {\rm{length}}\,({\it{code\/}})\index{length}))\index{tag}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\it{temp-stk\/}}, \\ 
{\it{proc-list-code\/}}, \\ 
{\it{data-segment\/}}, \\ 
{\it{max-ctrl\/}}, \\ 
{\sc{mg-max-temp-stk-size}}\index{mg-max-temp-stk-size}, \\ 
{\it{word-size\/}}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state}, \\ 
{\rm{length}}\,({\it{actuals\/}})\index{length})\-\index{p} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{pc}}, {\rm{cons}}\,({\it{subr\/}}, {\rm{length}}\,({\it{code\/}})\index{length} $+$ {\rm{length}}\,({\it{actuals\/}})\index{length}))\index{tag}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\rm{append}}\,(\=\+{\rm{reverse}}\,({\rm{mg-actuals-to-p-actuals}}\,(\=\+{\it{actuals\/}}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{mg-actuals-to-p-actuals})\index{reverse}, \\ 
{\it{temp-stk\/}})\-, \\ 
{\it{proc-list-code\/}}, \\ 
{\it{data-segment\/}}, \\ 
{\it{max-ctrl\/}}, \\ 
{\sc{mg-max-temp-stk-size}}\index{mg-max-temp-stk-size}, \\ 
{\it{word-size\/}}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  call-push-parameters-effect1 \\ \index{call-push-parameters-effect1}
\=\+(\=\+(\=\+(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length} \\ 
$+$$\;\;\;\;${\rm{data-length}}\,({\it{locals\/}})\index{data-length} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\it{locals\/}})\index{length} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\it{actuals\/}})\index{length})\- \\ 
$<$$\;\;\;\;${\sc{mg-max-temp-stk-size}}\index{mg-max-temp-stk-size})\- \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-local-data-plistp}}\,({\it{locals\/}})\index{ok-mg-local-data-plistp} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{cdddr}}\,({\rm{assoc}}\,({\it{subr\/}}, {\it{proc-list-code\/}})) \\ 
$=$$\;\;\;\;${\rm{append}}\,(\=\+{\it{code\/}}, \\ 
{\rm{append}}\,({\rm{push-parameters-code}}\,({\it{locals\/}}, {\it{actuals\/}})\index{push-parameters-code}, {\it{code2\/}}))\-)\-)\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{p}}\,(\=\+{\rm{p-state}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{pc}}, {\rm{cons}}\,({\it{subr\/}}, {\rm{length}}\,({\it{code\/}})\index{length}))\index{tag}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\it{temp-stk\/}}, \\ 
{\it{proc-list-code\/}}, \\ 
{\it{data-segment\/}}, \\ 
{\it{max-ctrl\/}}, \\ 
{\sc{mg-max-temp-stk-size}}\index{mg-max-temp-stk-size}, \\ 
{\it{word-size\/}}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state}, \\ 
{\rm{data-length}}\,({\it{locals\/}})\index{data-length} $+$ {\rm{length}}\,({\it{locals\/}})\index{length} $+$ {\rm{length}}\,({\it{actuals\/}})\index{length})\-\index{p} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,(\=\+{\it{subr\/}}, \\ 
\=\+{\rm{length}}\,({\it{code\/}})\index{length} \\ 
$+$$\;\;\;\;${\rm{data-length}}\,({\it{locals\/}})\index{data-length} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\it{locals\/}})\index{length} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\it{actuals\/}})\index{length}\-)\-)\-\index{tag}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\rm{append}}\,(\=\+{\rm{reverse}}\,({\rm{mg-actuals-to-p-actuals}}\,(\=\+{\it{actuals\/}}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{mg-actuals-to-p-actuals})\index{reverse}, \\ 
{\rm{append}}\,(\=\+{\rm{reverse}}\,({\rm{ascending-local-address-sequence}}\,(\=\+{\it{locals\/}}, \\ 
{\rm{length}}\,({\it{temp-stk\/}})\index{length})\-\index{ascending-local-address-sequence})\index{reverse}, \\ 
{\rm{append}}\,(\=\+{\rm{reverse}}\,({\rm{mg-to-p-local-values}}\,({\it{locals\/}})\index{mg-to-p-local-values})\index{reverse}, \\ 
{\it{temp-stk\/}})\-)\-)\-, \\ 
{\it{proc-list-code\/}}, \\ 
{\it{data-segment\/}}, \\ 
{\it{max-ctrl\/}}, \\ 
{\sc{mg-max-temp-stk-size}}\index{mg-max-temp-stk-size}, \\ 
{\it{word-size\/}}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  call-push-parameters-effect \\ \index{call-push-parameters-effect}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{r-cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statep}}\,({\it{mg-state\/}}, {\it{r-cond-list\/}})\index{ok-mg-statep} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{code}}\,({\rm{translate-def-body}}\,({\rm{assoc}}\,({\it{subr\/}}, {\it{proc-list\/}}), {\it{proc-list\/}})\index{translate-def-body})\index{code} \\ 
$=$$\;\;\;\;${\rm{append}}\,(\=\+{\rm{code}}\,({\rm{translate}}\,({\it{cinfo\/}}, {\it{t-cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}})\index{translate})\index{code}, \\ 
{\it{code2\/}})\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{user-defined-procp}}\,({\it{subr\/}}, {\it{proc-list\/}})\index{user-defined-procp} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,(\=\+{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, \\ 
{\it{temp-stk\/}})\-\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resources-inadequatep}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{resources-inadequatep}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{p}}\,(\=\+{\rm{map-down}}\,(\=\+{\it{mg-state\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\it{temp-stk\/}}, \\ 
{\rm{tag}}\,({\tt{'}}{\tt{pc}}, {\rm{cons}}\,({\it{subr\/}}, {\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length}))\index{tag}, \\ 
{\it{t-cond-list\/}})\-\index{map-down}, \\ 
\=\+{\rm{data-length}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,({\it{stmt\/}}, {\it{proc-list\/}})\index{fetch-called-def})\index{def-locals})\index{data-length} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,({\it{stmt\/}}, {\it{proc-list\/}})\index{fetch-called-def})\index{def-locals})\index{length} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals})\index{length}\-)\-\index{p} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,(\=\+{\it{subr\/}}, \\ 
\=\+{\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} \\ 
$+$$\;\;\;\;${\rm{data-length}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{data-length} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{length} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals})\index{length}\-)\-)\-\index{tag}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\rm{append}}\,(\=\+{\rm{reverse}}\,({\rm{mg-actuals-to-p-actuals}}\,(\=\+{\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{mg-actuals-to-p-actuals})\index{reverse}, \\ 
{\rm{append}}\,(\=\+{\rm{reverse}}\,({\rm{ascending-local-address-sequence}}\,(\=\+{\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals}, \\ 
{\rm{length}}\,({\it{temp-stk\/}})\index{length})\-\index{ascending-local-address-sequence})\index{reverse}, \\ 
{\rm{append}}\,(\=\+{\rm{reverse}}\,({\rm{mg-to-p-local-values}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{mg-to-p-local-values})\index{reverse}, \\ 
{\rm{map-down-values}}\,(\=\+{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, \\ 
{\it{temp-stk\/}})\-\index{map-down-values})\-)\-)\-, \\ 
{\rm{translate-proc-list}}\,({\it{proc-list\/}})\index{translate-proc-list}, \\ 
{\rm{list}}\,({\rm{list}}\,(\=\+{\tt{'}}{\tt{c-c}}, \\ 
{\rm{mg-cond-to-p-nat}}\,({\rm{cc}}\,({\it{mg-state\/}})\index{cc}, {\it{t-cond-list\/}})\index{mg-cond-to-p-nat})\-), \\ 
{\sc{mg-max-ctrl-stk-size}}\index{mg-max-ctrl-stk-size}, \\ 
{\sc{mg-max-temp-stk-size}}\index{mg-max-temp-stk-size}, \\ 
{\sc{mg-word-size}}\index{mg-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  call-call-step \\ \index{call-call-step}
\=\+(\=\+({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resources-inadequatep}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{resources-inadequatep}) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{r-cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-translation-parameters}}\,({\it{cinfo\/}}, {\it{t-cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}}, {\it{code2\/}})\index{ok-translation-parameters} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statep}}\,({\it{mg-state\/}}, {\it{r-cond-list\/}})\index{ok-mg-statep} \\ 
$\wedge$$\;\;\;\;${\rm{cond-subsetp}}\,({\it{r-cond-list\/}}, {\it{t-cond-list\/}})\index{cond-subsetp} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{code}}\,({\rm{translate-def-body}}\,({\rm{assoc}}\,({\it{subr\/}}, {\it{proc-list\/}}), {\it{proc-list\/}})\index{translate-def-body})\index{code} \\ 
$=$$\;\;\;\;${\rm{append}}\,(\=\+{\rm{code}}\,({\rm{translate}}\,({\it{cinfo\/}}, {\it{t-cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}})\index{translate})\index{code}, \\ 
{\it{code2\/}})\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{user-defined-procp}}\,({\it{subr\/}}, {\it{proc-list\/}})\index{user-defined-procp} \\ 
$\wedge$$\;\;\;\;${\rm{plistp}}\,({\it{temp-stk\/}})\index{plistp} \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\it{ctrl-stk\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,(\=\+{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, \\ 
{\it{temp-stk\/}})\-\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, {\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match} \\ 
$\wedge$$\;\;\;\;${\rm{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resource-errorp}}\,({\rm{mg-meaning-r}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{resource-errorp}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{p-step}}\,({\rm{p-state}}\,(\=\+{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,(\=\+{\it{subr\/}}, \\ 
\=\+{\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} \\ 
$+$$\;\;\;\;${\rm{data-length}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{data-length} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{length} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals})\index{length}\-)\-)\-\index{tag}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\rm{append}}\,(\=\+{\rm{reverse}}\,({\rm{mg-actuals-to-p-actuals}}\,(\=\+{\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{mg-actuals-to-p-actuals})\index{reverse}, \\ 
{\rm{append}}\,(\=\+{\rm{reverse}}\,({\rm{ascending-local-address-sequence}}\,(\=\+{\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals}, \\ 
{\rm{length}}\,({\it{temp-stk\/}})\index{length})\-\index{ascending-local-address-sequence})\index{reverse}, \\ 
{\rm{append}}\,(\=\+{\rm{reverse}}\,({\rm{mg-to-p-local-values}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{mg-to-p-local-values})\index{reverse}, \\ 
{\rm{map-down-values}}\,(\=\+{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, \\ 
{\it{temp-stk\/}})\-\index{map-down-values})\-)\-)\-, \\ 
{\rm{translate-proc-list}}\,({\it{proc-list\/}})\index{translate-proc-list}, \\ 
{\rm{list}}\,({\rm{list}}\,(\=\+{\tt{'}}{\tt{c-c}}, \\ 
{\rm{mg-cond-to-p-nat}}\,({\rm{cc}}\,({\it{mg-state\/}})\index{cc}, {\it{t-cond-list\/}})\index{mg-cond-to-p-nat})\-), \\ 
{\sc{mg-max-ctrl-stk-size}}\index{mg-max-ctrl-stk-size}, \\ 
{\sc{mg-max-temp-stk-size}}\index{mg-max-temp-stk-size}, \\ 
{\sc{mg-word-size}}\index{mg-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state})\index{p-step} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{pc}}, {\rm{cons}}\,({\rm{call-name}}\,({\it{stmt\/}})\index{call-name}, {\tt{0}}))\index{tag}, \\ 
{\rm{push}}\,(\=\+{\rm{p-frame}}\,(\=\+{\rm{append}}\,(\=\+{\rm{pairlist}}\,(\=\+{\rm{cadr}}\,({\rm{assoc}}\,(\=\+{\rm{call-name}}\,({\it{stmt\/}})\index{call-name}, \\ 
{\rm{translate-proc-list}}\,({\it{proc-list\/}})\index{translate-proc-list})\-), \\ 
{\rm{append}}\,(\=\+{\rm{ascending-local-address-sequence}}\,(\=\+{\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals}, \\ 
{\rm{length}}\,({\it{temp-stk\/}})\index{length})\-\index{ascending-local-address-sequence}, \\ 
{\rm{mg-actuals-to-p-actuals}}\,(\=\+{\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{mg-actuals-to-p-actuals})\-)\-, \\ 
{\rm{pair-temps-with-initial-values}}\,({\rm{caddr}}\,({\rm{assoc}}\,(\=\+{\rm{call-name}}\,({\it{stmt\/}})\index{call-name}, \\ 
{\rm{translate-proc-list}}\,({\it{proc-list\/}})\index{translate-proc-list})\-))\index{pair-temps-with-initial-values})\-, \\ 
{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,(\=\+{\it{subr\/}}, \\ 
\=\+{\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} \\ 
$+$$\;\;\;\;${\rm{data-length}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{data-length} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{length} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals})\index{length} \\ 
$+$$\;\;\;\;${\tt{1}}\-)\-)\-\index{tag})\-\index{p-frame}, \\ 
{\it{ctrl-stk\/}})\-\index{push}, \\ 
{\rm{append}}\,(\=\+{\rm{reverse}}\,({\rm{mg-to-p-local-values}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{mg-to-p-local-values})\index{reverse}, \\ 
{\rm{map-down-values}}\,(\=\+{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, \\ 
{\it{temp-stk\/}})\-\index{map-down-values})\-, \\ 
{\rm{translate-proc-list}}\,({\it{proc-list\/}})\index{translate-proc-list}, \\ 
{\rm{list}}\,({\rm{list}}\,(\=\+{\tt{'}}{\tt{c-c}}, \\ 
{\rm{mg-cond-to-p-nat}}\,({\rm{cc}}\,({\it{mg-state\/}})\index{cc}, {\it{t-cond-list\/}})\index{mg-cond-to-p-nat})\-), \\ 
{\sc{mg-max-ctrl-stk-size}}\index{mg-max-ctrl-stk-size}, \\ 
{\sc{mg-max-temp-stk-size}}\index{mg-max-temp-stk-size}, \\ 
{\sc{mg-word-size}}\index{mg-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  call-steps-to-body \\ \index{call-steps-to-body}
\=\+(\=\+({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resources-inadequatep}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{resources-inadequatep}) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{r-cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-translation-parameters}}\,({\it{cinfo\/}}, {\it{t-cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}}, {\it{code2\/}})\index{ok-translation-parameters} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statep}}\,({\it{mg-state\/}}, {\it{r-cond-list\/}})\index{ok-mg-statep} \\ 
$\wedge$$\;\;\;\;${\rm{cond-subsetp}}\,({\it{r-cond-list\/}}, {\it{t-cond-list\/}})\index{cond-subsetp} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{code}}\,({\rm{translate-def-body}}\,({\rm{assoc}}\,({\it{subr\/}}, {\it{proc-list\/}}), {\it{proc-list\/}})\index{translate-def-body})\index{code} \\ 
$=$$\;\;\;\;${\rm{append}}\,(\=\+{\rm{code}}\,({\rm{translate}}\,({\it{cinfo\/}}, {\it{t-cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}})\index{translate})\index{code}, \\ 
{\it{code2\/}})\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{user-defined-procp}}\,({\it{subr\/}}, {\it{proc-list\/}})\index{user-defined-procp} \\ 
$\wedge$$\;\;\;\;${\rm{plistp}}\,({\it{temp-stk\/}})\index{plistp} \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\it{ctrl-stk\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,(\=\+{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, \\ 
{\it{temp-stk\/}})\-\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, {\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match} \\ 
$\wedge$$\;\;\;\;${\rm{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resource-errorp}}\,({\rm{mg-meaning-r}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{resource-errorp}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{p}}\,(\=\+{\rm{map-down}}\,(\=\+{\it{mg-state\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\it{temp-stk\/}}, \\ 
{\rm{tag}}\,({\tt{'}}{\tt{pc}}, {\rm{cons}}\,({\it{subr\/}}, {\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length}))\index{tag}, \\ 
{\it{t-cond-list\/}})\-\index{map-down}, \\ 
\=\+{\rm{data-length}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,({\it{stmt\/}}, {\it{proc-list\/}})\index{fetch-called-def})\index{def-locals})\index{data-length} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,({\it{stmt\/}}, {\it{proc-list\/}})\index{fetch-called-def})\index{def-locals})\index{length} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals})\index{length} \\ 
$+$$\;\;\;\;${\tt{1}}\-)\-\index{p} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{pc}}, {\rm{cons}}\,({\rm{call-name}}\,({\it{stmt\/}})\index{call-name}, {\tt{0}}))\index{tag}, \\ 
{\rm{push}}\,(\=\+{\rm{p-frame}}\,(\=\+{\rm{append}}\,(\=\+{\rm{pairlist}}\,(\=\+{\rm{cadr}}\,({\rm{assoc}}\,(\=\+{\rm{call-name}}\,({\it{stmt\/}})\index{call-name}, \\ 
{\rm{translate-proc-list}}\,({\it{proc-list\/}})\index{translate-proc-list})\-), \\ 
{\rm{append}}\,(\=\+{\rm{ascending-local-address-sequence}}\,(\=\+{\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals}, \\ 
{\rm{length}}\,({\it{temp-stk\/}})\index{length})\-\index{ascending-local-address-sequence}, \\ 
{\rm{mg-actuals-to-p-actuals}}\,(\=\+{\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{mg-actuals-to-p-actuals})\-)\-, \\ 
{\rm{pair-temps-with-initial-values}}\,({\rm{caddr}}\,({\rm{assoc}}\,(\=\+{\rm{call-name}}\,({\it{stmt\/}})\index{call-name}, \\ 
{\rm{translate-proc-list}}\,({\it{proc-list\/}})\index{translate-proc-list})\-))\index{pair-temps-with-initial-values})\-, \\ 
{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,(\=\+{\it{subr\/}}, \\ 
\=\+{\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} \\ 
$+$$\;\;\;\;${\rm{data-length}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{data-length} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{length} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals})\index{length} \\ 
$+$$\;\;\;\;${\tt{1}}\-)\-)\-\index{tag})\-\index{p-frame}, \\ 
{\it{ctrl-stk\/}})\-\index{push}, \\ 
{\rm{append}}\,(\=\+{\rm{reverse}}\,({\rm{mg-to-p-local-values}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{mg-to-p-local-values})\index{reverse}, \\ 
{\rm{map-down-values}}\,(\=\+{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, \\ 
{\it{temp-stk\/}})\-\index{map-down-values})\-, \\ 
{\rm{translate-proc-list}}\,({\it{proc-list\/}})\index{translate-proc-list}, \\ 
{\rm{list}}\,({\rm{list}}\,(\=\+{\tt{'}}{\tt{c-c}}, \\ 
{\rm{mg-cond-to-p-nat}}\,({\rm{cc}}\,({\it{mg-state\/}})\index{cc}, {\it{t-cond-list\/}})\index{mg-cond-to-p-nat})\-), \\ 
{\sc{mg-max-ctrl-stk-size}}\index{mg-max-ctrl-stk-size}, \\ 
{\sc{mg-max-temp-stk-size}}\index{mg-max-temp-stk-size}, \\ 
{\sc{mg-word-size}}\index{mg-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state})\-\-
\end{tabbing}


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

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  call-local-var-lists-match1 \\ \index{call-local-var-lists-match1}
\=\+({\it{k\/}} $\in\;${\bf{N}}${}$) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{pairlist}}\,({\rm{listcars}}\,({\it{locals\/}})\index{listcars}, {\rm{ascending-local-address-sequence}}\,({\it{locals\/}}, {\it{k\/}})\index{ascending-local-address-sequence}) \\ 
$=$$\;\;\;\;${\rm{map-call-locals}}\,({\it{locals\/}}, {\it{k\/}})\index{map-call-locals})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  call-formal-var-lists-match \\ \index{call-formal-var-lists-match}
\=\+{\rm{data-param-lists-match}}\,({\it{actuals\/}}, {\it{formals\/}}, {\it{alist\/}})\index{data-param-lists-match} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{pairlist}}\,({\rm{listcars}}\,({\it{formals\/}})\index{listcars}, {\rm{mg-actuals-to-p-actuals}}\,({\it{actuals\/}}, {\it{bindings\/}})\index{mg-actuals-to-p-actuals}) \\ 
$=$$\;\;\;\;${\rm{map-call-formals}}\,({\it{formals\/}}, {\it{actuals\/}}, {\it{bindings\/}})\index{map-call-formals})\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{map-down-locals-doesnt-affect-f!ormals-induction-hint} \\  
\=\+{\rm{map-down-locals-doesnt-affect-formals-induction-hint}}\,(\=\+{\it{formals\/}}, \\ 
{\it{actuals\/}}, \\ 
{\it{temp-stk\/}}, \\ 
{\it{mg-alist\/}}, \\ 
{\it{bindings\/}})\-\index{map-down-locals-doesnt-affect-f!ormals-induction-hint} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{formals\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{map-down-locals-doesnt-affect-formals-induction-hint}}\,(\=\+{\rm{cdr}}\,({\it{formals\/}}), \\ 
{\rm{cdr}}\,({\it{actuals\/}}), \\ 
{\rm{deposit-alist-value}}\,(\=\+{\rm{list}}\,(\=\+{\rm{caar}}\,({\it{formals\/}}), \\ 
{\rm{cadar}}\,({\it{formals\/}}), \\ 
{\rm{caddr}}\,({\rm{assoc}}\,(\=\+{\rm{car}}\,({\it{actuals\/}}), \\ 
{\it{mg-alist\/}})\-))\-, \\ 
{\rm{cons}}\,(\=\+{\rm{cons}}\,(\=\+{\rm{car}}\,({\rm{car}}\,({\it{formals\/}})), \\ 
{\rm{cdr}}\,({\rm{assoc}}\,(\=\+{\rm{car}}\,({\it{actuals\/}}), \\ 
{\it{bindings\/}})\-))\-, \\ 
{\rm{map-call-formals}}\,(\=\+{\rm{cdr}}\,({\it{formals\/}}), \\ 
{\rm{cdr}}\,({\it{actuals\/}}), \\ 
{\it{bindings\/}})\-\index{map-call-formals})\-, \\ 
{\it{temp-stk\/}})\-\index{deposit-alist-value}, \\ 
{\it{mg-alist\/}}, \\ 
{\it{bindings\/}})\-\index{map-down-locals-doesnt-affect-f!ormals-induction-hint}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  map-down-locals-doesnt-affect-formals \\ \index{map-down-locals-doesnt-affect-f!ormals}
\=\+{\rm{all-cars-unique}}\,({\rm{append}}\,({\it{formals\/}}, {\it{locals\/}}))\index{all-cars-unique} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{map-down-values}}\,(\=\+{\rm{make-call-param-alist}}\,({\it{formals\/}}, {\it{actuals\/}}, {\it{mg-alist\/}})\index{make-call-param-alist}, \\ 
{\rm{append}}\,(\=\+{\rm{map-call-locals}}\,({\it{locals\/}}, {\it{n\/}})\index{map-call-locals}, \\ 
{\rm{map-call-formals}}\,({\it{formals\/}}, {\it{actuals\/}}, {\it{bindings\/}})\index{map-call-formals})\-, \\ 
{\it{temp-stk\/}})\-\index{map-down-values} \\ 
$=$$\;\;\;\;${\rm{map-down-values}}\,(\=\+{\rm{make-call-param-alist}}\,(\=\+{\it{formals\/}}, \\ 
{\it{actuals\/}}, \\ 
{\it{mg-alist\/}})\-\index{make-call-param-alist}, \\ 
{\rm{map-call-formals}}\,({\it{formals\/}}, {\it{actuals\/}}, {\it{bindings\/}})\index{map-call-formals}, \\ 
{\it{temp-stk\/}})\-\index{map-down-values})\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{map-down-formals-doesnt-affect-!locals-induction-hint} \\  
\=\+{\rm{map-down-formals-doesnt-affect-locals-induction-hint}}\,({\it{locals\/}}, {\it{temp-stk\/}}, {\it{n\/}}, {\it{lst\/}})\index{map-down-formals-doesnt-affect-!locals-induction-hint} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{locals\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\rm{car}}\,({\it{locals\/}})))\index{simple-mg-type-refp} \\ 
{\bf then }{\rm{map-down-formals-doesnt-affect-locals-induction-hint}}\,(\=\+{\rm{cdr}}\,({\it{locals\/}}), \\ 
{\rm{deposit-alist-value}}\,(\=\+{\rm{car}}\,({\it{locals\/}}), \\ 
{\rm{append}}\,(\=\+{\rm{map-call-locals}}\,(\=\+{\it{locals\/}}, \\ 
{\it{n\/}})\-\index{map-call-locals}, \\ 
{\it{lst\/}})\-, \\ 
{\it{temp-stk\/}})\-\index{deposit-alist-value}, \\ 
$1\;+$ {\it{n\/}}, \\ 
{\it{lst\/}})\-\index{map-down-formals-doesnt-affect-!locals-induction-hint} \\ 
{\bf else }{\rm{map-down-formals-doesnt-affect-locals-induction-hint}}\,(\=\+{\rm{cdr}}\,({\it{locals\/}}), \\ 
{\rm{deposit-alist-value}}\,(\=\+{\rm{car}}\,({\it{locals\/}}), \\ 
{\rm{append}}\,(\=\+{\rm{map-call-locals}}\,(\=\+{\it{locals\/}}, \\ 
{\it{n\/}})\-\index{map-call-locals}, \\ 
{\it{lst\/}})\-, \\ 
{\it{temp-stk\/}})\-\index{deposit-alist-value}, \\ 
\=\+{\rm{array-length}}\,({\rm{cadr}}\,({\rm{car}}\,({\it{locals\/}})))\index{array-length} \\ 
$+$$\;\;\;\;${\it{n\/}}\-, \\ 
{\it{lst\/}})\-\index{map-down-formals-doesnt-affect-!locals-induction-hint}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  map-down-formals-doesnt-affect-locals \\ \index{map-down-formals-doesnt-affect-!locals}
\=\+{\rm{all-cars-unique}}\,({\it{locals\/}})\index{all-cars-unique} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{map-down-values}}\,(\=\+{\it{locals\/}}, \\ 
{\rm{append}}\,({\rm{map-call-locals}}\,({\it{locals\/}}, {\it{n\/}})\index{map-call-locals}, {\it{lst\/}}), \\ 
{\it{temp-stk\/}})\-\index{map-down-values} \\ 
$=$$\;\;\;\;${\rm{map-down-values}}\,({\it{locals\/}}, {\rm{map-call-locals}}\,({\it{locals\/}}, {\it{n\/}})\index{map-call-locals}, {\it{temp-stk\/}})\index{map-down-values})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  map-down-skips-non-referenced-segment \\ \index{map-down-skips-non-referenced-se!gment}
\=\+({\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{map-down-values}}\,({\it{vars\/}}, {\it{bindings\/}}, {\rm{append}}\,({\it{lst\/}}, {\it{temp-stk\/}}))\index{map-down-values} \\ 
$=$$\;\;\;\;${\rm{append}}\,({\it{lst\/}}, {\rm{map-down-values}}\,({\it{vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{map-down-values}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{map-down-locals-induction-hint} \\  
\=\+{\rm{map-down-locals-induction-hint}}\,({\it{locals\/}}, {\it{n\/}}, {\it{temp-stk\/}})\index{map-down-locals-induction-hint} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{locals\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\rm{car}}\,({\it{locals\/}})))\index{simple-mg-type-refp} \\ 
{\bf then }{\rm{map-down-locals-induction-hint}}\,(\=\+{\rm{cdr}}\,({\it{locals\/}}), \\ 
$1\;+$ {\it{n\/}}, \\ 
{\rm{cons}}\,(\=\+{\rm{mg-to-p-simple-literal}}\,({\rm{caddar}}\,({\it{locals\/}}))\index{mg-to-p-simple-literal}, \\ 
{\it{temp-stk\/}})\-)\-\index{map-down-locals-induction-hint} \\ 
{\bf else }{\rm{map-down-locals-induction-hint}}\,(\=\+{\rm{cdr}}\,({\it{locals\/}}), \\ 
\=\+{\rm{array-length}}\,({\rm{cadr}}\,({\rm{car}}\,({\it{locals\/}})))\index{array-length} \\ 
$+$$\;\;\;\;${\it{n\/}}\-, \\ 
{\rm{append}}\,(\=\+{\rm{reverse}}\,({\rm{mg-to-p-simple-literal-list}}\,({\rm{caddr}}\,({\rm{car}}\,({\it{locals\/}})))\index{mg-to-p-simple-literal-list})\index{reverse}, \\ 
{\it{temp-stk\/}})\-)\-\index{map-down-locals-induction-hint}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  map-down-locals-equals-reverse-values \\ \index{map-down-locals-equals-reverse-v!alues}
\=\+(\=\+({\it{n\/}} $=$ {\rm{length}}\,({\it{temp-stk\/}})\index{length}) \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\it{locals\/}})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-local-data-plistp}}\,({\it{locals\/}})\index{ok-mg-local-data-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{plistp}}\,({\it{temp-stk\/}})\index{plistp})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{map-down-values}}\,(\=\+{\it{locals\/}}, \\ 
{\rm{map-call-locals}}\,({\it{locals\/}}, {\it{n\/}})\index{map-call-locals}, \\ 
{\rm{append}}\,(\=\+{\rm{reverse}}\,({\rm{mg-to-p-local-values}}\,({\it{locals\/}})\index{mg-to-p-local-values})\index{reverse}, \\ 
{\it{temp-stk\/}})\-)\-\index{map-down-values} \\ 
$=$$\;\;\;\;${\rm{append}}\,({\rm{reverse}}\,({\rm{mg-to-p-local-values}}\,({\it{locals\/}})\index{mg-to-p-local-values})\index{reverse}, {\it{temp-stk\/}}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  map-down-again-preserves-values \\ \index{map-down-again-preserves-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{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{all-cars-unique}}\,({\it{mg-vars\/}})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{plistp}}\,({\it{temp-stk\/}})\index{plistp} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\it{mg-vars\/}})\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\it{formals\/}})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\it{mg-vars\/}})\index{mg-alistp})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{map-down-values}}\,(\=\+{\rm{make-call-param-alist}}\,({\it{formals\/}}, {\it{actuals\/}}, {\it{mg-vars\/}})\index{make-call-param-alist}, \\ 
{\rm{map-call-formals}}\,({\it{formals\/}}, {\it{actuals\/}}, {\it{bindings\/}})\index{map-call-formals}, \\ 
{\rm{map-down-values}}\,({\it{mg-vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{map-down-values})\-\index{map-down-values} \\ 
$=$$\;\;\;\;${\rm{map-down-values}}\,({\it{mg-vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{map-down-values})\-\-
\end{tabbing}


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

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  array-formal-ok-for-actual2 \\ \index{array-formal-ok-for-actual2}
\=\+(\=\+{\rm{definedp}}\,({\it{actual\/}}, {\it{mg-alist\/}})\index{definedp} \\ 
$\wedge$$\;\;\;\;${\rm{data-params-match}}\,({\it{actual\/}}, {\it{formal\/}}, {\it{mg-alist\/}})\index{data-params-match} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{mg-alist\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\it{formal\/}}))\index{simple-mg-type-refp}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{ok-temp-stk-array-index}}\,(\=\+{\rm{cdr}}\,({\rm{assoc}}\,({\it{actual\/}}, {\it{bindings\/}})), \\ 
{\rm{map-down-values}}\,({\it{mg-alist\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{map-down-values}, \\ 
{\rm{array-length}}\,({\rm{cadr}}\,({\it{formal\/}}))\index{array-length})\-\index{ok-temp-stk-array-index}\-
\end{tabbing}


\noindent{\sc Event}:   Disable array-formal-ok-for-actual2.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  call-environment-mg-vars-list-ok1 \\ \index{call-environment-mg-vars-list-o!k1}
\=\+(\=\+{\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\it{mg-vars\/}})\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\it{mg-vars\/}})\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\it{formals\/}})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{ok-actual-params-list}}\,({\it{actuals\/}}, {\it{mg-vars\/}})\index{ok-actual-params-list} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-formal-data-params-plistp}}\,({\it{formals\/}})\index{ok-mg-formal-data-params-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{data-param-lists-match}}\,({\it{actuals\/}}, {\it{formals\/}}, {\it{mg-vars\/}})\index{data-param-lists-match} \\ 
$\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{mg-vars-list-ok-in-p-state}}\,(\=\+{\rm{make-call-param-alist}}\,(\=\+{\it{formals\/}}, \\ 
{\it{actuals\/}}, \\ 
{\it{mg-vars\/}})\-\index{make-call-param-alist}, \\ 
{\rm{map-call-formals}}\,({\it{formals\/}}, {\it{actuals\/}}, {\it{bindings\/}})\index{map-call-formals}, \\ 
{\rm{map-down-values}}\,({\it{mg-vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{map-down-values})\-\index{mg-vars-list-ok-in-p-state}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  map-down-preserves-references \\ \index{map-down-preserves-references}
\=\+(\=\+({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resources-inadequatep}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{resources-inadequatep}) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{r-cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-translation-parameters}}\,({\it{cinfo\/}}, {\it{t-cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}}, {\it{code2\/}})\index{ok-translation-parameters} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statep}}\,({\it{mg-state\/}}, {\it{r-cond-list\/}})\index{ok-mg-statep} \\ 
$\wedge$$\;\;\;\;${\rm{cond-subsetp}}\,({\it{r-cond-list\/}}, {\it{t-cond-list\/}})\index{cond-subsetp} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{code}}\,({\rm{translate-def-body}}\,({\rm{assoc}}\,({\it{subr\/}}, {\it{proc-list\/}}), {\it{proc-list\/}})\index{translate-def-body})\index{code} \\ 
$=$$\;\;\;\;${\rm{append}}\,(\=\+{\rm{code}}\,({\rm{translate}}\,({\it{cinfo\/}}, {\it{t-cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}})\index{translate})\index{code}, \\ 
{\it{code2\/}})\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{user-defined-procp}}\,({\it{subr\/}}, {\it{proc-list\/}})\index{user-defined-procp} \\ 
$\wedge$$\;\;\;\;${\rm{plistp}}\,({\it{temp-stk\/}})\index{plistp} \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\it{ctrl-stk\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,(\=\+{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, \\ 
{\it{temp-stk\/}})\-\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, {\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match} \\ 
$\wedge$$\;\;\;\;${\rm{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resource-errorp}}\,({\rm{mg-meaning-r}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{resource-errorp}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{append}}\,(\=\+{\rm{reverse}}\,({\rm{mg-to-p-local-values}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{mg-to-p-local-values})\index{reverse}, \\ 
{\rm{map-down-values}}\,(\=\+{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, \\ 
{\it{temp-stk\/}})\-\index{map-down-values})\- \\ 
$=$$\;\;\;\;${\rm{map-down-values}}\,(\=\+{\rm{make-call-var-alist}}\,(\=\+{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, \\ 
{\it{stmt\/}}, \\ 
{\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\-\index{make-call-var-alist}, \\ 
{\rm{make-frame-alist}}\,(\=\+{\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def}, \\ 
{\it{stmt\/}}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\it{temp-stk\/}})\-\index{make-frame-alist}, \\ 
{\rm{append}}\,(\=\+{\rm{reverse}}\,({\rm{mg-to-p-local-values}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{mg-to-p-local-values})\index{reverse}, \\ 
{\rm{map-down-values}}\,(\=\+{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, \\ 
{\it{temp-stk\/}})\-\index{map-down-values})\-)\-\index{map-down-values})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  call-step-initial-equals-state1 \\ \index{call-step-initial-equals-state1}
\=\+(\=\+({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resources-inadequatep}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{resources-inadequatep}) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{r-cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-translation-parameters}}\,({\it{cinfo\/}}, {\it{t-cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}}, {\it{code2\/}})\index{ok-translation-parameters} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statep}}\,({\it{mg-state\/}}, {\it{r-cond-list\/}})\index{ok-mg-statep} \\ 
$\wedge$$\;\;\;\;${\rm{cond-subsetp}}\,({\it{r-cond-list\/}}, {\it{t-cond-list\/}})\index{cond-subsetp} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{code}}\,({\rm{translate-def-body}}\,({\rm{assoc}}\,({\it{subr\/}}, {\it{proc-list\/}}), {\it{proc-list\/}})\index{translate-def-body})\index{code} \\ 
$=$$\;\;\;\;${\rm{append}}\,(\=\+{\rm{code}}\,({\rm{translate}}\,({\it{cinfo\/}}, {\it{t-cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}})\index{translate})\index{code}, \\ 
{\it{code2\/}})\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{user-defined-procp}}\,({\it{subr\/}}, {\it{proc-list\/}})\index{user-defined-procp} \\ 
$\wedge$$\;\;\;\;${\rm{plistp}}\,({\it{temp-stk\/}})\index{plistp} \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\it{ctrl-stk\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,(\=\+{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, \\ 
{\it{temp-stk\/}})\-\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, {\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match} \\ 
$\wedge$$\;\;\;\;${\rm{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resource-errorp}}\,({\rm{mg-meaning-r}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{resource-errorp}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{p-state}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{pc}}, {\rm{cons}}\,({\rm{call-name}}\,({\it{stmt\/}})\index{call-name}, {\tt{0}}))\index{tag}, \\ 
{\rm{push}}\,(\=\+{\rm{p-frame}}\,(\=\+{\rm{append}}\,(\=\+{\rm{pairlist}}\,(\=\+{\rm{cadr}}\,({\rm{assoc}}\,(\=\+{\rm{call-name}}\,({\it{stmt\/}})\index{call-name}, \\ 
{\rm{translate-proc-list}}\,({\it{proc-list\/}})\index{translate-proc-list})\-), \\ 
{\rm{append}}\,(\=\+{\rm{ascending-local-address-sequence}}\,(\=\+{\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals}, \\ 
{\rm{length}}\,({\it{temp-stk\/}})\index{length})\-\index{ascending-local-address-sequence}, \\ 
{\rm{mg-actuals-to-p-actuals}}\,(\=\+{\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{mg-actuals-to-p-actuals})\-)\-, \\ 
{\rm{pair-temps-with-initial-values}}\,({\rm{caddr}}\,({\rm{assoc}}\,(\=\+{\rm{call-name}}\,({\it{stmt\/}})\index{call-name}, \\ 
{\rm{translate-proc-list}}\,({\it{proc-list\/}})\index{translate-proc-list})\-))\index{pair-temps-with-initial-values})\-, \\ 
{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,(\=\+{\it{subr\/}}, \\ 
\=\+{\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} \\ 
$+$$\;\;\;\;${\rm{data-length}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{data-length} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{length} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals})\index{length} \\ 
$+$$\;\;\;\;${\tt{1}}\-)\-)\-\index{tag})\-\index{p-frame}, \\ 
{\it{ctrl-stk\/}})\-\index{push}, \\ 
{\rm{append}}\,(\=\+{\rm{reverse}}\,({\rm{mg-to-p-local-values}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{mg-to-p-local-values})\index{reverse}, \\ 
{\rm{map-down-values}}\,(\=\+{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, \\ 
{\it{temp-stk\/}})\-\index{map-down-values})\-, \\ 
{\rm{translate-proc-list}}\,({\it{proc-list\/}})\index{translate-proc-list}, \\ 
{\rm{list}}\,({\rm{list}}\,({\tt{'}}{\tt{c-c}}, {\rm{mg-cond-to-p-nat}}\,({\rm{cc}}\,({\it{mg-state\/}})\index{cc}, {\it{t-cond-list\/}})\index{mg-cond-to-p-nat})), \\ 
{\sc{mg-max-ctrl-stk-size}}\index{mg-max-ctrl-stk-size}, \\ 
{\sc{mg-max-temp-stk-size}}\index{mg-max-temp-stk-size}, \\ 
{\sc{mg-word-size}}\index{mg-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state} \\ 
$=$$\;\;\;\;${\rm{map-down}}\,(\=\+{\rm{make-call-environment}}\,(\=\+{\it{mg-state\/}}, \\ 
{\it{stmt\/}}, \\ 
{\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\-\index{make-call-environment}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{cons}}\,(\=\+{\rm{p-frame}}\,(\=\+{\rm{make-frame-alist}}\,(\=\+{\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def}, \\ 
{\it{stmt\/}}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\it{temp-stk\/}})\-\index{make-frame-alist}, \\ 
{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,(\=\+{\it{subr\/}}, \\ 
$1\;+$ (\=\+{\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} \\ 
$+$$\;\;\;\;${\rm{data-length}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{data-length} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{length} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals})\index{length})\-)\-)\-\index{tag})\-\index{p-frame}, \\ 
{\it{ctrl-stk\/}})\-, \\ 
{\rm{append}}\,(\=\+{\rm{reverse}}\,({\rm{mg-to-p-local-values}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{mg-to-p-local-values})\index{reverse}, \\ 
{\rm{map-down-values}}\,(\=\+{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, \\ 
{\it{temp-stk\/}})\-\index{map-down-values})\-, \\ 
{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,(\=\+{\rm{call-name}}\,({\it{stmt\/}})\index{call-name}, \\ 
{\rm{length}}\,({\rm{code}}\,({\rm{make-cinfo}}\,(\=\+{\bf{nil}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}\=\+{\tt{routineerror}} \\ 
{\tt{.\ }}{\tt{0}}{\tt{)}}\-, \\ 
{\rm{make-label-alist}}\,(\=\+{\rm{make-cond-list}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{make-cond-list}, \\ 
{\tt{0}})\-\index{make-label-alist})\-, \\ 
{\tt{1}})\-\index{make-cinfo})\index{code})\index{length})\-)\-\index{tag}, \\ 
{\rm{make-cond-list}}\,({\rm{fetch-called-def}}\,({\it{stmt\/}}, {\it{proc-list\/}})\index{fetch-called-def})\index{make-cond-list})\-\index{map-down})\-\-
\end{tabbing}

\begin{verbatim};; This lemma characterizes the bevavior all of the way through the call-body

\end{verbatim}%\item 
\begin{verbatim}


;; This lemma characterizes the bevavior all of the way through the call-body

(prove-lemma call-step-initial-to-state2 (rewrite)
      (IMPLIES
       (AND (NOT (ZEROP N))
	    (NOT (RESOURCES-INADEQUATEP STMT PROC-LIST
					(LIST (LENGTH TEMP-STK)
					      (P-CTRL-STK-SIZE CTRL-STK))))
	    (EQUAL (CAR STMT) 'PROC-CALL-MG)
	    (OK-MG-STATEMENT STMT R-COND-LIST NAME-ALIST PROC-LIST)
	    (OK-MG-DEF-PLISTP PROC-LIST)
	    (OK-TRANSLATION-PARAMETERS CINFO T-COND-LIST STMT PROC-LIST CODE2)
	    (OK-MG-STATEP MG-STATE R-COND-LIST)
	    (COND-SUBSETP R-COND-LIST T-COND-LIST)
	    (EQUAL (CODE (TRANSLATE-DEF-BODY (ASSOC SUBR PROC-LIST)
					     PROC-LIST))
		   (APPEND (CODE (TRANSLATE CINFO T-COND-LIST STMT PROC-LIST))
			   CODE2))
	    (USER-DEFINED-PROCP SUBR PROC-LIST)
	    (PLISTP TEMP-STK)
	    (LISTP CTRL-STK)
	    (MG-VARS-LIST-OK-IN-P-STATE (MG-ALIST MG-STATE)
					(BINDINGS (TOP CTRL-STK))
					TEMP-STK)
	    (NO-P-ALIASING (BINDINGS (TOP CTRL-STK))
			   (MG-ALIST MG-STATE))
	    (SIGNATURES-MATCH (MG-ALIST MG-STATE)
			      NAME-ALIST)
	    (NORMAL MG-STATE)
	    (ALL-CARS-UNIQUE (MG-ALIST MG-STATE))
	    (NOT (RESOURCE-ERRORP (MG-MEANING-R STMT PROC-LIST MG-STATE N
						(LIST (LENGTH TEMP-STK)
						      (P-CTRL-STK-SIZE CTRL-STK)))))
            (EQUAL
	      (P
	       (MAP-DOWN                                              ;; state1
		(MAKE-CALL-ENVIRONMENT MG-STATE STMT
				       (FETCH-CALLED-DEF STMT PROC-LIST))
		PROC-LIST
		(CONS
		 (P-FRAME
		  (MAKE-FRAME-ALIST (FETCH-CALLED-DEF STMT PROC-LIST)
				    STMT CTRL-STK TEMP-STK)
		  (TAG 'PC
		       (CONS SUBR
			     (ADD1
			      (PLUS (LENGTH (CODE CINFO))
				    (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
				    (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
				    (LENGTH (CALL-ACTUALS STMT)))))))
		 CTRL-STK)
		(APPEND
		 (REVERSE
		  (MG-TO-P-LOCAL-VALUES (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))))
		 (MAP-DOWN-VALUES (MG-ALIST MG-STATE)
				  (BINDINGS (TOP CTRL-STK))
				  TEMP-STK))
		(TAG 'PC
		     (CONS
		      (CALL-NAME STMT)
		      (LENGTH
		       (CODE
			(MAKE-CINFO NIL
				    (CONS
				     '(ROUTINEERROR . 0)
				     (MAKE-LABEL-ALIST
				      (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))
				      0))
				    1)))))
		(MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST)))
	       (CLOCK (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
		      PROC-LIST
		      (MAKE-CALL-ENVIRONMENT MG-STATE STMT
					     (FETCH-CALLED-DEF STMT PROC-LIST))
		      (SUB1 N)))
	      (P-STATE                                     ;; state2
	       (TAG 'PC
		    (CONS
		     (CALL-NAME STMT)
		     (IF
		      (NORMAL
		       (MG-MEANING-R
			(DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
			PROC-LIST
			(MAKE-CALL-ENVIRONMENT MG-STATE STMT
					       (FETCH-CALLED-DEF STMT PROC-LIST))
			(SUB1 N)
			(LIST
			 (LENGTH
			  (APPEND
			   (REVERSE
			    (MG-TO-P-LOCAL-VALUES
			     (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))))
			   (MAP-DOWN-VALUES (MG-ALIST MG-STATE)
					    (BINDINGS (TOP CTRL-STK))
					    TEMP-STK)))
			 (P-CTRL-STK-SIZE
			  (CONS
			   (P-FRAME
			    (MAKE-FRAME-ALIST (FETCH-CALLED-DEF STMT PROC-LIST)
					      STMT CTRL-STK TEMP-STK)
			    (TAG 'PC
				 (CONS SUBR
				       (ADD1
					(PLUS
					 (LENGTH (CODE CINFO))
					 (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
					 (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
					 (LENGTH (CALL-ACTUALS STMT)))))))
			   CTRL-STK)))))
		      (LENGTH
		       (CODE
			(TRANSLATE
			 (MAKE-CINFO NIL
				     (CONS
				      '(ROUTINEERROR . 0)
				      (MAKE-LABEL-ALIST
				       (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))
				       0))
				     1)
			 (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))
			 (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
			 PROC-LIST)))
		      (FIND-LABEL
		       (FETCH-LABEL
			(CC
			 (MG-MEANING-R
			  (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
			  PROC-LIST
			  (MAKE-CALL-ENVIRONMENT MG-STATE STMT
						 (FETCH-CALLED-DEF STMT PROC-LIST))
			  (SUB1 N)
			  (LIST
			   (LENGTH
			    (APPEND
			     (REVERSE
			      (MG-TO-P-LOCAL-VALUES
                               (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))))
			     (MAP-DOWN-VALUES (MG-ALIST MG-STATE)
					      (BINDINGS (TOP CTRL-STK))
					      TEMP-STK)))
			   (P-CTRL-STK-SIZE
			    (CONS
			     (P-FRAME
			      (MAKE-FRAME-ALIST (FETCH-CALLED-DEF STMT PROC-LIST)
						STMT CTRL-STK TEMP-STK)
			      (TAG 'PC
				   (CONS SUBR
					 (ADD1
					  (PLUS
					   (LENGTH (CODE CINFO))
					   (DATA-LENGTH
					    (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
					   (LENGTH
					    (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
					   (LENGTH (CALL-ACTUALS STMT)))))))
			     CTRL-STK)))))
			(LABEL-ALIST
			 (TRANSLATE
			  (MAKE-CINFO NIL
				      (CONS
				       '(ROUTINEERROR . 0)
				       (MAKE-LABEL-ALIST
					(MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))
					0))
				      1)
			  (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))
			  (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
			  PROC-LIST)))
		       (APPEND
			(CODE
			 (TRANSLATE
			  (MAKE-CINFO NIL
				      (CONS
				       '(ROUTINEERROR . 0)
				       (MAKE-LABEL-ALIST
					(MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))
					0))
				      1)
			  (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))
			  (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
			  PROC-LIST))
			(CONS
			 '(DL 0 NIL (NO-OP))
			 (CONS
			  (LIST 'POP* (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))))
			  '((RET)))))))))
	       (CONS
		(P-FRAME
		 (MAKE-FRAME-ALIST (FETCH-CALLED-DEF STMT PROC-LIST)
				   STMT CTRL-STK TEMP-STK)
		 (TAG 'PC
		      (CONS SUBR
			    (ADD1
			     (PLUS (LENGTH (CODE CINFO))
				   (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
				   (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
				   (LENGTH (CALL-ACTUALS STMT)))))))
		CTRL-STK)
	       (MAP-DOWN-VALUES
		(MG-ALIST
		 (MG-MEANING-R
		  (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
		  PROC-LIST
		  (MAKE-CALL-ENVIRONMENT MG-STATE STMT
					 (FETCH-CALLED-DEF STMT PROC-LIST))
		  (SUB1 N)
		  (LIST
		   (LENGTH
		    (APPEND
		     (REVERSE
		      (MG-TO-P-LOCAL-VALUES
		       (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))))
		     (MAP-DOWN-VALUES (MG-ALIST MG-STATE)
				      (BINDINGS (TOP CTRL-STK))
				      TEMP-STK)))
		   (P-CTRL-STK-SIZE
		    (CONS
		     (P-FRAME
		      (MAKE-FRAME-ALIST (FETCH-CALLED-DEF STMT PROC-LIST)
					STMT CTRL-STK TEMP-STK)
		      (TAG 'PC
			   (CONS SUBR
				 (ADD1
				  (PLUS
				   (LENGTH (CODE CINFO))
				   (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
				   (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
				   (LENGTH (CALL-ACTUALS STMT)))))))
		     CTRL-STK)))))
		(BINDINGS
		 (TOP
		  (CONS
		   (P-FRAME
		    (MAKE-FRAME-ALIST (FETCH-CALLED-DEF STMT PROC-LIST)
				      STMT CTRL-STK TEMP-STK)
		    (TAG 'PC
			 (CONS SUBR
			       (ADD1
				(PLUS (LENGTH (CODE CINFO))
				      (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
				      (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
				      (LENGTH (CALL-ACTUALS STMT)))))))
		   CTRL-STK)))
		(APPEND
		 (REVERSE
		  (MG-TO-P-LOCAL-VALUES (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))))
		 (MAP-DOWN-VALUES (MG-ALIST MG-STATE)
				  (BINDINGS (TOP CTRL-STK))
				  TEMP-STK)))
	       (TRANSLATE-PROC-LIST PROC-LIST)
	       (LIST
		(LIST 'C-C
		      (MG-COND-TO-P-NAT
		       (CC
			(MG-MEANING-R
			 (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
			 PROC-LIST
			 (MAKE-CALL-ENVIRONMENT MG-STATE STMT
						(FETCH-CALLED-DEF STMT PROC-LIST))
			 (SUB1 N)
			 (LIST
			  (LENGTH
			   (APPEND
			    (REVERSE
			     (MG-TO-P-LOCAL-VALUES
			      (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))))
			    (MAP-DOWN-VALUES (MG-ALIST MG-STATE)
					     (BINDINGS (TOP CTRL-STK))
					     TEMP-STK)))
			  (P-CTRL-STK-SIZE
			   (CONS
			    (P-FRAME
			     (MAKE-FRAME-ALIST (FETCH-CALLED-DEF STMT PROC-LIST)
					       STMT CTRL-STK TEMP-STK)
			     (TAG 'PC
				  (CONS SUBR
					(ADD1
					 (PLUS
					  (LENGTH (CODE CINFO))
					  (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
					  (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
					  (LENGTH (CALL-ACTUALS STMT)))))))
			    CTRL-STK)))))
		       (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST)))))
	       (MG-MAX-CTRL-STK-SIZE) (MG-MAX-TEMP-STK-SIZE) (MG-WORD-SIZE)
	       'RUN)))
       (EQUAL
	(P (MAP-DOWN MG-STATE PROC-LIST CTRL-STK TEMP-STK
		     (TAG 'PC
			  (CONS SUBR (LENGTH (CODE CINFO))))
		     T-COND-LIST)
           (plus (data-length (def-locals (fetch-called-def stmt proc-list)))
		 (length (def-locals (fetch-called-def stmt proc-list)))
		 (length (call-actuals stmt))
		 1
		 (CLOCK (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
			PROC-LIST
			(MAKE-CALL-ENVIRONMENT MG-STATE STMT
					       (FETCH-CALLED-DEF STMT PROC-LIST))
			(SUB1 N))))
	      (P-STATE                                     ;; state2
	       (TAG 'PC
		    (CONS
		     (CALL-NAME STMT)
		     (IF
		      (NORMAL
		       (MG-MEANING-R
			(DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
			PROC-LIST
			(MAKE-CALL-ENVIRONMENT MG-STATE STMT
					       (FETCH-CALLED-DEF STMT PROC-LIST))
			(SUB1 N)
			(LIST
			 (LENGTH
			  (APPEND
			   (REVERSE
			    (MG-TO-P-LOCAL-VALUES
			     (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))))
			   (MAP-DOWN-VALUES (MG-ALIST MG-STATE)
					    (BINDINGS (TOP CTRL-STK))
					    TEMP-STK)))
			 (P-CTRL-STK-SIZE
			  (CONS
			   (P-FRAME
			    (MAKE-FRAME-ALIST (FETCH-CALLED-DEF STMT PROC-LIST)
					      STMT CTRL-STK TEMP-STK)
			    (TAG 'PC
				 (CONS SUBR
				       (ADD1
					(PLUS
					 (LENGTH (CODE CINFO))
					 (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
					 (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
					 (LENGTH (CALL-ACTUALS STMT)))))))
			   CTRL-STK)))))
		      (LENGTH
		       (CODE
			(TRANSLATE
			 (MAKE-CINFO NIL
				     (CONS
				      '(ROUTINEERROR . 0)
				      (MAKE-LABEL-ALIST
				       (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))
				       0))
				     1)
			 (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))
			 (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
			 PROC-LIST)))
		      (FIND-LABEL
		       (FETCH-LABEL
			(CC
			 (MG-MEANING-R
			  (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
			  PROC-LIST
			  (MAKE-CALL-ENVIRONMENT MG-STATE STMT
						 (FETCH-CALLED-DEF STMT PROC-LIST))
			  (SUB1 N)
			  (LIST
			   (LENGTH
			    (APPEND
			     (REVERSE
			      (MG-TO-P-LOCAL-VALUES
                               (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))))
			     (MAP-DOWN-VALUES (MG-ALIST MG-STATE)
					      (BINDINGS (TOP CTRL-STK))
					      TEMP-STK)))
			   (P-CTRL-STK-SIZE
			    (CONS
			     (P-FRAME
			      (MAKE-FRAME-ALIST (FETCH-CALLED-DEF STMT PROC-LIST)
						STMT CTRL-STK TEMP-STK)
			      (TAG 'PC
				   (CONS SUBR
					 (ADD1
					  (PLUS
					   (LENGTH (CODE CINFO))
					   (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
					   (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
					   (LENGTH (CALL-ACTUALS STMT)))))))
			     CTRL-STK)))))
			(LABEL-ALIST
			 (TRANSLATE
			  (MAKE-CINFO NIL
				      (CONS
				       '(ROUTINEERROR . 0)
				       (MAKE-LABEL-ALIST
					(MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))
					0))
				      1)
			  (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))
			  (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
			  PROC-LIST)))
		       (APPEND
			(CODE
			 (TRANSLATE
			  (MAKE-CINFO NIL
				      (CONS
				       '(ROUTINEERROR . 0)
				       (MAKE-LABEL-ALIST
					(MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))
					0))
				      1)
			  (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))
			  (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
			  PROC-LIST))
			(CONS
			 '(DL 0 NIL (NO-OP))
			 (CONS
			  (LIST 'POP* (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))))
			  '((RET)))))))))
	       (CONS
		(P-FRAME
		 (MAKE-FRAME-ALIST (FETCH-CALLED-DEF STMT PROC-LIST)
				   STMT CTRL-STK TEMP-STK)
		 (TAG 'PC
		      (CONS SUBR
			    (ADD1
			     (PLUS (LENGTH (CODE CINFO))
				   (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
				   (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
				   (LENGTH (CALL-ACTUALS STMT)))))))
		CTRL-STK)
	       (MAP-DOWN-VALUES
		(MG-ALIST
		 (MG-MEANING-R
		  (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
		  PROC-LIST
		  (MAKE-CALL-ENVIRONMENT MG-STATE STMT
					 (FETCH-CALLED-DEF STMT PROC-LIST))
		  (SUB1 N)
		  (LIST
		   (LENGTH
		    (APPEND
		     (REVERSE
		      (MG-TO-P-LOCAL-VALUES
		       (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))))
		     (MAP-DOWN-VALUES (MG-ALIST MG-STATE)
				      (BINDINGS (TOP CTRL-STK))
				      TEMP-STK)))
		   (P-CTRL-STK-SIZE
		    (CONS
		     (P-FRAME
		      (MAKE-FRAME-ALIST (FETCH-CALLED-DEF STMT PROC-LIST)
					STMT CTRL-STK TEMP-STK)
		      (TAG 'PC
			   (CONS SUBR
				 (ADD1
				  (PLUS
				   (LENGTH (CODE CINFO))
				   (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
				   (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
				   (LENGTH (CALL-ACTUALS STMT)))))))
		     CTRL-STK)))))
		(BINDINGS
		 (TOP
		  (CONS
		   (P-FRAME
		    (MAKE-FRAME-ALIST (FETCH-CALLED-DEF STMT PROC-LIST)
				      STMT CTRL-STK TEMP-STK)
		    (TAG 'PC
			 (CONS SUBR
			       (ADD1
				(PLUS (LENGTH (CODE CINFO))
				      (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
				      (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
				      (LENGTH (CALL-ACTUALS STMT)))))))
		   CTRL-STK)))
		(APPEND
		 (REVERSE
		  (MG-TO-P-LOCAL-VALUES (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))))
		 (MAP-DOWN-VALUES (MG-ALIST MG-STATE)
				  (BINDINGS (TOP CTRL-STK))
				  TEMP-STK)))
	       (TRANSLATE-PROC-LIST PROC-LIST)
	       (LIST
		(LIST 'C-C
		      (MG-COND-TO-P-NAT
		       (CC
			(MG-MEANING-R
			 (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
			 PROC-LIST
			 (MAKE-CALL-ENVIRONMENT MG-STATE STMT
						(FETCH-CALLED-DEF STMT PROC-LIST))
			 (SUB1 N)
			 (LIST
			  (LENGTH
			   (APPEND
			    (REVERSE
			     (MG-TO-P-LOCAL-VALUES
			      (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))))
			    (MAP-DOWN-VALUES (MG-ALIST MG-STATE)
					     (BINDINGS (TOP CTRL-STK))
					     TEMP-STK)))
			  (P-CTRL-STK-SIZE
			   (CONS
			    (P-FRAME
			     (MAKE-FRAME-ALIST (FETCH-CALLED-DEF STMT PROC-LIST)
					       STMT CTRL-STK TEMP-STK)
			     (TAG 'PC
				  (CONS SUBR
					(ADD1
					 (PLUS
					  (LENGTH (CODE CINFO))
					  (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
					  (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
					  (LENGTH (CALL-ACTUALS STMT)))))))
			    CTRL-STK)))))
		       (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST)))))
	       (MG-MAX-CTRL-STK-SIZE) (MG-MAX-TEMP-STK-SIZE) (MG-WORD-SIZE)
	       'RUN)))
 ((INSTRUCTIONS
   (ADD-ABBREVIATION @INITIAL
                     (MAP-DOWN MG-STATE PROC-LIST CTRL-STK TEMP-STK
                               (TAG 'PC
                                    (CONS SUBR (LENGTH (CODE CINFO))))
                               T-COND-LIST))
   (ADD-ABBREVIATION @STATE1
    (MAP-DOWN
     (MAKE-CALL-ENVIRONMENT MG-STATE STMT
                            (FETCH-CALLED-DEF STMT PROC-LIST))
     PROC-LIST
     (CONS
      (P-FRAME
       (MAKE-FRAME-ALIST (FETCH-CALLED-DEF STMT PROC-LIST)
                         STMT CTRL-STK TEMP-STK)
       (TAG 'PC
        (CONS SUBR
         (ADD1
             (PLUS (LENGTH (CODE CINFO))
                   (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
                   (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
                   (LENGTH (CALL-ACTUALS STMT)))))))
      CTRL-STK)
     (APPEND
      (REVERSE
         (MG-TO-P-LOCAL-VALUES (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))))
      (MAP-DOWN-VALUES (MG-ALIST MG-STATE)
                       (BINDINGS (TOP CTRL-STK))
                       TEMP-STK))
     (TAG 'PC
      (CONS
       (CALL-NAME STMT)
       (LENGTH
        (CODE
         (MAKE-CINFO NIL
          (CONS
           '(ROUTINEERROR . 0)
           (MAKE-LABEL-ALIST (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))
                             0))
          1)))))
     (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))))
   (ADD-ABBREVIATION @STATE2
    (P-STATE
     (TAG 'PC
      (CONS
       (CALL-NAME STMT)
       (IF
        (NORMAL
         (MG-MEANING-R
          (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
          PROC-LIST
          (MAKE-CALL-ENVIRONMENT MG-STATE STMT
                                 (FETCH-CALLED-DEF STMT PROC-LIST))
          (SUB1 N)
          (LIST
           (LENGTH
            (APPEND
             (REVERSE
              (MG-TO-P-LOCAL-VALUES
                               (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))))
             (MAP-DOWN-VALUES (MG-ALIST MG-STATE)
                              (BINDINGS (TOP CTRL-STK))
                              TEMP-STK)))
           (P-CTRL-STK-SIZE
            (CONS
             (P-FRAME
              (MAKE-FRAME-ALIST (FETCH-CALLED-DEF STMT PROC-LIST)
                                STMT CTRL-STK TEMP-STK)
              (TAG 'PC
               (CONS SUBR
                (ADD1
                 (PLUS
                   (LENGTH (CODE CINFO))
                   (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
                   (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
                   (LENGTH (CALL-ACTUALS STMT)))))))
             CTRL-STK)))))
        (LENGTH
         (CODE
          (TRANSLATE
           (MAKE-CINFO NIL
            (CONS
             '(ROUTINEERROR . 0)
             (MAKE-LABEL-ALIST
                             (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))
                             0))
            1)
           (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))
           (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
           PROC-LIST)))
        (FIND-LABEL
         (FETCH-LABEL
          (CC
           (MG-MEANING-R
            (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
            PROC-LIST
            (MAKE-CALL-ENVIRONMENT MG-STATE STMT
                                   (FETCH-CALLED-DEF STMT PROC-LIST))
            (SUB1 N)
            (LIST
             (LENGTH
              (APPEND
               (REVERSE
                (MG-TO-P-LOCAL-VALUES
                               (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))))
               (MAP-DOWN-VALUES (MG-ALIST MG-STATE)
                                (BINDINGS (TOP CTRL-STK))
                                TEMP-STK)))
             (P-CTRL-STK-SIZE
              (CONS
               (P-FRAME
                (MAKE-FRAME-ALIST (FETCH-CALLED-DEF STMT PROC-LIST)
                                  STMT CTRL-STK TEMP-STK)
                (TAG 'PC
                 (CONS SUBR
                  (ADD1
                   (PLUS
                    (LENGTH (CODE CINFO))
                    (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
                    (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
                    (LENGTH (CALL-ACTUALS STMT)))))))
               CTRL-STK)))))
          (LABEL-ALIST
           (TRANSLATE
            (MAKE-CINFO NIL
             (CONS
              '(ROUTINEERROR . 0)
              (MAKE-LABEL-ALIST
                             (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))
                             0))
             1)
            (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))
            (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
            PROC-LIST)))
         (APPEND
          (CODE
           (TRANSLATE
            (MAKE-CINFO NIL
             (CONS
              '(ROUTINEERROR . 0)
              (MAKE-LABEL-ALIST
                             (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))
                             0))
             1)
            (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))
            (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
            PROC-LIST))
          (CONS
           '(DL 0 NIL (NO-OP))
           (CONS
            (LIST 'POP* (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))))
            '((RET)))))))))
     (CONS
      (P-FRAME
       (MAKE-FRAME-ALIST (FETCH-CALLED-DEF STMT PROC-LIST)
                         STMT CTRL-STK TEMP-STK)
       (TAG 'PC
        (CONS SUBR
         (ADD1
             (PLUS (LENGTH (CODE CINFO))
                   (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
                   (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
                   (LENGTH (CALL-ACTUALS STMT)))))))
      CTRL-STK)
     (MAP-DOWN-VALUES
      (MG-ALIST
       (MG-MEANING-R
        (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
        PROC-LIST
        (MAKE-CALL-ENVIRONMENT MG-STATE STMT
                               (FETCH-CALLED-DEF STMT PROC-LIST))
        (SUB1 N)
        (LIST
         (LENGTH
          (APPEND
           (REVERSE
            (MG-TO-P-LOCAL-VALUES
                               (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))))
           (MAP-DOWN-VALUES (MG-ALIST MG-STATE)
                            (BINDINGS (TOP CTRL-STK))
                            TEMP-STK)))
         (P-CTRL-STK-SIZE
          (CONS
           (P-FRAME
            (MAKE-FRAME-ALIST (FETCH-CALLED-DEF STMT PROC-LIST)
                              STMT CTRL-STK TEMP-STK)
            (TAG 'PC
             (CONS SUBR
              (ADD1
               (PLUS
                   (LENGTH (CODE CINFO))
                   (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
                   (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
                   (LENGTH (CALL-ACTUALS STMT)))))))
           CTRL-STK)))))
      (BINDINGS
       (TOP
        (CONS
         (P-FRAME
          (MAKE-FRAME-ALIST (FETCH-CALLED-DEF STMT PROC-LIST)
                            STMT CTRL-STK TEMP-STK)
          (TAG 'PC
           (CONS SUBR
            (ADD1
             (PLUS (LENGTH (CODE CINFO))
                   (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
                   (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
                   (LENGTH (CALL-ACTUALS STMT)))))))
         CTRL-STK)))
      (APPEND
       (REVERSE
         (MG-TO-P-LOCAL-VALUES (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))))
       (MAP-DOWN-VALUES (MG-ALIST MG-STATE)
                        (BINDINGS (TOP CTRL-STK))
                        TEMP-STK)))
     (TRANSLATE-PROC-LIST PROC-LIST)
     (LIST
      (LIST 'C-C
       (MG-COND-TO-P-NAT
        (CC
         (MG-MEANING-R
          (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
          PROC-LIST
          (MAKE-CALL-ENVIRONMENT MG-STATE STMT
                                 (FETCH-CALLED-DEF STMT PROC-LIST))
          (SUB1 N)
          (LIST
           (LENGTH
            (APPEND
             (REVERSE
              (MG-TO-P-LOCAL-VALUES
                               (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))))
             (MAP-DOWN-VALUES (MG-ALIST MG-STATE)
                              (BINDINGS (TOP CTRL-STK))
                              TEMP-STK)))
           (P-CTRL-STK-SIZE
            (CONS
             (P-FRAME
              (MAKE-FRAME-ALIST (FETCH-CALLED-DEF STMT PROC-LIST)
                                STMT CTRL-STK TEMP-STK)
              (TAG 'PC
               (CONS SUBR
                (ADD1
                 (PLUS
                   (LENGTH (CODE CINFO))
                   (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
                   (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
                   (LENGTH (CALL-ACTUALS STMT)))))))
             CTRL-STK)))))
        (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST)))))
     (MG-MAX-CTRL-STK-SIZE) (MG-MAX-TEMP-STK-SIZE) (MG-WORD-SIZE)
     'RUN))
   (ADD-ABBREVIATION @BODY-TIME
               (CLOCK (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
                      PROC-LIST
                      (MAKE-CALL-ENVIRONMENT MG-STATE STMT
                                             (FETCH-CALLED-DEF STMT PROC-LIST))
                      (SUB1 N)))
   (ADD-ABBREVIATION @TIME-TO-STATE1
             (PLUS (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
                   (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
                   (LENGTH (CALL-ACTUALS STMT))
                   1))
   PROMOTE
   (DIVE 1 2)
   (= (PLUS (PLUS (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
                  (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
                  (LENGTH (CALL-ACTUALS STMT))
                  1)
            @BODY-TIME))
   UP
   (REWRITE P-PLUS-LEMMA)
   (DIVE 1)
   (REWRITE CALL-STEPS-TO-BODY)
   (REWRITE CALL-STEP-INITIAL-EQUALS-STATE1)
   UP UP
   (DEMOTE 19)
   S-PROP)))
\end{verbatim}



\noindent{\sc Event}:   Enable make-call-environment.

\addvspace{18pt}

%\item 
\begin{verbatim}


(prove-lemma call-state2-step1-effect (rewrite)
      (IMPLIES
       (AND (NOT (ZEROP N))
	    (NOT (RESOURCES-INADEQUATEP STMT PROC-LIST
					(LIST (LENGTH TEMP-STK)
					      (P-CTRL-STK-SIZE CTRL-STK))))
	    (EQUAL (CAR STMT) 'PROC-CALL-MG)
	    (OK-MG-STATEMENT STMT R-COND-LIST NAME-ALIST PROC-LIST)
	    (OK-MG-DEF-PLISTP PROC-LIST)
	    (OK-TRANSLATION-PARAMETERS CINFO T-COND-LIST STMT PROC-LIST CODE2)
	    (OK-MG-STATEP MG-STATE R-COND-LIST)
	    (COND-SUBSETP R-COND-LIST T-COND-LIST)
	    (EQUAL (CODE (TRANSLATE-DEF-BODY (ASSOC SUBR PROC-LIST)
					     PROC-LIST))
		   (APPEND (CODE (TRANSLATE CINFO T-COND-LIST STMT PROC-LIST))
			   CODE2))
	    (USER-DEFINED-PROCP SUBR PROC-LIST)
	    (PLISTP TEMP-STK)
	    (LISTP CTRL-STK)
	    (MG-VARS-LIST-OK-IN-P-STATE (MG-ALIST MG-STATE)
					(BINDINGS (TOP CTRL-STK))
					TEMP-STK)
	    (NO-P-ALIASING (BINDINGS (TOP CTRL-STK))
			   (MG-ALIST MG-STATE))
	    (SIGNATURES-MATCH (MG-ALIST MG-STATE)
			      NAME-ALIST)
	    (NORMAL MG-STATE)
	    (ALL-CARS-UNIQUE (MG-ALIST MG-STATE))
	    (NOT (RESOURCE-ERRORP (MG-MEANING-R STMT PROC-LIST MG-STATE N
						(LIST (LENGTH TEMP-STK)
						      (P-CTRL-STK-SIZE CTRL-STK))))))
     (equal 
      (p-step
       	      (P-STATE                                     ;; state2
	       (TAG 'PC
		    (CONS
		     (CALL-NAME STMT)
		     (IF
		      (NORMAL
		       (MG-MEANING-R
			(DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
			PROC-LIST
			(MAKE-CALL-ENVIRONMENT MG-STATE STMT
					       (FETCH-CALLED-DEF STMT PROC-LIST))
			(SUB1 N)
			(LIST
			 (LENGTH
			  (APPEND
			   (REVERSE
			    (MG-TO-P-LOCAL-VALUES
			     (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))))
			   (MAP-DOWN-VALUES (MG-ALIST MG-STATE)
					    (BINDINGS (TOP CTRL-STK))
					    TEMP-STK)))
			 (P-CTRL-STK-SIZE
			  (CONS
			   (P-FRAME
			    (MAKE-FRAME-ALIST (FETCH-CALLED-DEF STMT PROC-LIST)
					      STMT CTRL-STK TEMP-STK)
			    (TAG 'PC
				 (CONS SUBR
				       (ADD1
					(PLUS
					 (LENGTH (CODE CINFO))
					 (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
					 (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
					 (LENGTH (CALL-ACTUALS STMT)))))))
			   CTRL-STK)))))
		      (LENGTH
		       (CODE
			(TRANSLATE
			 (MAKE-CINFO NIL
				     (CONS
				      '(ROUTINEERROR . 0)
				      (MAKE-LABEL-ALIST
				       (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))
				       0))
				     1)
			 (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))
			 (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
			 PROC-LIST)))
		      (FIND-LABEL
		       (FETCH-LABEL
			(CC
			 (MG-MEANING-R
			  (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
			  PROC-LIST
			  (MAKE-CALL-ENVIRONMENT MG-STATE STMT
						 (FETCH-CALLED-DEF STMT PROC-LIST))
			  (SUB1 N)
			  (LIST
			   (LENGTH
			    (APPEND
			     (REVERSE
			      (MG-TO-P-LOCAL-VALUES
                               (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))))
			     (MAP-DOWN-VALUES (MG-ALIST MG-STATE)
					      (BINDINGS (TOP CTRL-STK))
					      TEMP-STK)))
			   (P-CTRL-STK-SIZE
			    (CONS
			     (P-FRAME
			      (MAKE-FRAME-ALIST (FETCH-CALLED-DEF STMT PROC-LIST)
						STMT CTRL-STK TEMP-STK)
			      (TAG 'PC
				   (CONS SUBR
					 (ADD1
					  (PLUS
					   (LENGTH (CODE CINFO))
					   (DATA-LENGTH
					    (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
					   (LENGTH
					    (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
					   (LENGTH (CALL-ACTUALS STMT)))))))
			     CTRL-STK)))))
			(LABEL-ALIST
			 (TRANSLATE
			  (MAKE-CINFO NIL
				      (CONS
				       '(ROUTINEERROR . 0)
				       (MAKE-LABEL-ALIST
					(MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))
					0))
				      1)
			  (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))
			  (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
			  PROC-LIST)))
		       (APPEND
			(CODE
			 (TRANSLATE
			  (MAKE-CINFO NIL
				      (CONS
				       '(ROUTINEERROR . 0)
				       (MAKE-LABEL-ALIST
					(MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))
					0))
				      1)
			  (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))
			  (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
			  PROC-LIST))
			(CONS
			 '(DL 0 NIL (NO-OP))
			 (CONS
			  (LIST 'POP* (Data-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))))
			  '((RET)))))))))
	       (CONS
		(P-FRAME
		 (MAKE-FRAME-ALIST (FETCH-CALLED-DEF STMT PROC-LIST)
				   STMT CTRL-STK TEMP-STK)
		 (TAG 'PC
		      (CONS SUBR
			    (ADD1
			     (PLUS (LENGTH (CODE CINFO))
				   (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
				   (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
				   (LENGTH (CALL-ACTUALS STMT)))))))
		CTRL-STK)
	       (MAP-DOWN-VALUES
		(MG-ALIST
		 (MG-MEANING-R
		  (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
		  PROC-LIST
		  (MAKE-CALL-ENVIRONMENT MG-STATE STMT
					 (FETCH-CALLED-DEF STMT PROC-LIST))
		  (SUB1 N)
		  (LIST
		   (LENGTH
		    (APPEND
		     (REVERSE
		      (MG-TO-P-LOCAL-VALUES
		       (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))))
		     (MAP-DOWN-VALUES (MG-ALIST MG-STATE)
				      (BINDINGS (TOP CTRL-STK))
				      TEMP-STK)))
		   (P-CTRL-STK-SIZE
		    (CONS
		     (P-FRAME
		      (MAKE-FRAME-ALIST (FETCH-CALLED-DEF STMT PROC-LIST)
					STMT CTRL-STK TEMP-STK)
		      (TAG 'PC
			   (CONS SUBR
				 (ADD1
				  (PLUS
				   (LENGTH (CODE CINFO))
				   (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
				   (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
				   (LENGTH (CALL-ACTUALS STMT)))))))
		     CTRL-STK)))))
		(BINDINGS
		 (TOP
		  (CONS
		   (P-FRAME
		    (MAKE-FRAME-ALIST (FETCH-CALLED-DEF STMT PROC-LIST)
				      STMT CTRL-STK TEMP-STK)
		    (TAG 'PC
			 (CONS SUBR
			       (ADD1
				(PLUS (LENGTH (CODE CINFO))
				      (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
				      (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
				      (LENGTH (CALL-ACTUALS STMT)))))))
		   CTRL-STK)))
		(APPEND
		 (REVERSE
		  (MG-TO-P-LOCAL-VALUES (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))))
		 (MAP-DOWN-VALUES (MG-ALIST MG-STATE)
				  (BINDINGS (TOP CTRL-STK))
				  TEMP-STK)))
	       (TRANSLATE-PROC-LIST PROC-LIST)
	       (LIST
		(LIST 'C-C
		      (MG-COND-TO-P-NAT
		       (CC
			(MG-MEANING-R
			 (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
			 PROC-LIST
			 (MAKE-CALL-ENVIRONMENT MG-STATE STMT
						(FETCH-CALLED-DEF STMT PROC-LIST))
			 (SUB1 N)
			 (LIST
			  (LENGTH
			   (APPEND
			    (REVERSE
			     (MG-TO-P-LOCAL-VALUES
			      (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))))
			    (MAP-DOWN-VALUES (MG-ALIST MG-STATE)
					     (BINDINGS (TOP CTRL-STK))
					     TEMP-STK)))
			  (P-CTRL-STK-SIZE
			   (CONS
			    (P-FRAME
			     (MAKE-FRAME-ALIST (FETCH-CALLED-DEF STMT PROC-LIST)
					       STMT CTRL-STK TEMP-STK)
			     (TAG 'PC
				  (CONS SUBR
					(ADD1
					 (PLUS
					  (LENGTH (CODE CINFO))
					  (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
					  (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
					  (LENGTH (CALL-ACTUALS STMT)))))))
			    CTRL-STK)))))
		       (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST)))))
	       (MG-MAX-CTRL-STK-SIZE) (MG-MAX-TEMP-STK-SIZE) (MG-WORD-SIZE)
	       'RUN))
       (P-STATE (TAG 'PC
		     (CONS
		      (CALL-NAME STMT)
		      (PLUS
		       (LENGTH
			(CODE
			 (TRANSLATE
			  (MAKE-CINFO NIL
				      (CONS
				       '(ROUTINEERROR . 0)
				       (MAKE-LABEL-ALIST (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))
							 0))
				      1)
			  (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))
			  (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
			  PROC-LIST)))
		       1)))
		(CONS
		 (P-FRAME
		  (APPEND (MAP-CALL-LOCALS (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))
					   (LENGTH TEMP-STK))
			  (MAP-CALL-FORMALS (DEF-FORMALS (FETCH-CALLED-DEF STMT PROC-LIST))
					    (CALL-ACTUALS STMT)
					    (BINDINGS (TOP CTRL-STK))))
		  (TAG 'PC
		       (CONS SUBR
			     (ADD1 (PLUS (LENGTH (CODE CINFO))
					 (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
					 (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
					 (LENGTH (CALL-ACTUALS STMT)))))))
		 CTRL-STK)
		(MAP-DOWN-VALUES
		 (MG-ALIST
		  (MG-MEANING-R
		   (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
		   PROC-LIST
		   (MG-STATE (CC MG-STATE)
			     (MAKE-CALL-VAR-ALIST (MG-ALIST MG-STATE)
						  STMT
						  (FETCH-CALLED-DEF STMT PROC-LIST))
			     (MG-PSW MG-STATE))
		   (SUB1 N)
		   (LIST (PLUS (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
			       (LENGTH TEMP-STK))
			 (PLUS 2
			       (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
			       (LENGTH (DEF-FORMALS (FETCH-CALLED-DEF STMT PROC-LIST)))
			       (P-CTRL-STK-SIZE CTRL-STK)))))
		 (APPEND (MAP-CALL-LOCALS (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))
					  (LENGTH TEMP-STK))
			 (MAP-CALL-FORMALS (DEF-FORMALS (FETCH-CALLED-DEF STMT PROC-LIST))
					   (CALL-ACTUALS STMT)
					   (BINDINGS (TOP CTRL-STK))))
		 (APPEND
		  (REVERSE
		   (MG-TO-P-LOCAL-VALUES (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))))
		  (MAP-DOWN-VALUES (MG-ALIST MG-STATE)
				   (BINDINGS (TOP CTRL-STK))
				   TEMP-STK)))
		(TRANSLATE-PROC-LIST PROC-LIST)
		(LIST
		 (LIST 'C-C
		       (MG-COND-TO-P-NAT
			(CC
			 (MG-MEANING-R
			  (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
			  PROC-LIST
			  (MG-STATE (CC MG-STATE)
				    (MAKE-CALL-VAR-ALIST (MG-ALIST MG-STATE)
							 STMT
							 (FETCH-CALLED-DEF STMT PROC-LIST))
				    (MG-PSW MG-STATE))
			  (SUB1 N)
			  (LIST
			   (PLUS
			    (LENGTH
			     (MG-TO-P-LOCAL-VALUES
			      (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))))
			    (LENGTH (MAP-DOWN-VALUES (MG-ALIST MG-STATE)
						     (BINDINGS (TOP CTRL-STK))
						     TEMP-STK)))
			   (P-CTRL-STK-SIZE
			    (CONS
			     (P-FRAME
			      (APPEND
			       (MAP-CALL-LOCALS (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))
						(LENGTH TEMP-STK))
			       (MAP-CALL-FORMALS (DEF-FORMALS (FETCH-CALLED-DEF STMT PROC-LIST))
						 (CALL-ACTUALS STMT)
						 (BINDINGS (TOP CTRL-STK))))
			      (TAG 'PC
				   (CONS SUBR
					 (ADD1
					  (PLUS
					   (LENGTH (CODE CINFO))
					   (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
					   (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
					   (LENGTH (CALL-ACTUALS STMT)))))))
			     CTRL-STK)))))
			(MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST)))))
                (MG-MAX-CTRL-STK-SIZE) (MG-MAX-TEMP-STK-SIZE) (MG-WORD-SIZE)
		'RUN)))
 ((INSTRUCTIONS
   (ENABLE LENGTH-CONS)
   PROMOTE
   (DIVE 1)
   X
   (S LEMMAS)
   (DIVE 1 1 1)
   (= *
    (LENGTH
     (CODE
      (TRANSLATE
       (MAKE-CINFO NIL
        (CONS
           '(ROUTINEERROR . 0)
           (MAKE-LABEL-ALIST (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))
                             0))
        1)
       (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))
       (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
       PROC-LIST)))
    0)
   UP
   (DIVE 2)
   (REWRITE TRANSLATE-DEF-BODY-REWRITE
    (($CINFO
      (MAKE-CINFO NIL
       (CONS
           (CONS 'ROUTINEERROR 0)
           (MAKE-LABEL-ALIST (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))
                             0))
       1))
     ($T-COND-LIST (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST)))
     ($CODE2
      (LIST '(DL 0 NIL (NO-OP))
            (LIST 'POP*
                  (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))))
            '(RET)))
     ($STMT (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST)))))
   UP
   (REWRITE GET-LENGTH-CAR)
   (S LEMMAS)
   UP X UP X
   (S LEMMAS)
   X
   (S LEMMAS)
   (DIVE 1 2 2 1)
   (= *
    (LENGTH
     (CODE
      (TRANSLATE
       (MAKE-CINFO NIL
        (CONS
           '(ROUTINEERROR . 0)
           (MAKE-LABEL-ALIST (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))
                             0))
        1)
       (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))
       (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
       PROC-LIST)))
    0)
   UP UP UP UP
   (DIVE 3 1 1 5 1 1)
   (REWRITE LENGTH-MG-TO-P-LOCAL-VALUES)
   NX
   (REWRITE MAP-DOWN-VALUES-PRESERVES-LENGTH)
   UP NX
   (DIVE 1)
   X
   (S LEMMAS)
   (S-PROP P-FRAME-SIZE)
   (S LEMMAS)
   TOP S SPLIT PROVE PROVE
   (REWRITE OK-MG-STATEP-MG-ALIST-MG-ALISTP)
   (REWRITE CALLED-DEF-FORMALS-OK)
   S-PROP SPLIT
   (DIVE 1 1)
   (REWRITE FETCH-LABEL-0-CASE-2)
   UP
   (REWRITE FIND-LABEL-APPEND)
   UP DROP
   (PROVE (ENABLE UNLABEL))
   (DIVE 1)
   (REWRITE FIND-LABELP-MONOTONIC-LESSP)
   TOP S
   (S LEMMAS)
   (S LEMMAS)
   (PROVE (ENABLE OK-MG-STATEMENT OK-PROC-CALL))
   (DIVE 1 1)
   X UP
   (S LEMMAS)
   UP
   (PROVE (ENABLE FETCH-CALLED-DEF FETCH-DEF))
   S-PROP SPLIT
   (DIVE 1 1)
   (REWRITE FETCH-LABEL-0-CASE-2)
   UP
   (REWRITE FIND-LABEL-APPEND)
   TOP DROP
   (PROVE (ENABLE UNLABEL))
   (DIVE 1)
   (REWRITE FIND-LABELP-MONOTONIC-LESSP)
   UP S
   (S LEMMAS)
   (S LEMMAS))))
\end{verbatim}


\begin{tabbing}{\sc Theorem}:  call-body-mg-vars-list-ok1 \\ \index{call-body-mg-vars-list-ok1}
\=\+(\=\+({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resources-inadequatep}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{resources-inadequatep}) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{r-cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-translation-parameters}}\,({\it{cinfo\/}}, {\it{t-cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}}, {\it{code2\/}})\index{ok-translation-parameters} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statep}}\,({\it{mg-state\/}}, {\it{r-cond-list\/}})\index{ok-mg-statep} \\ 
$\wedge$$\;\;\;\;${\rm{cond-subsetp}}\,({\it{r-cond-list\/}}, {\it{t-cond-list\/}})\index{cond-subsetp} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{code}}\,({\rm{translate-def-body}}\,({\rm{assoc}}\,({\it{subr\/}}, {\it{proc-list\/}}), {\it{proc-list\/}})\index{translate-def-body})\index{code} \\ 
$=$$\;\;\;\;${\rm{append}}\,(\=\+{\rm{code}}\,({\rm{translate}}\,({\it{cinfo\/}}, {\it{t-cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}})\index{translate})\index{code}, \\ 
{\it{code2\/}})\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{user-defined-procp}}\,({\it{subr\/}}, {\it{proc-list\/}})\index{user-defined-procp} \\ 
$\wedge$$\;\;\;\;${\rm{plistp}}\,({\it{temp-stk\/}})\index{plistp} \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\it{ctrl-stk\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,(\=\+{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, \\ 
{\it{temp-stk\/}})\-\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, {\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match} \\ 
$\wedge$$\;\;\;\;${\rm{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resource-errorp}}\,({\rm{mg-meaning-r}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{resource-errorp}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,(\=\+{\rm{mg-alist}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{def-body}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-body}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{mg-state}}\,(\=\+{\rm{cc}}\,({\it{mg-state\/}})\index{cc}, \\ 
{\rm{make-call-var-alist}}\,(\=\+{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, \\ 
{\it{stmt\/}}, \\ 
{\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\-\index{make-call-var-alist}, \\ 
{\rm{mg-psw}}\,({\it{mg-state\/}})\index{mg-psw})\-\index{mg-state}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\rm{list}}\,(\=\+\=\+{\rm{data-length}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{data-length} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\it{temp-stk\/}})\index{length}\-, \\ 
\=\+{\tt{2}} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{length} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\rm{def-formals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-formals})\index{length} \\ 
$+$$\;\;\;\;${\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size}\-)\-)\-\index{mg-meaning-r})\index{mg-alist}, \\ 
{\rm{append}}\,(\=\+{\rm{map-call-locals}}\,(\=\+{\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals}, \\ 
{\rm{length}}\,({\it{temp-stk\/}})\index{length})\-\index{map-call-locals}, \\ 
{\rm{map-call-formals}}\,(\=\+{\rm{def-formals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-formals}, \\ 
{\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{map-call-formals})\-, \\ 
{\rm{append}}\,(\=\+{\rm{reverse}}\,({\rm{mg-to-p-local-values}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{mg-to-p-local-values})\index{reverse}, \\ 
{\rm{map-down-values}}\,(\=\+{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, \\ 
{\it{temp-stk\/}})\-\index{map-down-values})\-)\-\index{mg-vars-list-ok-in-p-state}\-
\end{tabbing}

\begin{verbatim};; (pop* (data-length locals))

\end{verbatim}%\item 
\begin{verbatim}


;; (pop* (data-length locals))

(prove-lemma call-state2-step2-effect (rewrite)
      (IMPLIES
       (AND (NOT (ZEROP N))
	    (NOT (RESOURCES-INADEQUATEP STMT PROC-LIST
					(LIST (LENGTH TEMP-STK)
					      (P-CTRL-STK-SIZE CTRL-STK))))
	    (EQUAL (CAR STMT) 'PROC-CALL-MG)
	    (OK-MG-STATEMENT STMT R-COND-LIST NAME-ALIST PROC-LIST)
	    (OK-MG-DEF-PLISTP PROC-LIST)
	    (OK-TRANSLATION-PARAMETERS CINFO T-COND-LIST STMT PROC-LIST CODE2)
	    (OK-MG-STATEP MG-STATE R-COND-LIST)
	    (COND-SUBSETP R-COND-LIST T-COND-LIST)
	    (EQUAL (CODE (TRANSLATE-DEF-BODY (ASSOC SUBR PROC-LIST)
					     PROC-LIST))
		   (APPEND (CODE (TRANSLATE CINFO T-COND-LIST STMT PROC-LIST))
			   CODE2))
	    (USER-DEFINED-PROCP SUBR PROC-LIST)
	    (PLISTP TEMP-STK)
	    (LISTP CTRL-STK)
	    (MG-VARS-LIST-OK-IN-P-STATE (MG-ALIST MG-STATE)
					(BINDINGS (TOP CTRL-STK))
					TEMP-STK)
	    (NO-P-ALIASING (BINDINGS (TOP CTRL-STK))
			   (MG-ALIST MG-STATE))
	    (SIGNATURES-MATCH (MG-ALIST MG-STATE)
			      NAME-ALIST)
	    (NORMAL MG-STATE)
	    (ALL-CARS-UNIQUE (MG-ALIST MG-STATE))
	    (NOT (RESOURCE-ERRORP (MG-MEANING-R STMT PROC-LIST MG-STATE N
						(LIST (LENGTH TEMP-STK)
						      (P-CTRL-STK-SIZE CTRL-STK))))))
     (equal 
       (p-step
	 (P-STATE (TAG 'PC
		     (CONS
		      (CALL-NAME STMT)
		      (PLUS
		       (LENGTH
			(CODE
			 (TRANSLATE
			  (MAKE-CINFO NIL
				      (CONS
				       '(ROUTINEERROR . 0)
				       (MAKE-LABEL-ALIST (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))
							 0))
				      1)
			  (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))
			  (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
			  PROC-LIST)))
		       1)))
		(CONS
		 (P-FRAME
		  (APPEND (MAP-CALL-LOCALS (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))
					   (LENGTH TEMP-STK))
			  (MAP-CALL-FORMALS (DEF-FORMALS (FETCH-CALLED-DEF STMT PROC-LIST))
					    (CALL-ACTUALS STMT)
					    (BINDINGS (TOP CTRL-STK))))
		  (TAG 'PC
		       (CONS SUBR
			     (ADD1 (PLUS (LENGTH (CODE CINFO))
					 (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
					 (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
					 (LENGTH (CALL-ACTUALS STMT)))))))
		 CTRL-STK)
		(MAP-DOWN-VALUES
		 (MG-ALIST
		  (MG-MEANING-R
		   (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
		   PROC-LIST
		   (MG-STATE (CC MG-STATE)
			     (MAKE-CALL-VAR-ALIST (MG-ALIST MG-STATE)
						  STMT
						  (FETCH-CALLED-DEF STMT PROC-LIST))
			     (MG-PSW MG-STATE))
		   (SUB1 N)
		   (LIST (PLUS (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
			       (LENGTH TEMP-STK))
			 (PLUS 2
			       (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
			       (LENGTH (DEF-FORMALS (FETCH-CALLED-DEF STMT PROC-LIST)))
			       (P-CTRL-STK-SIZE CTRL-STK)))))
		 (APPEND (MAP-CALL-LOCALS (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))
					  (LENGTH TEMP-STK))
			 (MAP-CALL-FORMALS (DEF-FORMALS (FETCH-CALLED-DEF STMT PROC-LIST))
					   (CALL-ACTUALS STMT)
					   (BINDINGS (TOP CTRL-STK))))
		 (APPEND
		  (REVERSE
		   (MG-TO-P-LOCAL-VALUES (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))))
		  (MAP-DOWN-VALUES (MG-ALIST MG-STATE)
				   (BINDINGS (TOP CTRL-STK))
				   TEMP-STK)))
		(TRANSLATE-PROC-LIST PROC-LIST)
		(LIST
		 (LIST 'C-C
		       (MG-COND-TO-P-NAT
			(CC
			 (MG-MEANING-R
			  (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
			  PROC-LIST
			  (MG-STATE (CC MG-STATE)
				    (MAKE-CALL-VAR-ALIST (MG-ALIST MG-STATE)
							 STMT
							 (FETCH-CALLED-DEF STMT PROC-LIST))
				    (MG-PSW MG-STATE))
			  (SUB1 N)
			  (LIST
			   (PLUS
			    (LENGTH
			     (MG-TO-P-LOCAL-VALUES
			      (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))))
			    (LENGTH (MAP-DOWN-VALUES (MG-ALIST MG-STATE)
						     (BINDINGS (TOP CTRL-STK))
						     TEMP-STK)))
			   (P-CTRL-STK-SIZE
			    (CONS
			     (P-FRAME
			      (APPEND
			       (MAP-CALL-LOCALS (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))
						(LENGTH TEMP-STK))
			       (MAP-CALL-FORMALS (DEF-FORMALS (FETCH-CALLED-DEF STMT PROC-LIST))
						 (CALL-ACTUALS STMT)
						 (BINDINGS (TOP CTRL-STK))))
			      (TAG 'PC
				   (CONS SUBR
					 (ADD1
					  (PLUS
					   (LENGTH (CODE CINFO))
					   (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
					   (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
					   (LENGTH (CALL-ACTUALS STMT)))))))
			     CTRL-STK)))))
			(MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST)))))
		(MG-MAX-CTRL-STK-SIZE) (MG-MAX-TEMP-STK-SIZE) (MG-WORD-SIZE)
		'RUN))
        (P-STATE
	 (TAG 'PC
	      (CONS
	       (CALL-NAME STMT)
	       (PLUS
		(LENGTH
		 (CODE
		  (TRANSLATE
		   (MAKE-CINFO NIL
			       (CONS
				'(ROUTINEERROR . 0)
				(MAKE-LABEL-ALIST (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))
						  0))
			       1)
		   (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))
		   (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
		   PROC-LIST)))
		2)))
	 (CONS
	  (P-FRAME
	   (APPEND (MAP-CALL-LOCALS (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))
				    (LENGTH TEMP-STK))
		   (MAP-CALL-FORMALS (DEF-FORMALS (FETCH-CALLED-DEF STMT PROC-LIST))
				     (CALL-ACTUALS STMT)
				     (BINDINGS (TOP CTRL-STK))))
	   (TAG 'PC
		(CONS SUBR
		      (ADD1 (PLUS (LENGTH (CODE CINFO))
				  (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
				  (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
				  (LENGTH (CALL-ACTUALS STMT)))))))
	  CTRL-STK)
	 (POPN (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
	  (MAP-DOWN-VALUES
	   (MG-ALIST
	    (MG-MEANING-R
	     (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
	     PROC-LIST
	     (MG-STATE (CC MG-STATE)
		       (MAKE-CALL-VAR-ALIST (MG-ALIST MG-STATE)
					    STMT
					    (FETCH-CALLED-DEF STMT PROC-LIST))
		       (MG-PSW MG-STATE))
	     (SUB1 N)
	     (LIST (PLUS (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
			 (LENGTH TEMP-STK))
		   (PLUS 2
			 (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
			 (LENGTH (DEF-FORMALS (FETCH-CALLED-DEF STMT PROC-LIST)))
			 (P-CTRL-STK-SIZE CTRL-STK)))))
	   (APPEND (MAP-CALL-LOCALS (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))
				    (LENGTH TEMP-STK))
		   (MAP-CALL-FORMALS (DEF-FORMALS (FETCH-CALLED-DEF STMT PROC-LIST))
				     (CALL-ACTUALS STMT)
				     (BINDINGS (TOP CTRL-STK))))
	   (APPEND
	    (REVERSE
	     (MG-TO-P-LOCAL-VALUES (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))))
	    (MAP-DOWN-VALUES (MG-ALIST MG-STATE)
			     (BINDINGS (TOP CTRL-STK))
			     TEMP-STK))))
	 (TRANSLATE-PROC-LIST PROC-LIST)
	 (LIST
	  (LIST 'C-C
		(MG-COND-TO-P-NAT
		 (CC
		  (MG-MEANING-R
		   (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
		   PROC-LIST
		   (MG-STATE (CC MG-STATE)
			     (MAKE-CALL-VAR-ALIST (MG-ALIST MG-STATE)
						  STMT
						  (FETCH-CALLED-DEF STMT PROC-LIST))
			     (MG-PSW MG-STATE))
		   (SUB1 N)
		   (LIST
		    (PLUS
		     (LENGTH
		      (MG-TO-P-LOCAL-VALUES (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))))
		     (LENGTH (MAP-DOWN-VALUES (MG-ALIST MG-STATE)
					      (BINDINGS (TOP CTRL-STK))
					      TEMP-STK)))
		    (P-CTRL-STK-SIZE
		     (CONS
		      (P-FRAME
		       (APPEND
			(MAP-CALL-LOCALS (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))
					 (LENGTH TEMP-STK))
			(MAP-CALL-FORMALS (DEF-FORMALS (FETCH-CALLED-DEF STMT PROC-LIST))
					  (CALL-ACTUALS STMT)
					  (BINDINGS (TOP CTRL-STK))))
		       (TAG 'PC
			    (CONS SUBR
				  (ADD1
				   (PLUS (LENGTH (CODE CINFO))
					 (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
					 (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
					 (LENGTH (CALL-ACTUALS STMT)))))))
		      CTRL-STK)))))
		 (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST)))))
         (MG-MAX-CTRL-STK-SIZE) (MG-MAX-TEMP-STK-SIZE) (MG-WORD-SIZE)
	 'RUN)))
 ((INSTRUCTIONS PROMOTE
   (DIVE 1)
   X
   (S LEMMAS)
   (DIVE 1 1 2)
   (REWRITE TRANSLATE-DEF-BODY-REWRITE
    (($CINFO
      (MAKE-CINFO NIL
       (CONS
           (CONS 'ROUTINEERROR 0)
           (MAKE-LABEL-ALIST (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))
                             0))
       1))
     ($T-COND-LIST (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST)))
     ($CODE2
      (LIST '(DL 0 NIL (NO-OP))
            (LIST 'POP*
                  (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))))
            '(RET)))
     ($STMT (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST)))))
   UP
   (REWRITE GET-LENGTH-PLUS)
   (S LEMMAS)
   UP X UP X
   (S LEMMAS)
   (DIVE 1)
   X UP S
   (S LEMMAS)
   UP S-PROP
   (DIVE 1)
   (DIVE 1)
   (REWRITE MAP-DOWN-VALUES-PRESERVES-LENGTH)
   (S LEMMAS)
   (DIVE 1)
   (REWRITE LENGTH-MG-TO-P-LOCAL-VALUES)
   UP UP
   (= * F)
   UP S
   (REWRITE CALLED-DEF-FORMALS-OK)
   (REWRITE CALL-BODY-MG-VARS-LIST-OK1)
   (DIVE 1 1)
   (REWRITE MG-MEANING-EQUIVALENCE)
   UP UP
   (REWRITE MG-MEANING-PRESERVES-MG-ALISTP
           (($R-COND-LIST (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST)))
            ($NAME-ALIST (MAKE-NAME-ALIST (FETCH-CALLED-DEF STMT PROC-LIST)))))
   (DIVE 1)
   (= *
      (MAKE-CALL-ENVIRONMENT MG-STATE STMT
                             (FETCH-CALLED-DEF STMT PROC-LIST))
      0)
   UP
   (REWRITE PROC-CALL-EXACT-TIME-HYPS)
   S PROVE
   (REWRITE CALL-EXACT-TIME-HYPS1)
   (DIVE 1)
   S UP
   (REWRITE CALL-SIGNATURES-MATCH2)
   (DIVE 1)
   (REWRITE MORE-RESOURCES-PRESERVES-NOT-RESOURCE-ERRORP
    (($T-SIZE1
      (LENGTH
       (APPEND
        (REVERSE
         (MG-TO-P-LOCAL-VALUES (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))))
        (MAP-DOWN-VALUES (MG-ALIST MG-STATE)
                         (BINDINGS (TOP CTRL-STK))
                         TEMP-STK))))
     ($C-SIZE1
      (P-CTRL-STK-SIZE
       (CONS
        (P-FRAME
         (MAKE-FRAME-ALIST (FETCH-CALLED-DEF STMT PROC-LIST)
                           STMT CTRL-STK TEMP-STK)
         (TAG 'PC
          (CONS SUBR
           (ADD1
             (PLUS (LENGTH (CODE CINFO))
                   (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
                   (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
                   (LENGTH (CALL-ACTUALS STMT)))))))
        CTRL-STK)))))
   UP S
   (S LEMMAS)
   (DIVE 1 1 1)
   (REWRITE LENGTH-MG-TO-P-LOCAL-VALUES)
   NX
   (REWRITE MAP-DOWN-VALUES-PRESERVES-LENGTH)
   TOP DROP PROVE
   (REWRITE OK-MG-STATEP-MG-ALIST-MG-ALISTP)
   (REWRITE CALLED-DEF-FORMALS-OK)
   (DIVE 1 1)
   X
   (S LEMMAS)
   (S-PROP P-FRAME-SIZE)
   (S LEMMAS)
   UP TOP DROP PROVE
   (DIVE 1 1 3)
   (= *
      (MAKE-CALL-ENVIRONMENT MG-STATE STMT
                             (FETCH-CALLED-DEF STMT PROC-LIST))
      0)
   TOP
   (DIVE 1)
   (REWRITE PROC-CALL-DOESNT-HALT)
   TOP S
   (S-PROP MAKE-CALL-ENVIRONMENT)
   (PROVE (ENABLE OK-MG-STATEMENT OK-PROC-CALL))
   (REWRITE PROC-CALL-EXACT-TIME-HYPS)
   (DIVE 1 1)
   X TOP
   (PROVE (ENABLE FETCH-CALLED-DEF FETCH-DEF)))))
\end{verbatim}


\begin{verbatim};; (ret)

\end{verbatim}%\item 
\begin{verbatim}


;; (ret)

(prove-lemma call-state2-step3-effect (rewrite)
      (IMPLIES
       (AND (NOT (ZEROP N))
	    (NOT (RESOURCES-INADEQUATEP STMT PROC-LIST
					(LIST (LENGTH TEMP-STK)
					      (P-CTRL-STK-SIZE CTRL-STK))))
	    (EQUAL (CAR STMT) 'PROC-CALL-MG)
	    (OK-MG-STATEMENT STMT R-COND-LIST NAME-ALIST PROC-LIST)
	    (OK-MG-DEF-PLISTP PROC-LIST)
	    (OK-TRANSLATION-PARAMETERS CINFO T-COND-LIST STMT PROC-LIST CODE2)
	    (OK-MG-STATEP MG-STATE R-COND-LIST)
	    (COND-SUBSETP R-COND-LIST T-COND-LIST)
	    (EQUAL (CODE (TRANSLATE-DEF-BODY (ASSOC SUBR PROC-LIST)
					     PROC-LIST))
		   (APPEND (CODE (TRANSLATE CINFO T-COND-LIST STMT PROC-LIST))
			   CODE2))
	    (USER-DEFINED-PROCP SUBR PROC-LIST)
	    (PLISTP TEMP-STK)
	    (LISTP CTRL-STK)
	    (MG-VARS-LIST-OK-IN-P-STATE (MG-ALIST MG-STATE)
					(BINDINGS (TOP CTRL-STK))
					TEMP-STK)
	    (NO-P-ALIASING (BINDINGS (TOP CTRL-STK))
			   (MG-ALIST MG-STATE))
	    (SIGNATURES-MATCH (MG-ALIST MG-STATE)
			      NAME-ALIST)
	    (NORMAL MG-STATE)
	    (ALL-CARS-UNIQUE (MG-ALIST MG-STATE))
	    (NOT (RESOURCE-ERRORP (MG-MEANING-R STMT PROC-LIST MG-STATE N
						(LIST (LENGTH TEMP-STK)
						      (P-CTRL-STK-SIZE CTRL-STK))))))
     (equal 
       (p-step
        (P-STATE
	 (TAG 'PC
	      (CONS
	       (CALL-NAME STMT)
	       (PLUS
		(LENGTH
		 (CODE
		  (TRANSLATE
		   (MAKE-CINFO NIL
			       (CONS
				'(ROUTINEERROR . 0)
				(MAKE-LABEL-ALIST (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))
						  0))
			       1)
		   (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))
		   (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
		   PROC-LIST)))
		2)))
	 (CONS
	  (P-FRAME
	   (APPEND (MAP-CALL-LOCALS (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))
				    (LENGTH TEMP-STK))
		   (MAP-CALL-FORMALS (DEF-FORMALS (FETCH-CALLED-DEF STMT PROC-LIST))
				     (CALL-ACTUALS STMT)
				     (BINDINGS (TOP CTRL-STK))))
	   (TAG 'PC
		(CONS SUBR
		      (ADD1 (PLUS (LENGTH (CODE CINFO))
				  (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
				  (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
				  (LENGTH (CALL-ACTUALS STMT)))))))
	  CTRL-STK)
	 (POPN (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
	  (MAP-DOWN-VALUES
	   (MG-ALIST
	    (MG-MEANING-R
	     (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
	     PROC-LIST
	     (MG-STATE (CC MG-STATE)
		       (MAKE-CALL-VAR-ALIST (MG-ALIST MG-STATE)
					    STMT
					    (FETCH-CALLED-DEF STMT PROC-LIST))
		       (MG-PSW MG-STATE))
	     (SUB1 N)
	     (LIST (PLUS (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
			 (LENGTH TEMP-STK))
		   (PLUS 2
			 (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
			 (LENGTH (DEF-FORMALS (FETCH-CALLED-DEF STMT PROC-LIST)))
			 (P-CTRL-STK-SIZE CTRL-STK)))))
	   (APPEND (MAP-CALL-LOCALS (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))
				    (LENGTH TEMP-STK))
		   (MAP-CALL-FORMALS (DEF-FORMALS (FETCH-CALLED-DEF STMT PROC-LIST))
				     (CALL-ACTUALS STMT)
				     (BINDINGS (TOP CTRL-STK))))
	   (APPEND
	    (REVERSE
	     (MG-TO-P-LOCAL-VALUES (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))))
	    (MAP-DOWN-VALUES (MG-ALIST MG-STATE)
			     (BINDINGS (TOP CTRL-STK))
			     TEMP-STK))))
	 (TRANSLATE-PROC-LIST PROC-LIST)
	 (LIST
	  (LIST 'C-C
		(MG-COND-TO-P-NAT
		 (CC
		  (MG-MEANING-R
		   (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
		   PROC-LIST
		   (MG-STATE (CC MG-STATE)
			     (MAKE-CALL-VAR-ALIST (MG-ALIST MG-STATE)
						  STMT
						  (FETCH-CALLED-DEF STMT PROC-LIST))
			     (MG-PSW MG-STATE))
		   (SUB1 N)
		   (LIST
		    (PLUS
		     (LENGTH
		      (MG-TO-P-LOCAL-VALUES (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))))
		     (LENGTH (MAP-DOWN-VALUES (MG-ALIST MG-STATE)
					      (BINDINGS (TOP CTRL-STK))
					      TEMP-STK)))
		    (P-CTRL-STK-SIZE
		     (CONS
		      (P-FRAME
		       (APPEND
			(MAP-CALL-LOCALS (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))
					 (LENGTH TEMP-STK))
			(MAP-CALL-FORMALS (DEF-FORMALS (FETCH-CALLED-DEF STMT PROC-LIST))
					  (CALL-ACTUALS STMT)
					  (BINDINGS (TOP CTRL-STK))))
		       (TAG 'PC
			    (CONS SUBR
				  (ADD1
				   (PLUS (LENGTH (CODE CINFO))
					 (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
					 (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
					 (LENGTH (CALL-ACTUALS STMT)))))))
		      CTRL-STK)))))
		 (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST)))))
	 (MG-MAX-CTRL-STK-SIZE) (MG-MAX-TEMP-STK-SIZE) (MG-WORD-SIZE)
	 'RUN))
      (P-STATE
          (TAG 'PC
	       (CONS SUBR
		     (ADD1 (PLUS (LENGTH (CODE CINFO))
				 (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
				 (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
				 (LENGTH (CALL-ACTUALS STMT))))))
         ctrl-stk
	 (POPN (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
	  (MAP-DOWN-VALUES
	   (MG-ALIST
	    (MG-MEANING-R
	     (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
	     PROC-LIST
	     (MG-STATE (CC MG-STATE)
		       (MAKE-CALL-VAR-ALIST (MG-ALIST MG-STATE)
					    STMT
					    (FETCH-CALLED-DEF STMT PROC-LIST))
		       (MG-PSW MG-STATE))
	     (SUB1 N)
	     (LIST (PLUS (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
			 (LENGTH TEMP-STK))
		   (PLUS 2
			 (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
			 (LENGTH (DEF-FORMALS (FETCH-CALLED-DEF STMT PROC-LIST)))
			 (P-CTRL-STK-SIZE CTRL-STK)))))
	   (APPEND (MAP-CALL-LOCALS (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))
				    (LENGTH TEMP-STK))
		   (MAP-CALL-FORMALS (DEF-FORMALS (FETCH-CALLED-DEF STMT PROC-LIST))
				     (CALL-ACTUALS STMT)
				     (BINDINGS (TOP CTRL-STK))))
	   (APPEND
	    (REVERSE
	     (MG-TO-P-LOCAL-VALUES (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))))
	    (MAP-DOWN-VALUES (MG-ALIST MG-STATE)
			     (BINDINGS (TOP CTRL-STK))
			     TEMP-STK))))
	 (TRANSLATE-PROC-LIST PROC-LIST)
	 (LIST
	  (LIST 'C-C
		(MG-COND-TO-P-NAT
		 (CC
		  (MG-MEANING-R
		   (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST))
		   PROC-LIST
		   (MG-STATE (CC MG-STATE)
			     (MAKE-CALL-VAR-ALIST (MG-ALIST MG-STATE)
						  STMT
						  (FETCH-CALLED-DEF STMT PROC-LIST))
			     (MG-PSW MG-STATE))
		   (SUB1 N)
		   (LIST
		    (PLUS
		     (LENGTH
		      (MG-TO-P-LOCAL-VALUES (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))))
		     (LENGTH (MAP-DOWN-VALUES (MG-ALIST MG-STATE)
					      (BINDINGS (TOP CTRL-STK))
					      TEMP-STK)))
		    (P-CTRL-STK-SIZE
		     (CONS
		      (P-FRAME
		       (APPEND
			(MAP-CALL-LOCALS (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))
					 (LENGTH TEMP-STK))
			(MAP-CALL-FORMALS (DEF-FORMALS (FETCH-CALLED-DEF STMT PROC-LIST))
					  (CALL-ACTUALS STMT)
					  (BINDINGS (TOP CTRL-STK))))
		       (TAG 'PC
			    (CONS SUBR
				  (ADD1
				   (PLUS (LENGTH (CODE CINFO))
					 (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
					 (LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST)))
					 (LENGTH (CALL-ACTUALS STMT)))))))
		      CTRL-STK)))))
		 (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST)))))
	 (MG-MAX-CTRL-STK-SIZE) (MG-MAX-TEMP-STK-SIZE) (MG-WORD-SIZE)
	 'RUN)))
 ((INSTRUCTIONS PROMOTE
   (DIVE 1)
   X
   (S LEMMAS)
   (DIVE 1 1 2)
   (REWRITE TRANSLATE-DEF-BODY-REWRITE
    (($CINFO
      (MAKE-CINFO NIL
       (CONS
           (CONS 'ROUTINEERROR 0)
           (MAKE-LABEL-ALIST (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST))
                             0))
       1))
     ($T-COND-LIST (MAKE-COND-LIST (FETCH-CALLED-DEF STMT PROC-LIST)))
     ($CODE2
      (LIST
       '(DL 0 NIL (NO-OP))
       (LIST 'POP* (DATA-LENGTH (DEF-LOCALS (FETCH-CALLED-DEF STMT PROC-LIST))))
       '(RET)))
     ($STMT (DEF-BODY (FETCH-CALLED-DEF STMT PROC-LIST)))))
   UP
   (REWRITE GET-LENGTH-PLUS)
   (S LEMMAS)
   UP X UP X
   (S LEMMAS)
   X
   (S LEMMAS)
   UP prove
   (PROVE (ENABLE OK-MG-STATEMENT OK-PROC-CALL))
   (DIVE 1 1)
   X TOP
   (PROVE (ENABLE FETCH-CALLED-DEF FETCH-DEF)))))
\end{verbatim}




\noindent{\sc Event}:   Make the library {\tt{"c-proc-call1"}}.

\addvspace{18pt}

%\end{list}
\printindex
\end{document}
te-proc-list}, \\ 
{\rm{list}}\,({\rm{list}}\,(\=\+{\tt{'}}{\tt{c-c}}, \\ 
{\rm{mg-cond-to-p-nat}}\,(\=\+{\rm{cc}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{def-body}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-body}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{mg-state}}\,(\=\+{\rm{cc}}\,({\it{mg-state\/}})\index{cc}, \\ 
{\rm{make-call-var-alist}}\,(\=\+{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, \\ 
{\it{stmt\/}}, \\ 
{\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\-\index{make-call-var-alist}, \\ 
{\rm{mg-psw}}\,({\it{mg-state\/}})\index{mg-psw})\-\index{mg-state}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\rm{list}}\,(\=\+\=\+{\rm{length}}\,({\rm{mg-to-p-local-values}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{mg-to-p-local-values})\index{length} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\rm{map-down-values}}\,(\=\+{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, \\ 
{\it{temp-stk\/}})\-\index{map-down-values})\index{length}\-, \\ 
{\rm{p-ctrl-stk-size}}\,({\rm{cons}}\,(\=\+{\rm{p-frame}}\,(\=\+{\rm{append}}\,(\=\+{\rm{map-call-locals}}\,(\=\+{\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals}, \\ 
{\rm{length}}\,({\it{temp-stk\/}})\index{length})\-\index{map-call-locals}, \\ 
{\rm{map-call-formals}}\,(\=\+{\rm{def-formals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-formals}, \\ 
{\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{map-call-formals})\-, \\ 
{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,(\=\+{\it{subr\/}}, \\ 
$1\;+$ (\=\+{\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} \\ 
$+$$\;\;\;\;${\rm{data-length}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(