\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-predefined1"}}.

\addvspace{18pt}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                           ;;
;;                    EXACT-TIME LEMMA MG-INTEGER-LE                         ;;
;;                                                                           ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

\end{verbatim}\begin{tabbing}{\sc Theorem}:  mg-integer-le-args-have-simple-mg-type-refps \\ \index{mg-integer-le-args-have-simple-!mg-type-refps}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{predefined-proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;$({\rm{call-name}}\,({\it{stmt\/}})\index{call-name} $=$ {\tt{'}}{\tt{mg-integer-le}}) \\ 
$\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{boolean-identifierp}}\,({\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), {\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{boolean-identifierp} \\ 
$\wedge$$\;\;\;\;${\rm{int-identifierp}}\,({\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), {\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{int-identifierp} \\ 
$\wedge$$\;\;\;\;${\rm{int-identifierp}}\,({\rm{caddr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), {\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{int-identifierp})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mg-integer-le-args-definedp \\ \index{mg-integer-le-args-definedp}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{predefined-proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;$({\rm{call-name}}\,({\it{stmt\/}})\index{call-name} $=$ {\tt{'}}{\tt{mg-integer-le}}) \\ 
$\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{definedp}}\,({\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), {\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{definedp} \\ 
$\wedge$$\;\;\;\;${\rm{definedp}}\,({\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), {\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{definedp} \\ 
$\wedge$$\;\;\;\;${\rm{definedp}}\,({\rm{caddr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), {\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{definedp})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mg-integer-le-steps-1-3 \\ \index{mg-integer-le-steps-1-3}
\=\+(\=\+({\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{predefined-proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;$({\rm{call-name}}\,({\it{stmt\/}})\index{call-name} $=$ {\tt{'}}{\tt{mg-integer-le}}) \\ 
$\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{listp}}\,({\it{ctrl-stk\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match} \\ 
$\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{normal}}\,({\it{mg-state\/}})\index{normal})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{p-step}}\,({\rm{p-step}}\,({\rm{p-step}}\,({\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})\index{p-step})\index{p-step})\index{p-step} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{pc}}, {\rm{cons}}\,({\it{subr\/}}, {\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} $+$ {\tt{3}}))\index{tag}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\rm{push}}\,(\=\+{\rm{value}}\,(\=\+{\rm{caddr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value}, \\ 
{\rm{push}}\,(\=\+{\rm{value}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value}, \\ 
{\rm{push}}\,(\=\+{\rm{value}}\,(\=\+{\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value}, \\ 
{\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{push})\-\index{push})\-\index{push}, \\ 
{\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}:  mg-integer-le-step-4 \\ \index{mg-integer-le-step-4}
\=\+(\=\+({\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{predefined-proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;$({\rm{call-name}}\,({\it{stmt\/}})\index{call-name} $=$ {\tt{'}}{\tt{mg-integer-le}}) \\ 
$\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{listp}}\,({\it{ctrl-stk\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match} \\ 
$\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{normal}}\,({\it{mg-state\/}})\index{normal})\- \\ 
$\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} $+$ {\tt{3}}))\index{tag}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\rm{push}}\,(\=\+{\rm{value}}\,(\=\+{\rm{caddr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value}, \\ 
{\rm{push}}\,(\=\+{\rm{value}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value}, \\ 
{\rm{push}}\,(\=\+{\rm{value}}\,(\=\+{\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value}, \\ 
{\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{push})\-\index{push})\-\index{push}, \\ 
{\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}}, {\tt{'}}{\tt{(}}{\tt{mg-integer-le}}{\tt{ .\ }}{\tt{0}}{\tt{)}})\index{tag}, \\ 
{\rm{push}}\,(\=\+{\rm{p-frame}}\,(\=\+{\rm{list}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{ans}}, \\ 
{\rm{value}}\,(\=\+{\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{x}}, \\ 
{\rm{value}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{y}}, \\ 
{\rm{value}}\,(\=\+{\rm{caddr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-)\-, \\ 
{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,({\it{subr\/}}, \=\+{\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} \\ 
$+$$\;\;\;\;${\tt{4}}\-))\-\index{tag})\-\index{p-frame}, \\ 
{\it{ctrl-stk\/}})\-\index{push}, \\ 
{\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}:  mg-integer-le-step-5 \\ \index{mg-integer-le-step-5}
\=\+(\=\+({\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{predefined-proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;$({\rm{call-name}}\,({\it{stmt\/}})\index{call-name} $=$ {\tt{'}}{\tt{mg-integer-le}}) \\ 
$\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{listp}}\,({\it{ctrl-stk\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match} \\ 
$\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{normal}}\,({\it{mg-state\/}})\index{normal})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{p-step}}\,({\rm{p-state}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{pc}}, {\tt{'}}{\tt{(}}{\tt{mg-integer-le}}{\tt{ .\ }}{\tt{0}}{\tt{)}})\index{tag}, \\ 
{\rm{push}}\,(\=\+{\rm{p-frame}}\,(\=\+{\rm{list}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{ans}}, \\ 
{\rm{value}}\,(\=\+{\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{x}}, \\ 
{\rm{value}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{y}}, \\ 
{\rm{value}}\,(\=\+{\rm{caddr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-)\-, \\ 
{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,({\it{subr\/}}, \=\+{\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} \\ 
$+$$\;\;\;\;${\tt{4}}\-))\-\index{tag})\-\index{p-frame}, \\ 
{\it{ctrl-stk\/}})\-\index{push}, \\ 
{\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}}, {\tt{'}}{\tt{(}}{\tt{mg-integer-le}}{\tt{ .\ }}{\tt{1}}{\tt{)}})\index{tag}, \\ 
{\rm{push}}\,(\=\+{\rm{p-frame}}\,(\=\+{\rm{list}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{ans}}, \\ 
{\rm{value}}\,(\=\+{\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{x}}, \\ 
{\rm{value}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{y}}, \\ 
{\rm{value}}\,(\=\+{\rm{caddr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-)\-, \\ 
{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,({\it{subr\/}}, \=\+{\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} \\ 
$+$$\;\;\;\;${\tt{4}}\-))\-\index{tag})\-\index{p-frame}, \\ 
{\it{ctrl-stk\/}})\-\index{push}, \\ 
{\rm{push}}\,(\=\+{\rm{value}}\,(\=\+{\rm{caddr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value}, \\ 
{\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{push}, \\ 
{\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}:  mg-integer-le-step-6 \\ \index{mg-integer-le-step-6}
\=\+(\=\+({\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{predefined-proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;$({\rm{call-name}}\,({\it{stmt\/}})\index{call-name} $=$ {\tt{'}}{\tt{mg-integer-le}}) \\ 
$\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{listp}}\,({\it{ctrl-stk\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match} \\ 
$\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{normal}}\,({\it{mg-state\/}})\index{normal})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{p-step}}\,({\rm{p-state}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{pc}}, {\tt{'}}{\tt{(}}{\tt{mg-integer-le}}{\tt{ .\ }}{\tt{1}}{\tt{)}})\index{tag}, \\ 
{\rm{push}}\,(\=\+{\rm{p-frame}}\,(\=\+{\rm{list}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{ans}}, \\ 
{\rm{value}}\,(\=\+{\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{x}}, \\ 
{\rm{value}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{y}}, \\ 
{\rm{value}}\,(\=\+{\rm{caddr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-)\-, \\ 
{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,({\it{subr\/}}, \=\+{\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} \\ 
$+$$\;\;\;\;${\tt{4}}\-))\-\index{tag})\-\index{p-frame}, \\ 
{\it{ctrl-stk\/}})\-\index{push}, \\ 
{\rm{push}}\,(\=\+{\rm{value}}\,(\=\+{\rm{caddr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value}, \\ 
{\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{push}, \\ 
{\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}}, {\tt{'}}{\tt{(}}{\tt{mg-integer-le}}{\tt{ .\ }}{\tt{2}}{\tt{)}})\index{tag}, \\ 
{\rm{push}}\,(\=\+{\rm{p-frame}}\,(\=\+{\rm{list}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{ans}}, \\ 
{\rm{value}}\,(\=\+{\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{x}}, \\ 
{\rm{value}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{y}}, \\ 
{\rm{value}}\,(\=\+{\rm{caddr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-)\-, \\ 
{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,({\it{subr\/}}, \=\+{\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} \\ 
$+$$\;\;\;\;${\tt{4}}\-))\-\index{tag})\-\index{p-frame}, \\ 
{\it{ctrl-stk\/}})\-\index{push}, \\ 
{\rm{push}}\,(\=\+{\rm{rget}}\,(\=\+{\rm{untag}}\,({\rm{value}}\,(\=\+{\rm{caddr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\index{untag}, \\ 
{\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{rget}, \\ 
{\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{push}, \\ 
{\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}:  mg-integer-le-step-7 \\ \index{mg-integer-le-step-7}
\=\+(\=\+({\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{predefined-proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;$({\rm{call-name}}\,({\it{stmt\/}})\index{call-name} $=$ {\tt{'}}{\tt{mg-integer-le}}) \\ 
$\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{listp}}\,({\it{ctrl-stk\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match} \\ 
$\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{normal}}\,({\it{mg-state\/}})\index{normal})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{p-step}}\,({\rm{p-state}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{pc}}, {\tt{'}}{\tt{(}}{\tt{mg-integer-le}}{\tt{ .\ }}{\tt{2}}{\tt{)}})\index{tag}, \\ 
{\rm{push}}\,(\=\+{\rm{p-frame}}\,(\=\+{\rm{list}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{ans}}, \\ 
{\rm{value}}\,(\=\+{\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{x}}, \\ 
{\rm{value}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{y}}, \\ 
{\rm{value}}\,(\=\+{\rm{caddr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-)\-, \\ 
{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,({\it{subr\/}}, \=\+{\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} \\ 
$+$$\;\;\;\;${\tt{4}}\-))\-\index{tag})\-\index{p-frame}, \\ 
{\it{ctrl-stk\/}})\-\index{push}, \\ 
{\rm{push}}\,(\=\+{\rm{rget}}\,(\=\+{\rm{untag}}\,({\rm{value}}\,(\=\+{\rm{caddr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\index{untag}, \\ 
{\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{rget}, \\ 
{\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{push}, \\ 
{\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}}, {\tt{'}}{\tt{(}}{\tt{mg-integer-le}}{\tt{ .\ }}{\tt{3}}{\tt{)}})\index{tag}, \\ 
{\rm{push}}\,(\=\+{\rm{p-frame}}\,(\=\+{\rm{list}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{ans}}, \\ 
{\rm{value}}\,(\=\+{\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{x}}, \\ 
{\rm{value}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{y}}, \\ 
{\rm{value}}\,(\=\+{\rm{caddr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-)\-, \\ 
{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,({\it{subr\/}}, \=\+{\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} \\ 
$+$$\;\;\;\;${\tt{4}}\-))\-\index{tag})\-\index{p-frame}, \\ 
{\it{ctrl-stk\/}})\-\index{push}, \\ 
{\rm{push}}\,(\=\+{\rm{value}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value}, \\ 
{\rm{push}}\,(\=\+{\rm{rget}}\,(\=\+{\rm{untag}}\,({\rm{value}}\,(\=\+{\rm{caddr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\index{untag}, \\ 
{\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{rget}, \\ 
{\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{push})\-\index{push}, \\ 
{\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}:  mg-integer-le-step-8 \\ \index{mg-integer-le-step-8}
\=\+(\=\+({\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{predefined-proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;$({\rm{call-name}}\,({\it{stmt\/}})\index{call-name} $=$ {\tt{'}}{\tt{mg-integer-le}}) \\ 
$\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{listp}}\,({\it{ctrl-stk\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match} \\ 
$\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{normal}}\,({\it{mg-state\/}})\index{normal})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{p-step}}\,({\rm{p-state}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{pc}}, {\tt{'}}{\tt{(}}{\tt{mg-integer-le}}{\tt{ .\ }}{\tt{3}}{\tt{)}})\index{tag}, \\ 
{\rm{push}}\,(\=\+{\rm{p-frame}}\,(\=\+{\rm{list}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{ans}}, \\ 
{\rm{value}}\,(\=\+{\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{x}}, \\ 
{\rm{value}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{y}}, \\ 
{\rm{value}}\,(\=\+{\rm{caddr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-)\-, \\ 
{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,({\it{subr\/}}, \=\+{\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} \\ 
$+$$\;\;\;\;${\tt{4}}\-))\-\index{tag})\-\index{p-frame}, \\ 
{\it{ctrl-stk\/}})\-\index{push}, \\ 
{\rm{push}}\,(\=\+{\rm{value}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value}, \\ 
{\rm{push}}\,(\=\+{\rm{rget}}\,(\=\+{\rm{untag}}\,({\rm{value}}\,(\=\+{\rm{caddr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\index{untag}, \\ 
{\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{rget}, \\ 
{\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{push})\-\index{push}, \\ 
{\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}}, {\tt{'}}{\tt{(}}{\tt{mg-integer-le}}{\tt{ .\ }}{\tt{4}}{\tt{)}})\index{tag}, \\ 
{\rm{push}}\,(\=\+{\rm{p-frame}}\,(\=\+{\rm{list}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{ans}}, \\ 
{\rm{value}}\,(\=\+{\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{x}}, \\ 
{\rm{value}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{y}}, \\ 
{\rm{value}}\,(\=\+{\rm{caddr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-)\-, \\ 
{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,({\it{subr\/}}, \=\+{\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} \\ 
$+$$\;\;\;\;${\tt{4}}\-))\-\index{tag})\-\index{p-frame}, \\ 
{\it{ctrl-stk\/}})\-\index{push}, \\ 
{\rm{push}}\,(\=\+{\rm{rget}}\,(\=\+{\rm{untag}}\,({\rm{value}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\index{untag}, \\ 
{\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{rget}, \\ 
{\rm{push}}\,(\=\+{\rm{rget}}\,(\=\+{\rm{untag}}\,({\rm{value}}\,(\=\+{\rm{caddr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\index{untag}, \\ 
{\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{rget}, \\ 
{\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{push})\-\index{push}, \\ 
{\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}:  mg-integer-le-step-9 \\ \index{mg-integer-le-step-9}
\=\+(\=\+({\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{predefined-proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;$({\rm{call-name}}\,({\it{stmt\/}})\index{call-name} $=$ {\tt{'}}{\tt{mg-integer-le}}) \\ 
$\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{listp}}\,({\it{ctrl-stk\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match} \\ 
$\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{normal}}\,({\it{mg-state\/}})\index{normal})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{p-step}}\,({\rm{p-state}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{pc}}, {\tt{'}}{\tt{(}}{\tt{mg-integer-le}}{\tt{ .\ }}{\tt{4}}{\tt{)}})\index{tag}, \\ 
{\rm{push}}\,(\=\+{\rm{p-frame}}\,(\=\+{\rm{list}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{ans}}, \\ 
{\rm{value}}\,(\=\+{\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{x}}, \\ 
{\rm{value}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{y}}, \\ 
{\rm{value}}\,(\=\+{\rm{caddr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-)\-, \\ 
{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,({\it{subr\/}}, \=\+{\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} \\ 
$+$$\;\;\;\;${\tt{4}}\-))\-\index{tag})\-\index{p-frame}, \\ 
{\it{ctrl-stk\/}})\-\index{push}, \\ 
{\rm{push}}\,(\=\+{\rm{rget}}\,(\=\+{\rm{untag}}\,({\rm{value}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\index{untag}, \\ 
{\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{rget}, \\ 
{\rm{push}}\,(\=\+{\rm{rget}}\,(\=\+{\rm{untag}}\,({\rm{value}}\,(\=\+{\rm{caddr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\index{untag}, \\ 
{\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{rget}, \\ 
{\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{push})\-\index{push}, \\ 
{\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}}, {\tt{'}}{\tt{(}}{\tt{mg-integer-le}}{\tt{ .\ }}{\tt{5}}{\tt{)}})\index{tag}, \\ 
{\rm{push}}\,(\=\+{\rm{p-frame}}\,(\=\+{\rm{list}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{ans}}, \\ 
{\rm{value}}\,(\=\+{\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{x}}, \\ 
{\rm{value}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{y}}, \\ 
{\rm{value}}\,(\=\+{\rm{caddr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-)\-, \\ 
{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,({\it{subr\/}}, \=\+{\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} \\ 
$+$$\;\;\;\;${\tt{4}}\-))\-\index{tag})\-\index{p-frame}, \\ 
{\it{ctrl-stk\/}})\-\index{push}, \\ 
{\rm{push}}\,(\=\+{\rm{tag}}\,(\=\+{\tt{'}}{\tt{bool}}, \\ 
\=\+{\bf if }{\rm{ilessp}}\,(\=\+{\rm{untag}}\,({\rm{mg-to-p-simple-literal}}\,({\rm{caddr}}\,({\rm{assoc}}\,(\=\+{\rm{caddr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\-))\index{mg-to-p-simple-literal})\index{untag}, \\ 
{\rm{untag}}\,({\rm{mg-to-p-simple-literal}}\,({\rm{caddr}}\,({\rm{assoc}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\-))\index{mg-to-p-simple-literal})\index{untag})\-\index{ilessp} \\ 
{\bf then }{\tt{'}}{\tt{t}} \\ 
{\bf else }{\tt{'}}{\tt{f}}$\;${\bf  endif}\-)\-\index{tag}, \\ 
{\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{push}, \\ 
{\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}:  mg-integer-le-step-10 \\ \index{mg-integer-le-step-10}
\=\+(\=\+({\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{predefined-proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;$({\rm{call-name}}\,({\it{stmt\/}})\index{call-name} $=$ {\tt{'}}{\tt{mg-integer-le}}) \\ 
$\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{listp}}\,({\it{ctrl-stk\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match} \\ 
$\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{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;$({\it{lt-value\/}} $\in$ {\tt{'}}{\tt{(}}{\tt{t}}{\tt{ }}{\tt{f}}{\tt{)}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{p-step}}\,({\rm{p-state}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{pc}}, {\tt{'}}{\tt{(}}{\tt{mg-integer-le}}{\tt{ .\ }}{\tt{5}}{\tt{)}})\index{tag}, \\ 
{\rm{push}}\,(\=\+{\rm{p-frame}}\,(\=\+{\rm{list}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{ans}}, \\ 
{\rm{value}}\,(\=\+{\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{x}}, \\ 
{\rm{value}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{y}}, \\ 
{\rm{value}}\,(\=\+{\rm{caddr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-)\-, \\ 
{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,({\it{subr\/}}, \=\+{\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} \\ 
$+$$\;\;\;\;${\tt{4}}\-))\-\index{tag})\-\index{p-frame}, \\ 
{\it{ctrl-stk\/}})\-\index{push}, \\ 
{\rm{push}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{bool}}, {\it{lt-value\/}})\index{tag}, \\ 
{\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{push}, \\ 
{\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}}, {\tt{'}}{\tt{(}}{\tt{mg-integer-le}}{\tt{ .\ }}{\tt{6}}{\tt{)}})\index{tag}, \\ 
{\rm{push}}\,(\=\+{\rm{p-frame}}\,(\=\+{\rm{list}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{ans}}, \\ 
{\rm{value}}\,(\=\+{\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{x}}, \\ 
{\rm{value}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{y}}, \\ 
{\rm{value}}\,(\=\+{\rm{caddr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-)\-, \\ 
{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,({\it{subr\/}}, \=\+{\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} \\ 
$+$$\;\;\;\;${\tt{4}}\-))\-\index{tag})\-\index{p-frame}, \\ 
{\it{ctrl-stk\/}})\-\index{push}, \\ 
{\rm{push}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{bool}}, {\rm{not-bool}}\,({\it{lt-value\/}})\index{not-bool})\index{tag}, \\ 
{\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{push}, \\ 
{\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}:  mg-integer-le-step-11 \\ \index{mg-integer-le-step-11}
\=\+(\=\+({\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{predefined-proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;$({\rm{call-name}}\,({\it{stmt\/}})\index{call-name} $=$ {\tt{'}}{\tt{mg-integer-le}}) \\ 
$\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{listp}}\,({\it{ctrl-stk\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match} \\ 
$\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{normal}}\,({\it{mg-state\/}})\index{normal})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{p-step}}\,({\rm{p-state}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{pc}}, {\tt{'}}{\tt{(}}{\tt{mg-integer-le}}{\tt{ .\ }}{\tt{6}}{\tt{)}})\index{tag}, \\ 
{\rm{push}}\,(\=\+{\rm{p-frame}}\,(\=\+{\rm{list}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{ans}}, \\ 
{\rm{value}}\,(\=\+{\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{x}}, \\ 
{\rm{value}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{y}}, \\ 
{\rm{value}}\,(\=\+{\rm{caddr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-)\-, \\ 
{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,({\it{subr\/}}, \=\+{\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} \\ 
$+$$\;\;\;\;${\tt{4}}\-))\-\index{tag})\-\index{p-frame}, \\ 
{\it{ctrl-stk\/}})\-\index{push}, \\ 
{\rm{push}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{bool}}, {\rm{not-bool}}\,({\it{lt-value\/}})\index{not-bool})\index{tag}, \\ 
{\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{push}, \\ 
{\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}}, {\tt{'}}{\tt{(}}{\tt{mg-integer-le}}{\tt{ .\ }}{\tt{7}}{\tt{)}})\index{tag}, \\ 
{\rm{push}}\,(\=\+{\rm{p-frame}}\,(\=\+{\rm{list}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{ans}}, \\ 
{\rm{value}}\,(\=\+{\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{x}}, \\ 
{\rm{value}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{y}}, \\ 
{\rm{value}}\,(\=\+{\rm{caddr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-)\-, \\ 
{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,({\it{subr\/}}, \=\+{\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} \\ 
$+$$\;\;\;\;${\tt{4}}\-))\-\index{tag})\-\index{p-frame}, \\ 
{\it{ctrl-stk\/}})\-\index{push}, \\ 
{\rm{push}}\,(\=\+{\rm{value}}\,(\=\+{\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value}, \\ 
{\rm{push}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{bool}}, {\rm{not-bool}}\,({\it{lt-value\/}})\index{not-bool})\index{tag}, \\ 
{\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{push})\-\index{push}, \\ 
{\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}:  mg-integer-le-step-12 \\ \index{mg-integer-le-step-12}
\=\+(\=\+({\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{predefined-proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;$({\rm{call-name}}\,({\it{stmt\/}})\index{call-name} $=$ {\tt{'}}{\tt{mg-integer-le}}) \\ 
$\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{listp}}\,({\it{ctrl-stk\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match} \\ 
$\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{normal}}\,({\it{mg-state\/}})\index{normal})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{p-step}}\,({\rm{p-state}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{pc}}, {\tt{'}}{\tt{(}}{\tt{mg-integer-le}}{\tt{ .\ }}{\tt{7}}{\tt{)}})\index{tag}, \\ 
{\rm{push}}\,(\=\+{\rm{p-frame}}\,(\=\+{\rm{list}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{ans}}, \\ 
{\rm{value}}\,(\=\+{\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{x}}, \\ 
{\rm{value}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{y}}, \\ 
{\rm{value}}\,(\=\+{\rm{caddr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-)\-, \\ 
{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,({\it{subr\/}}, \=\+{\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} \\ 
$+$$\;\;\;\;${\tt{4}}\-))\-\index{tag})\-\index{p-frame}, \\ 
{\it{ctrl-stk\/}})\-\index{push}, \\ 
{\rm{push}}\,(\=\+{\rm{value}}\,(\=\+{\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value}, \\ 
{\rm{push}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{bool}}, {\rm{not-bool}}\,({\it{lt-value\/}})\index{not-bool})\index{tag}, \\ 
{\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{push})\-\index{push}, \\ 
{\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}}, {\tt{'}}{\tt{(}}{\tt{mg-integer-le}}{\tt{ .\ }}{\tt{8}}{\tt{)}})\index{tag}, \\ 
{\rm{push}}\,(\=\+{\rm{p-frame}}\,(\=\+{\rm{list}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{ans}}, \\ 
{\rm{value}}\,(\=\+{\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{x}}, \\ 
{\rm{value}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{y}}, \\ 
{\rm{value}}\,(\=\+{\rm{caddr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-)\-, \\ 
{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,({\it{subr\/}}, \=\+{\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} \\ 
$+$$\;\;\;\;${\tt{4}}\-))\-\index{tag})\-\index{p-frame}, \\ 
{\it{ctrl-stk\/}})\-\index{push}, \\ 
{\rm{rput}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{bool}}, {\rm{not-bool}}\,({\it{lt-value\/}})\index{not-bool})\index{tag}, \\ 
{\rm{untag}}\,({\rm{value}}\,(\=\+{\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\index{untag}, \\ 
{\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{rput}, \\ 
{\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}:  mg-integer-le-step-13-true-case \\ \index{mg-integer-le-step-13-true-case}
\=\+(\=\+({\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{predefined-proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;$({\rm{call-name}}\,({\it{stmt\/}})\index{call-name} $=$ {\tt{'}}{\tt{mg-integer-le}}) \\ 
$\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{listp}}\,({\it{ctrl-stk\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match} \\ 
$\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{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;${\rm{ilessp}}\,(\=\+{\rm{untag}}\,({\rm{mg-to-p-simple-literal}}\,({\rm{caddr}}\,({\rm{assoc}}\,(\=\+{\rm{caddr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\-))\index{mg-to-p-simple-literal})\index{untag}, \\ 
{\rm{untag}}\,({\rm{mg-to-p-simple-literal}}\,({\rm{caddr}}\,({\rm{assoc}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\-))\index{mg-to-p-simple-literal})\index{untag})\-\index{ilessp})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{p-step}}\,({\rm{p-state}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{pc}}, {\tt{'}}{\tt{(}}{\tt{mg-integer-le}}{\tt{ .\ }}{\tt{8}}{\tt{)}})\index{tag}, \\ 
{\rm{push}}\,(\=\+{\rm{p-frame}}\,(\=\+{\rm{list}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{ans}}, \\ 
{\rm{value}}\,(\=\+{\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{x}}, \\ 
{\rm{value}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{y}}, \\ 
{\rm{value}}\,(\=\+{\rm{caddr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-)\-, \\ 
{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,({\it{subr\/}}, \=\+{\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} \\ 
$+$$\;\;\;\;${\tt{4}}\-))\-\index{tag})\-\index{p-frame}, \\ 
{\it{ctrl-stk\/}})\-\index{push}, \\ 
{\rm{rput}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{bool}}, {\rm{not-bool}}\,({\tt{'}}{\tt{t}})\index{not-bool})\index{tag}, \\ 
{\rm{untag}}\,({\rm{value}}\,(\=\+{\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\index{untag}, \\ 
{\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{rput}, \\ 
{\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}}\,(\=\+{\it{subr\/}}, \\ 
\=\+{\bf if }{\rm{normal}}\,({\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{normal} \\ 
{\bf then }{\rm{length}}\,({\rm{code}}\,({\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code})\index{length} \\ 
{\bf else }{\rm{find-label}}\,(\=\+{\rm{fetch-label}}\,(\=\+{\rm{cc}}\,({\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{cc}, \\ 
{\rm{label-alist}}\,({\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{label-alist})\-\index{fetch-label}, \\ 
{\rm{append}}\,(\=\+{\rm{code}}\,({\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code}, \\ 
{\it{code2\/}})\-)\-\index{find-label}$\;${\bf  endif}\-)\-)\-\index{tag}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\rm{map-down-values}}\,(\=\+{\rm{mg-alist}}\,({\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{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}}\,({\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{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}:  mg-integer-le-step-13-false-case \\ \index{mg-integer-le-step-13-false-case}
\=\+(\=\+({\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{predefined-proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;$({\rm{call-name}}\,({\it{stmt\/}})\index{call-name} $=$ {\tt{'}}{\tt{mg-integer-le}}) \\ 
$\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{listp}}\,({\it{ctrl-stk\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match} \\ 
$\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{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,(\=\+{\rm{untag}}\,({\rm{mg-to-p-simple-literal}}\,({\rm{caddr}}\,({\rm{assoc}}\,(\=\+{\rm{caddr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\-))\index{mg-to-p-simple-literal})\index{untag}, \\ 
{\rm{untag}}\,({\rm{mg-to-p-simple-literal}}\,({\rm{caddr}}\,({\rm{assoc}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\-))\index{mg-to-p-simple-literal})\index{untag})\-\index{ilessp}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{p-step}}\,({\rm{p-state}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{pc}}, {\tt{'}}{\tt{(}}{\tt{mg-integer-le}}{\tt{ .\ }}{\tt{8}}{\tt{)}})\index{tag}, \\ 
{\rm{push}}\,(\=\+{\rm{p-frame}}\,(\=\+{\rm{list}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{ans}}, \\ 
{\rm{value}}\,(\=\+{\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{x}}, \\ 
{\rm{value}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{y}}, \\ 
{\rm{value}}\,(\=\+{\rm{caddr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-)\-, \\ 
{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,({\it{subr\/}}, \=\+{\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} \\ 
$+$$\;\;\;\;${\tt{4}}\-))\-\index{tag})\-\index{p-frame}, \\ 
{\it{ctrl-stk\/}})\-\index{push}, \\ 
{\rm{rput}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{bool}}, {\rm{not-bool}}\,({\tt{'}}{\tt{f}})\index{not-bool})\index{tag}, \\ 
{\rm{untag}}\,({\rm{value}}\,(\=\+{\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\index{untag}, \\ 
{\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{rput}, \\ 
{\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}}\,(\=\+{\it{subr\/}}, \\ 
\=\+{\bf if }{\rm{normal}}\,({\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{normal} \\ 
{\bf then }{\rm{length}}\,({\rm{code}}\,({\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code})\index{length} \\ 
{\bf else }{\rm{find-label}}\,(\=\+{\rm{fetch-label}}\,(\=\+{\rm{cc}}\,({\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{cc}, \\ 
{\rm{label-alist}}\,({\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{label-alist})\-\index{fetch-label}, \\ 
{\rm{append}}\,(\=\+{\rm{code}}\,({\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code}, \\ 
{\it{code2\/}})\-)\-\index{find-label}$\;${\bf  endif}\-)\-)\-\index{tag}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\rm{map-down-values}}\,(\=\+{\rm{mg-alist}}\,({\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{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}}\,({\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{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}:  mg-integer-le-exact-time-lemma \\ \index{mg-integer-le-exact-time-lemma}
\=\+(\=\+({\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{predefined-proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;$({\rm{call-name}}\,({\it{stmt\/}})\index{call-name} $=$ {\tt{'}}{\tt{mg-integer-le}}) \\ 
$\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{listp}}\,({\it{ctrl-stk\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match} \\ 
$\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{normal}}\,({\it{mg-state\/}})\index{normal})\- \\ 
$\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{clock}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}})\index{clock})\-\index{p} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,(\=\+{\it{subr\/}}, \\ 
\=\+{\bf if }{\rm{normal}}\,({\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{normal} \\ 
{\bf then }{\rm{length}}\,({\rm{code}}\,({\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code})\index{length} \\ 
{\bf else }{\rm{find-label}}\,(\=\+{\rm{fetch-label}}\,(\=\+{\rm{cc}}\,({\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{cc}, \\ 
{\rm{label-alist}}\,({\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{label-alist})\-\index{fetch-label}, \\ 
{\rm{append}}\,(\=\+{\rm{code}}\,({\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code}, \\ 
{\it{code2\/}})\-)\-\index{find-label}$\;${\bf  endif}\-)\-)\-\index{tag}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\rm{map-down-values}}\,(\=\+{\rm{mg-alist}}\,({\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{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}}\,({\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{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{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                           ;;
;;                 EXACT-TIME LEMMA MG-INTEGER-UNARY-MINUS                   ;;
;;                                                                           ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

\end{verbatim}\begin{tabbing}{\sc Theorem}:  min-int-only-non-negatable-small-int \\ \index{min-int-only-non-negatable-smal!l-int}
\=\+({\rm{small-integerp}}\,({\it{x\/}}, {\it{n\/}})\index{small-integerp} $\wedge$ ({\it{x\/}} $\not=$ ($-$ {\rm{exp}}\,({\tt{2}}, {\it{n\/}} $-\;1$)\index{exp}))) \\ 
$\rightarrow$$\;\;\;\;${\rm{small-integerp}}\,({\rm{inegate}}\,({\it{x\/}})\index{inegate}, {\it{n\/}})\index{small-integerp}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mg-integer-unary-minus-args-have-simple-mg-type-refps \\ \index{mg-integer-unary-minus-args-have!-simple-mg-type-refps}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{predefined-proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;$({\rm{call-name}}\,({\it{stmt\/}})\index{call-name} $=$ {\tt{'}}{\tt{mg-integer-unary-minus}}) \\ 
$\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{int-identifierp}}\,({\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), {\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{int-identifierp} \\ 
$\wedge$$\;\;\;\;${\rm{int-identifierp}}\,({\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), {\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{int-identifierp})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mg-integer-unary-minus-args-definedp \\ \index{mg-integer-unary-minus-args-defi!nedp}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{predefined-proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;$({\rm{call-name}}\,({\it{stmt\/}})\index{call-name} $=$ {\tt{'}}{\tt{mg-integer-unary-minus}}) \\ 
$\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{definedp}}\,({\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), {\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{definedp} \\ 
$\wedge$$\;\;\;\;${\rm{definedp}}\,({\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), {\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{definedp})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mg-integer-unary-minus-steps-1-2 \\ \index{mg-integer-unary-minus-steps-1-!2}
\=\+(\=\+({\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{predefined-proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;$({\rm{call-name}}\,({\it{stmt\/}})\index{call-name} $=$ {\tt{'}}{\tt{mg-integer-unary-minus}}) \\ 
$\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{listp}}\,({\it{ctrl-stk\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match} \\ 
$\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{normal}}\,({\it{mg-state\/}})\index{normal})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{p-step}}\,({\rm{p-step}}\,({\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})\index{p-step})\index{p-step} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{pc}}, {\rm{cons}}\,({\it{subr\/}}, {\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} $+$ {\tt{2}}))\index{tag}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\rm{push}}\,(\=\+{\rm{value}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value}, \\ 
{\rm{push}}\,(\=\+{\rm{value}}\,(\=\+{\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value}, \\ 
{\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{push})\-\index{push}, \\ 
{\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}:  mg-integer-unary-minus-step-3 \\ \index{mg-integer-unary-minus-step-3}
\=\+(\=\+({\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{predefined-proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;$({\rm{call-name}}\,({\it{stmt\/}})\index{call-name} $=$ {\tt{'}}{\tt{mg-integer-unary-minus}}) \\ 
$\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{listp}}\,({\it{ctrl-stk\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match} \\ 
$\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{normal}}\,({\it{mg-state\/}})\index{normal})\- \\ 
$\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} $+$ {\tt{2}}))\index{tag}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\rm{push}}\,(\=\+{\rm{value}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value}, \\ 
{\rm{push}}\,(\=\+{\rm{value}}\,(\=\+{\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value}, \\ 
{\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{push})\-\index{push}, \\ 
{\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}}, {\tt{'}}{\tt{(}}{\tt{mg-integer-unary-minus}}{\tt{ .\ }}{\tt{0}}{\tt{)}})\index{tag}, \\ 
{\rm{push}}\,(\=\+{\rm{p-frame}}\,(\=\+{\rm{cons}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{ans}}, \\ 
{\rm{value}}\,(\=\+{\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{x}}, \\ 
{\rm{value}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\tt{'}}{\tt{(}}\=\+{\tt{(}}\=\+{\tt{min-int}}{\tt{ }}{\tt{int}}{\tt{ }}{\tt{-2147483648}}{\tt{)}}\- \\ 
{\tt{(}}{\tt{temp-x}}{\tt{ }}{\tt{int}}{\tt{ }}{\tt{0}}{\tt{)}}{\tt{)}}\-)\-)\-, \\ 
{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,({\it{subr\/}}, \=\+{\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} \\ 
$+$$\;\;\;\;${\tt{3}}\-))\-\index{tag})\-\index{p-frame}, \\ 
{\it{ctrl-stk\/}})\-\index{push}, \\ 
{\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}:  mg-integer-unary-minus-steps-4-8 \\ \index{mg-integer-unary-minus-steps-4-!8}
\=\+(\=\+({\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{predefined-proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;$({\rm{call-name}}\,({\it{stmt\/}})\index{call-name} $=$ {\tt{'}}{\tt{mg-integer-unary-minus}}) \\ 
$\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{listp}}\,({\it{ctrl-stk\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match} \\ 
$\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{normal}}\,({\it{mg-state\/}})\index{normal})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{p-step}}\,({\rm{p-step}}\,({\rm{p-step}}\,({\rm{p-step}}\,({\rm{p-step}}\,({\rm{p-state}}\,(\=\+{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\tt{'}}{\tt{(}}\=\+{\tt{mg-integer-unary-minus}} \\ 
{\tt{.\ }}{\tt{0}}{\tt{)}}\-)\-\index{tag}, \\ 
{\rm{push}}\,(\=\+{\rm{p-frame}}\,(\=\+{\rm{cons}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{ans}}, \\ 
{\rm{value}}\,(\=\+{\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{x}}, \\ 
{\rm{value}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\tt{'}}{\tt{(}}\=\+{\tt{(}}\=\+{\tt{min-int}} \\ 
{\tt{int}} \\ 
{\tt{-2147483648}}{\tt{)}}\- \\ 
{\tt{(}}\=\+{\tt{temp-x}} \\ 
{\tt{int}} \\ 
{\tt{0}}{\tt{)}}\-{\tt{)}}\-)\-)\-, \\ 
{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,(\=\+{\it{subr\/}}, \\ 
\=\+{\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} \\ 
$+$$\;\;\;\;${\tt{3}}\-)\-)\-\index{tag})\-\index{p-frame}, \\ 
{\it{ctrl-stk\/}})\-\index{push}, \\ 
{\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})\index{p-step})\index{p-step})\index{p-step})\index{p-step} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{pc}}, {\tt{'}}{\tt{(}}{\tt{mg-integer-unary-minus}}{\tt{ .\ }}{\tt{5}}{\tt{)}})\index{tag}, \\ 
{\rm{push}}\,(\=\+{\rm{p-frame}}\,(\=\+{\rm{list}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{ans}}, \\ 
{\rm{value}}\,(\=\+{\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{x}}, \\ 
{\rm{value}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\tt{'}}{\tt{(}}{\tt{min-int}}{\tt{ }}{\tt{int}}{\tt{ }}{\tt{-2147483648}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{temp-x}}, \\ 
{\rm{mg-to-p-simple-literal}}\,({\rm{caddr}}\,({\rm{assoc}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\-))\index{mg-to-p-simple-literal})\-)\-, \\ 
{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,({\it{subr\/}}, \=\+{\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} \\ 
$+$$\;\;\;\;${\tt{3}}\-))\-\index{tag})\-\index{p-frame}, \\ 
{\it{ctrl-stk\/}})\-\index{push}, \\ 
{\rm{push}}\,(\=\+{\rm{tag}}\,(\=\+{\tt{'}}{\tt{bool}}, \\ 
\=\+{\bf if }\=\+{\rm{untag}}\,({\rm{mg-to-p-simple-literal}}\,({\rm{caddr}}\,({\rm{assoc}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\-))\index{mg-to-p-simple-literal})\index{untag} \\ 
$=$$\;\;\;\;${\rm{untag}}\,({\tt{'}}{\tt{(}}{\tt{int}}{\tt{ }}{\tt{-2147483648}}{\tt{)}})\index{untag}\- \\ 
{\bf then }{\tt{'}}{\tt{t}} \\ 
{\bf else }{\tt{'}}{\tt{f}}$\;${\bf  endif}\-)\-\index{tag}, \\ 
{\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{push}, \\ 
{\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{verbatim};; (test-bool-and-jump f 0)
;; (push-constant (nat 1))
;; (pop-global c-c)
;; (jump 1)
;; (dl 1 nil (ret))

\end{verbatim}\begin{tabbing}{\sc Theorem}:  mg-integer-unary-minus-steps-9-13-error-case \\ \index{mg-integer-unary-minus-steps-9-!13-error-case}
\=\+(\=\+({\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{predefined-proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;$({\rm{call-name}}\,({\it{stmt\/}})\index{call-name} $=$ {\tt{'}}{\tt{mg-integer-unary-minus}}) \\ 
$\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{listp}}\,({\it{ctrl-stk\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match} \\ 
$\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{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{untag}}\,({\rm{mg-to-p-simple-literal}}\,({\rm{caddr}}\,({\rm{assoc}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\-))\index{mg-to-p-simple-literal})\index{untag} \\ 
$=$$\;\;\;\;${\rm{untag}}\,({\tt{'}}{\tt{(}}{\tt{int}}{\tt{ }}{\tt{-2147483648}}{\tt{)}})\index{untag})\-)\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{p-step}}\,({\rm{p-step}}\,({\rm{p-step}}\,({\rm{p-step}}\,({\rm{p-step}}\,({\rm{p-state}}\,(\=\+{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\tt{'}}{\tt{(}}\=\+{\tt{mg-integer-unary-minus}} \\ 
{\tt{.\ }}{\tt{5}}{\tt{)}}\-)\-\index{tag}, \\ 
{\rm{push}}\,(\=\+{\rm{p-frame}}\,(\=\+{\rm{list}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{ans}}, \\ 
{\rm{value}}\,(\=\+{\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{x}}, \\ 
{\rm{value}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\tt{'}}{\tt{(}}\=\+{\tt{min-int}} \\ 
{\tt{int}} \\ 
{\tt{-2147483648}}{\tt{)}}\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{temp-x}}, \\ 
{\rm{mg-to-p-simple-literal}}\,({\rm{caddr}}\,({\rm{assoc}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\-))\index{mg-to-p-simple-literal})\-)\-, \\ 
{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,(\=\+{\it{subr\/}}, \\ 
\=\+{\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} \\ 
$+$$\;\;\;\;${\tt{3}}\-)\-)\-\index{tag})\-\index{p-frame}, \\ 
{\it{ctrl-stk\/}})\-\index{push}, \\ 
{\rm{push}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{bool}}, {\tt{'}}{\tt{t}})\index{tag}, \\ 
{\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{push}, \\ 
{\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})\index{p-step})\index{p-step})\index{p-step})\index{p-step} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{pc}}, {\rm{cons}}\,({\it{subr\/}}, {\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} $+$ {\tt{3}}))\index{tag}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\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}}, {\tt{'}}{\tt{(}}{\tt{nat}}{\tt{ }}{\tt{1}}{\tt{)}})), \\ 
{\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}:  mg-integer-unary-minus-steps-9-12-nonerror-case \\ \index{mg-integer-unary-minus-steps-9-!12-nonerror-case}
\=\+(\=\+({\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{predefined-proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;$({\rm{call-name}}\,({\it{stmt\/}})\index{call-name} $=$ {\tt{'}}{\tt{mg-integer-unary-minus}}) \\ 
$\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{listp}}\,({\it{ctrl-stk\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match} \\ 
$\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{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{untag}}\,({\rm{mg-to-p-simple-literal}}\,({\rm{caddr}}\,({\rm{assoc}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\-))\index{mg-to-p-simple-literal})\index{untag} \\ 
$\not=$$\;\;\;\;${\rm{untag}}\,({\tt{'}}{\tt{(}}{\tt{int}}{\tt{ }}{\tt{-2147483648}}{\tt{)}})\index{untag})\-)\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{p-step}}\,({\rm{p-step}}\,({\rm{p-step}}\,({\rm{p-step}}\,({\rm{p-state}}\,(\=\+{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\tt{'}}{\tt{(}}\=\+{\tt{mg-integer-unary-minus}} \\ 
{\tt{.\ }}{\tt{5}}{\tt{)}}\-)\-\index{tag}, \\ 
{\rm{push}}\,(\=\+{\rm{p-frame}}\,(\=\+{\rm{list}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{ans}}, \\ 
{\rm{value}}\,(\=\+{\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{x}}, \\ 
{\rm{value}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\tt{'}}{\tt{(}}\=\+{\tt{min-int}} \\ 
{\tt{int}} \\ 
{\tt{-2147483648}}{\tt{)}}\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{temp-x}}, \\ 
{\rm{mg-to-p-simple-literal}}\,({\rm{caddr}}\,({\rm{assoc}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\-))\index{mg-to-p-simple-literal})\-)\-, \\ 
{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,(\=\+{\it{subr\/}}, \\ 
\=\+{\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} \\ 
$+$$\;\;\;\;${\tt{3}}\-)\-)\-\index{tag})\-\index{p-frame}, \\ 
{\it{ctrl-stk\/}})\-\index{push}, \\ 
{\rm{push}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{bool}}, {\tt{'}}{\tt{f}})\index{tag}, \\ 
{\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{push}, \\ 
{\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})\index{p-step})\index{p-step})\index{p-step} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{pc}}, {\tt{'}}{\tt{(}}{\tt{mg-integer-unary-minus}}{\tt{ .\ }}{\tt{12}}{\tt{)}})\index{tag}, \\ 
{\rm{push}}\,(\=\+{\rm{p-frame}}\,(\=\+{\rm{list}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{ans}}, \\ 
{\rm{value}}\,(\=\+{\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{x}}, \\ 
{\rm{value}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\tt{'}}{\tt{(}}{\tt{min-int}}{\tt{ }}{\tt{int}}{\tt{ }}{\tt{-2147483648}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{temp-x}}, \\ 
{\rm{mg-to-p-simple-literal}}\,({\rm{caddr}}\,({\rm{assoc}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\-))\index{mg-to-p-simple-literal})\-)\-, \\ 
{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,({\it{subr\/}}, \=\+{\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} \\ 
$+$$\;\;\;\;${\tt{3}}\-))\-\index{tag})\-\index{p-frame}, \\ 
{\it{ctrl-stk\/}})\-\index{push}, \\ 
{\rm{push}}\,(\=\+{\rm{value}}\,(\=\+{\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value}, \\ 
{\rm{push}}\,(\=\+{\rm{tag}}\,(\=\+{\tt{'}}{\tt{int}}, \\ 
{\rm{inegate}}\,({\rm{untag}}\,({\rm{mg-to-p-simple-literal}}\,({\rm{caddr}}\,({\rm{assoc}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\-))\index{mg-to-p-simple-literal})\index{untag})\index{inegate})\-\index{tag}, \\ 
{\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{push})\-\index{push}, \\ 
{\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{verbatim};; (deposit-temp-stk)
;; (dl 1 nil (ret))

\end{verbatim}\begin{tabbing}{\sc Theorem}:  mg-integer-unary-minus-steps-13-14-nonerror-case \\ \index{mg-integer-unary-minus-steps-13!-14-nonerror-case}
\=\+(\=\+({\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{predefined-proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;$({\rm{call-name}}\,({\it{stmt\/}})\index{call-name} $=$ {\tt{'}}{\tt{mg-integer-unary-minus}}) \\ 
$\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{listp}}\,({\it{ctrl-stk\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match} \\ 
$\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{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{untag}}\,({\rm{mg-to-p-simple-literal}}\,({\rm{caddr}}\,({\rm{assoc}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\-))\index{mg-to-p-simple-literal})\index{untag} \\ 
$\not=$$\;\;\;\;${\rm{untag}}\,({\tt{'}}{\tt{(}}{\tt{int}}{\tt{ }}{\tt{-2147483648}}{\tt{)}})\index{untag})\-)\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{p-step}}\,({\rm{p-step}}\,({\rm{p-state}}\,(\=\+{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\tt{'}}{\tt{(}}{\tt{mg-integer-unary-minus}}{\tt{ .\ }}{\tt{12}}{\tt{)}})\-\index{tag}, \\ 
{\rm{push}}\,(\=\+{\rm{p-frame}}\,(\=\+{\rm{list}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{ans}}, \\ 
{\rm{value}}\,(\=\+{\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{x}}, \\ 
{\rm{value}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\-, \\ 
{\tt{'}}{\tt{(}}\=\+{\tt{min-int}}{\tt{ }}{\tt{int}} \\ 
{\tt{-2147483648}}{\tt{)}}\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{temp-x}}, \\ 
{\rm{mg-to-p-simple-literal}}\,({\rm{caddr}}\,({\rm{assoc}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\-))\index{mg-to-p-simple-literal})\-)\-, \\ 
{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,(\=\+{\it{subr\/}}, \\ 
\=\+{\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} \\ 
$+$$\;\;\;\;${\tt{3}}\-)\-)\-\index{tag})\-\index{p-frame}, \\ 
{\it{ctrl-stk\/}})\-\index{push}, \\ 
{\rm{push}}\,(\=\+{\rm{value}}\,(\=\+{\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value}, \\ 
{\rm{push}}\,(\=\+{\rm{tag}}\,(\=\+{\tt{'}}{\tt{int}}, \\ 
{\rm{inegate}}\,({\rm{untag}}\,({\rm{mg-to-p-simple-literal}}\,({\rm{caddr}}\,({\rm{assoc}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\-))\index{mg-to-p-simple-literal})\index{untag})\index{inegate})\-\index{tag}, \\ 
{\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{push})\-\index{push}, \\ 
{\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})\index{p-step} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{pc}}, {\rm{cons}}\,({\it{subr\/}}, {\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} $+$ {\tt{3}}))\index{tag}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\rm{rput}}\,(\=\+{\rm{tag}}\,(\=\+{\tt{'}}{\tt{int}}, \\ 
{\rm{inegate}}\,({\rm{untag}}\,({\rm{caddr}}\,({\rm{assoc}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\-))\index{untag})\index{inegate})\-\index{tag}, \\ 
{\rm{untag}}\,({\rm{value}}\,(\=\+{\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\index{untag}, \\ 
{\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{rput}, \\ 
{\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}:  mg-integer-unary-minus-push-c-c-effect \\ \index{mg-integer-unary-minus-push-c-c!-effect}
\=\+(\=\+({\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{predefined-proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;$({\rm{call-name}}\,({\it{stmt\/}})\index{call-name} $=$ {\tt{'}}{\tt{mg-integer-unary-minus}}) \\ 
$\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{listp}}\,({\it{ctrl-stk\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match} \\ 
$\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{normal}}\,({\it{mg-state\/}})\index{normal})\- \\ 
$\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} $+$ {\tt{3}}))\index{tag}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\it{temp-stk\/}}, \\ 
{\rm{translate-proc-list}}\,({\it{proc-list\/}})\index{translate-proc-list}, \\ 
{\rm{list}}\,({\rm{list}}\,({\tt{'}}{\tt{c-c}}, {\it{cc-value\/}})), \\ 
{\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}}\,({\it{subr\/}}, {\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} $+$ {\tt{4}}))\index{tag}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\rm{push}}\,({\it{cc-value\/}}, {\it{temp-stk\/}})\index{push}, \\ 
{\rm{translate-proc-list}}\,({\it{proc-list\/}})\index{translate-proc-list}, \\ 
{\rm{list}}\,({\rm{list}}\,({\tt{'}}{\tt{c-c}}, {\it{cc-value\/}})), \\ 
{\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}:  mg-integer-unary-minus-sub1-nat-effect \\ \index{mg-integer-unary-minus-sub1-nat!-effect}
\=\+(\=\+({\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{predefined-proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;$({\rm{call-name}}\,({\it{stmt\/}})\index{call-name} $=$ {\tt{'}}{\tt{mg-integer-unary-minus}}) \\ 
$\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{listp}}\,({\it{ctrl-stk\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\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$$\;\;\;\;$({\it{cc-value\/}} $\in$ {\rm{list}}\,({\tt{'}}{\tt{(}}{\tt{nat}}{\tt{ }}{\tt{1}}{\tt{)}}, {\tt{'}}{\tt{(}}{\tt{nat}}{\tt{ }}{\tt{2}}{\tt{)}})))\- \\ 
$\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} $+$ {\tt{4}}))\index{tag}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\rm{push}}\,({\it{cc-value\/}}, {\it{temp-stk\/}})\index{push}, \\ 
{\rm{translate-proc-list}}\,({\it{proc-list\/}})\index{translate-proc-list}, \\ 
{\rm{list}}\,({\rm{list}}\,({\tt{'}}{\tt{c-c}}, {\it{cc-value\/}})), \\ 
{\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}}\,({\it{subr\/}}, {\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} $+$ {\tt{5}}))\index{tag}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\rm{push}}\,({\rm{tag}}\,({\tt{'}}{\tt{nat}}, {\rm{untag}}\,({\it{cc-value\/}})\index{untag} $-\;1$)\index{tag}, {\it{temp-stk\/}})\index{push}, \\ 
{\rm{translate-proc-list}}\,({\it{proc-list\/}})\index{translate-proc-list}, \\ 
{\rm{list}}\,({\rm{list}}\,({\tt{'}}{\tt{c-c}}, {\it{cc-value\/}})), \\ 
{\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}:  mg-integer-unary-minus-step-16-error \\ \index{mg-integer-unary-minus-step-16-e!rror}
\=\+(\=\+({\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{predefined-proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;$({\rm{call-name}}\,({\it{stmt\/}})\index{call-name} $=$ {\tt{'}}{\tt{mg-integer-unary-minus}}) \\ 
$\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{listp}}\,({\it{ctrl-stk\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match} \\ 
$\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{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{untag}}\,({\rm{mg-to-p-simple-literal}}\,({\rm{caddr}}\,({\rm{assoc}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\-))\index{mg-to-p-simple-literal})\index{untag} \\ 
$=$$\;\;\;\;${\rm{untag}}\,({\tt{'}}{\tt{(}}{\tt{int}}{\tt{ }}{\tt{-2147483648}}{\tt{)}})\index{untag})\-)\- \\ 
$\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} $+$ {\tt{5}}))\index{tag}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\rm{push}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{nat}}, {\rm{untag}}\,({\tt{'}}{\tt{(}}{\tt{nat}}{\tt{ }}{\tt{1}}{\tt{)}})\index{untag} $-\;1$)\index{tag}, \\ 
{\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{push}, \\ 
{\rm{translate-proc-list}}\,({\it{proc-list\/}})\index{translate-proc-list}, \\ 
{\tt{'}}{\tt{(}}{\tt{(}}{\tt{c-c}}{\tt{ }}{\tt{(}}{\tt{nat}}{\tt{ }}{\tt{1}}{\tt{)}}{\tt{)}}{\tt{)}}, \\ 
{\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}}\,(\=\+{\it{subr\/}}, \\ 
\=\+{\bf if }{\rm{normal}}\,({\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{normal} \\ 
{\bf then }{\rm{length}}\,({\rm{code}}\,({\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code})\index{length} \\ 
{\bf else }{\rm{find-label}}\,(\=\+{\rm{fetch-label}}\,(\=\+{\rm{cc}}\,({\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{cc}, \\ 
{\rm{label-alist}}\,({\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{label-alist})\-\index{fetch-label}, \\ 
{\rm{append}}\,(\=\+{\rm{code}}\,({\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code}, \\ 
{\it{code2\/}})\-)\-\index{find-label}$\;${\bf  endif}\-)\-)\-\index{tag}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\rm{map-down-values}}\,(\=\+{\rm{mg-alist}}\,({\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{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}}\,({\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{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}:  mg-integer-unary-minus-step-17-nonerror \\ \index{mg-integer-unary-minus-step-17-!nonerror}
\=\+(\=\+({\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{predefined-proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;$({\rm{call-name}}\,({\it{stmt\/}})\index{call-name} $=$ {\tt{'}}{\tt{mg-integer-unary-minus}}) \\ 
$\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{listp}}\,({\it{ctrl-stk\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match} \\ 
$\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{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{untag}}\,({\rm{mg-to-p-simple-literal}}\,({\rm{caddr}}\,({\rm{assoc}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\-))\index{mg-to-p-simple-literal})\index{untag} \\ 
$\not=$$\;\;\;\;${\rm{untag}}\,({\tt{'}}{\tt{(}}{\tt{int}}{\tt{ }}{\tt{-2147483648}}{\tt{)}})\index{untag})\-)\- \\ 
$\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} $+$ {\tt{5}}))\index{tag}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\rm{push}}\,(\=\+{\rm{tag}}\,(\=\+{\tt{'}}{\tt{nat}}, \\ 
{\rm{untag}}\,({\rm{mg-cond-to-p-nat}}\,(\=\+{\rm{cc}}\,({\it{mg-state\/}})\index{cc}, \\ 
{\it{t-cond-list\/}})\-\index{mg-cond-to-p-nat})\index{untag} $-\;1$)\-\index{tag}, \\ 
{\rm{rput}}\,(\=\+{\rm{tag}}\,(\=\+{\tt{'}}{\tt{int}}, \\ 
{\rm{inegate}}\,({\rm{untag}}\,({\rm{caddr}}\,({\rm{assoc}}\,(\=\+{\rm{cadr}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\-))\index{untag})\index{inegate})\-\index{tag}, \\ 
{\rm{untag}}\,({\rm{value}}\,(\=\+{\rm{car}}\,({\rm{call-actuals}}\,({\it{stmt\/}})\index{call-actuals}), \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\-\index{value})\index{untag}, \\ 
{\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{rput})\-\index{push}, \\ 
{\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}}\,(\=\+{\it{subr\/}}, \\ 
\=\+{\bf if }{\rm{normal}}\,({\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{normal} \\ 
{\bf then }{\rm{length}}\,({\rm{code}}\,({\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code})\index{length} \\ 
{\bf else }{\rm{find-label}}\,(\=\+{\rm{fetch-label}}\,(\=\+{\rm{cc}}\,({\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{cc}, \\ 
{\rm{label-alist}}\,({\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{label-alist})\-\index{fetch-label}, \\ 
{\rm{append}}\,(\=\+{\rm{code}}\,({\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code}, \\ 
{\it{code2\/}})\-)\-\index{find-label}$\;${\bf  endif}\-)\-)\-\index{tag}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\rm{map-down-values}}\,(\=\+{\rm{mg-alist}}\,({\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{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}}\,({\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{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}:  mg-integer-unary-minus-exact-time-lemma \\ \index{mg-integer-unary-minus-exact-ti!me-lemma}
\=\+(\=\+({\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{predefined-proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;$({\rm{call-name}}\,({\it{stmt\/}})\index{call-name} $=$ {\tt{'}}{\tt{mg-integer-unary-minus}}) \\ 
$\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{listp}}\,({\it{ctrl-stk\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match} \\ 
$\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{normal}}\,({\it{mg-state\/}})\index{normal})\- \\ 
$\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{clock}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}})\index{clock})\-\index{p} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,(\=\+{\it{subr\/}}, \\ 
\=\+{\bf if }{\rm{normal}}\,({\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{normal} \\ 
{\bf then }{\rm{length}}\,({\rm{code}}\,({\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code})\index{length} \\ 
{\bf else }{\rm{find-label}}\,(\=\+{\rm{fetch-label}}\,(\=\+{\rm{cc}}\,({\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{cc}, \\ 
{\rm{label-alist}}\,({\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{label-alist})\-\index{fetch-label}, \\ 
{\rm{append}}\,(\=\+{\rm{code}}\,({\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code}, \\ 
{\it{code2\/}})\-)\-\index{find-label}$\;${\bf  endif}\-)\-)\-\index{tag}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\rm{map-down-values}}\,(\=\+{\rm{mg-alist}}\,({\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{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}}\,({\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{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}:   Make the library {\tt{"c-predefined2"}}.

\addvspace{18pt}

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