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

\addvspace{18pt}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                           ;;
;;                           EXACT-TIME IF CASE                              ;;
;;                                                                           ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

\end{verbatim}\begin{tabbing}{\sc Theorem}:  if-condition-boolean-identifierp \\ \index{if-condition-boolean-identifierp}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{if-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statep}}\,({\it{mg-state\/}}, {\it{cond-list\/}})\index{ok-mg-statep} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{r-cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{boolean-identifierp}}\,({\rm{if-condition}}\,({\it{stmt\/}})\index{if-condition}, {\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{boolean-identifierp}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  fetch-boolean-identifier-ins-okp \\ \index{fetch-boolean-identifier-ins-okp}
\=\+(\=\+{\rm{boolean-identifierp}}\,({\it{b\/}}, {\it{mg-vars\/}})\index{boolean-identifierp} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\it{mg-vars\/}})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;$({\rm{length}}\,({\it{temp-stk\/}})\index{length} $<$ {\sc{mg-max-temp-stk-size}}\index{mg-max-temp-stk-size}) \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{mg-vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{type}}\,({\rm{value}}\,({\it{b\/}}, {\it{bindings\/}})\index{value})\index{type} $=$ {\tt{'}}{\tt{nat}}) \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\rm{value}}\,({\it{b\/}}, {\it{bindings\/}})\index{value}) \\ 
$\wedge$$\;\;\;\;$({\rm{cddr}}\,({\rm{value}}\,({\it{b\/}}, {\it{bindings\/}})\index{value}) $=$ {\bf{nil}}) \\ 
$\wedge$$\;\;\;\;${\rm{small-naturalp}}\,({\rm{untag}}\,({\rm{value}}\,({\it{b\/}}, {\it{bindings\/}})\index{value})\index{untag}, {\tt{32}})\index{small-naturalp} \\ 
$\wedge$$\;\;\;\;$(({\rm{untag}}\,({\rm{value}}\,({\it{b\/}}, {\it{bindings\/}})\index{value})\index{untag} $<$ ($1\;+$ {\rm{length}}\,({\it{temp-stk\/}})\index{length})) $=$ {\bf{t}}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  if-translation-2 \\ \index{if-translation-2}
\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{if-mg}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{translate}}\,({\it{cinfo\/}}, {\it{cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}})\index{translate} \\ 
$=$$\;\;\;\;${\rm{add-code}}\,(\=\+{\rm{translate}}\,(\=\+{\rm{add-code}}\,(\=\+{\rm{translate}}\,(\=\+{\rm{make-cinfo}}\,(\=\+{\rm{append}}\,(\=\+{\rm{code}}\,({\it{cinfo\/}})\index{code}, \\ 
{\rm{list}}\,(\=\+{\rm{list}}\,(\=\+{\tt{'}}{\tt{push-local}}, \\ 
{\rm{if-condition}}\,({\it{stmt\/}})\index{if-condition})\-, \\ 
{\tt{'}}{\tt{(}}\=\+{\tt{fetch-temp-stk}}{\tt{)}}\-, \\ 
{\rm{list}}\,(\=\+{\tt{'}}{\tt{test-bool-and-jump}}, \\ 
{\tt{'}}{\tt{false}}, \\ 
{\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt})\-)\-)\-, \\ 
{\rm{label-alist}}\,({\it{cinfo\/}})\index{label-alist}, \\ 
$1\;+$ ($1\;+$ {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}))\-\index{make-cinfo}, \\ 
{\it{cond-list\/}}, \\ 
{\rm{if-true-branch}}\,({\it{stmt\/}})\index{if-true-branch}, \\ 
{\it{proc-list\/}})\-\index{translate}, \\ 
{\rm{list}}\,(\=\+{\rm{list}}\,(\=\+{\tt{'}}{\tt{jump}}, \\ 
$1\;+$ {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt})\-, \\ 
{\rm{list}}\,(\=\+{\tt{'}}{\tt{dl}}, \\ 
{\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}, \\ 
{\bf{nil}}, \\ 
{\tt{'}}{\tt{(}}{\tt{no-op}}{\tt{)}})\-)\-)\-\index{add-code}, \\ 
{\it{cond-list\/}}, \\ 
{\rm{if-false-branch}}\,({\it{stmt\/}})\index{if-false-branch}, \\ 
{\it{proc-list\/}})\-\index{translate}, \\ 
{\rm{list}}\,({\rm{list}}\,({\tt{'}}{\tt{dl}}, $1\;+$ {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}, {\bf{nil}}, {\tt{'}}{\tt{(}}{\tt{no-op}}{\tt{)}})))\-\index{add-code})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  if-meaning-r-2 \\ \index{if-meaning-r-2}
\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{if-mg}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{mg-meaning-r}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}}, {\it{sizes\/}})\index{mg-meaning-r} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{signal-system-error}}\,({\it{mg-state\/}}, {\tt{'}}{\tt{timed-out}})\index{signal-system-error} \\ 
{\bf elseif }$\neg$ {\rm{normal}}\,({\it{mg-state\/}})\index{normal}$\;\;${\bf then }{\it{mg-state\/}} \\ 
{\bf elseif }{\rm{resources-inadequatep}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{sizes\/}})\index{resources-inadequatep} \\ 
{\bf then }{\rm{signal-system-error}}\,({\it{mg-state\/}}, {\tt{'}}{\tt{resource-error}})\index{signal-system-error} \\ 
{\bf elseif }{\rm{mg-expression-falsep}}\,({\rm{if-condition}}\,({\it{stmt\/}})\index{if-condition}, {\it{mg-state\/}})\index{mg-expression-falsep} \\ 
{\bf then }{\rm{mg-meaning-r}}\,(\=\+{\rm{if-false-branch}}\,({\it{stmt\/}})\index{if-false-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{sizes\/}})\-\index{mg-meaning-r} \\ 
{\bf else }{\rm{mg-meaning-r}}\,(\=\+{\rm{if-true-branch}}\,({\it{stmt\/}})\index{if-true-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{sizes\/}})\-\index{mg-meaning-r}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  if-false-branch-doesnt-halt \\ \index{if-false-branch-doesnt-halt}
\=\+(\=\+({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{if-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;${\rm{mg-expression-falsep}}\,({\rm{if-condition}}\,({\it{stmt\/}})\index{if-condition}, {\it{mg-state\/}})\index{mg-expression-falsep} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resource-errorp}}\,({\rm{mg-meaning-r}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}}, {\it{sizes\/}})\index{mg-meaning-r})\index{resource-errorp}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{mg-psw}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{if-false-branch}}\,({\it{stmt\/}})\index{if-false-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{sizes\/}})\-\index{mg-meaning-r})\index{mg-psw} \\ 
$=$$\;\;\;\;${\tt{'}}{\tt{run}})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  if-true-branch-doesnt-halt \\ \index{if-true-branch-doesnt-halt}
\=\+(\=\+({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{if-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{mg-expression-falsep}}\,({\rm{if-condition}}\,({\it{stmt\/}})\index{if-condition}, {\it{mg-state\/}})\index{mg-expression-falsep}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resource-errorp}}\,({\rm{mg-meaning-r}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}}, {\it{sizes\/}})\index{mg-meaning-r})\index{resource-errorp}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{mg-psw}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{if-true-branch}}\,({\it{stmt\/}})\index{if-true-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{sizes\/}})\-\index{mg-meaning-r})\index{mg-psw} \\ 
$=$$\;\;\;\;${\tt{'}}{\tt{run}})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  if-code-rewrite1 \\ \index{if-code-rewrite1}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{if-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{r-cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{append}}\,({\rm{code}}\,({\rm{translate}}\,({\it{cinfo\/}}, {\it{t-cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}})\index{translate})\index{code}, {\it{code2\/}}) \\ 
$=$$\;\;\;\;${\rm{append}}\,(\=\+{\rm{code}}\,({\rm{translate}}\,(\=\+{\rm{add-code}}\,(\=\+{\rm{translate}}\,(\=\+{\rm{make-cinfo}}\,(\=\+{\rm{append}}\,(\=\+{\rm{code}}\,({\it{cinfo\/}})\index{code}, \\ 
{\rm{list}}\,(\=\+{\rm{list}}\,(\=\+{\tt{'}}{\tt{push-local}}, \\ 
{\rm{if-condition}}\,({\it{stmt\/}})\index{if-condition})\-, \\ 
{\tt{'}}{\tt{(}}\=\+{\tt{fetch-temp-stk}}{\tt{)}}\-, \\ 
{\rm{list}}\,(\=\+{\tt{'}}{\tt{test-bool-and-jump}}, \\ 
{\tt{'}}{\tt{false}}, \\ 
{\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt})\-)\-)\-, \\ 
{\rm{label-alist}}\,({\it{cinfo\/}})\index{label-alist}, \\ 
$1\;+$ ($1\;+$ {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}))\-\index{make-cinfo}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{if-true-branch}}\,({\it{stmt\/}})\index{if-true-branch}, \\ 
{\it{proc-list\/}})\-\index{translate}, \\ 
{\rm{list}}\,(\=\+{\rm{list}}\,(\=\+{\tt{'}}{\tt{jump}}, \\ 
$1\;+$ {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{dl}}, \\ 
{\rm{cons}}\,(\=\+{\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}, \\ 
{\tt{'}}{\tt{(}}\=\+{\tt{nil}} \\ 
{\tt{(}}{\tt{no-op}}{\tt{)}}{\tt{)}}\-)\-)\-)\-)\-\index{add-code}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{if-false-branch}}\,({\it{stmt\/}})\index{if-false-branch}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code}, \\ 
{\rm{cons}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{dl}}, \\ 
{\rm{cons}}\,(\=\+$1\;+$ {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}, \\ 
{\tt{'}}{\tt{(}}{\tt{nil}}{\tt{ }}{\tt{(}}{\tt{no-op}}{\tt{)}}{\tt{)}})\-)\-, \\ 
{\it{code2\/}})\-)\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  if-code-rewrite2 \\ \index{if-code-rewrite2}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{if-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{r-cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{append}}\,({\rm{code}}\,({\rm{translate}}\,({\it{cinfo\/}}, {\it{t-cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}})\index{translate})\index{code}, {\it{code2\/}}) \\ 
$=$$\;\;\;\;${\rm{append}}\,(\=\+{\rm{code}}\,({\rm{translate}}\,(\=\+{\rm{make-cinfo}}\,(\=\+{\rm{append}}\,(\=\+{\rm{code}}\,({\it{cinfo\/}})\index{code}, \\ 
{\rm{list}}\,(\=\+{\rm{list}}\,(\=\+{\tt{'}}{\tt{push-local}}, \\ 
{\rm{if-condition}}\,({\it{stmt\/}})\index{if-condition})\-, \\ 
{\tt{'}}{\tt{(}}\=\+{\tt{fetch-temp-stk}}{\tt{)}}\-, \\ 
{\rm{list}}\,(\=\+{\tt{'}}{\tt{test-bool-and-jump}}, \\ 
{\tt{'}}{\tt{false}}, \\ 
{\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt})\-)\-)\-, \\ 
{\rm{label-alist}}\,({\it{cinfo\/}})\index{label-alist}, \\ 
$1\;+$ ($1\;+$ {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}))\-\index{make-cinfo}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{if-true-branch}}\,({\it{stmt\/}})\index{if-true-branch}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code}, \\ 
{\rm{cons}}\,(\=\+{\rm{list}}\,({\tt{'}}{\tt{jump}}, $1\;+$ {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}), \\ 
{\rm{cons}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{dl}}, \\ 
{\rm{cons}}\,(\=\+{\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}, \\ 
{\tt{'}}{\tt{(}}{\tt{nil}}{\tt{ }}{\tt{(}}{\tt{no-op}}{\tt{)}}{\tt{)}})\-)\-, \\ 
{\rm{append}}\,(\=\+{\rm{code}}\,({\rm{translate}}\,(\=\+{\rm{nullify}}\,({\rm{translate}}\,(\=\+{\rm{make-cinfo}}\,(\=\+{\bf{nil}}, \\ 
{\rm{label-alist}}\,({\it{cinfo\/}})\index{label-alist}, \\ 
$1\;+$ ($1\;+$ {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}))\-\index{make-cinfo}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{if-true-branch}}\,({\it{stmt\/}})\index{if-true-branch}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{nullify}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{if-false-branch}}\,({\it{stmt\/}})\index{if-false-branch}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code}, \\ 
{\rm{cons}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{dl}}, \\ 
{\rm{cons}}\,(\=\+$1\;+$ {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}, \\ 
{\tt{'}}{\tt{(}}{\tt{nil}}{\tt{ }}{\tt{(}}{\tt{no-op}}{\tt{)}}{\tt{)}})\-)\-, \\ 
{\it{code2\/}})\-)\-)\-)\-)\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  if-false-branch-hyps \\ \index{if-false-branch-hyps}
\=\+(\=\+({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{if-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{r-cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{ok-translation-parameters}}\,({\it{cinfo\/}}, {\it{t-cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}}, {\it{code2\/}})\index{ok-translation-parameters} \\ 
$\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{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resource-errorp}}\,({\rm{mg-meaning-r}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{resource-errorp}) \\ 
$\wedge$$\;\;\;\;${\rm{mg-expression-falsep}}\,({\rm{if-condition}}\,({\it{stmt\/}})\index{if-condition}, {\it{mg-state\/}})\index{mg-expression-falsep})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{ok-mg-statement}}\,(\=\+{\rm{if-false-branch}}\,({\it{stmt\/}})\index{if-false-branch}, \\ 
{\it{r-cond-list\/}}, \\ 
{\it{name-alist\/}}, \\ 
{\it{proc-list\/}})\-\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{ok-translation-parameters}}\,(\=\+{\rm{add-code}}\,(\=\+{\rm{translate}}\,(\=\+{\rm{make-cinfo}}\,(\=\+{\rm{append}}\,(\=\+{\rm{code}}\,({\it{cinfo\/}})\index{code}, \\ 
{\rm{list}}\,(\=\+{\rm{list}}\,(\=\+{\tt{'}}{\tt{push-local}}, \\ 
{\rm{if-condition}}\,({\it{stmt\/}})\index{if-condition})\-, \\ 
{\tt{'}}{\tt{(}}\=\+{\tt{fetch-temp-stk}}{\tt{)}}\-, \\ 
{\rm{list}}\,(\=\+{\tt{'}}{\tt{test-bool-and-jump}}, \\ 
{\tt{'}}{\tt{false}}, \\ 
{\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt})\-)\-)\-, \\ 
{\rm{label-alist}}\,({\it{cinfo\/}})\index{label-alist}, \\ 
$1\;+$ ($1\;+$ {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}))\-\index{make-cinfo}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{if-true-branch}}\,({\it{stmt\/}})\index{if-true-branch}, \\ 
{\it{proc-list\/}})\-\index{translate}, \\ 
{\rm{list}}\,(\=\+{\rm{list}}\,(\=\+{\tt{'}}{\tt{jump}}, \\ 
$1\;+$ {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{dl}}, \\ 
{\rm{cons}}\,(\=\+{\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}, \\ 
{\tt{'}}{\tt{(}}\=\+{\tt{nil}} \\ 
{\tt{(}}\=\+{\tt{no-op}}{\tt{)}}\-{\tt{)}}\-)\-)\-)\-)\-\index{add-code}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{if-false-branch}}\,({\it{stmt\/}})\index{if-false-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{cons}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{dl}}, \\ 
{\rm{cons}}\,(\=\+$1\;+$ {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}, \\ 
{\tt{'}}{\tt{(}}{\tt{nil}}{\tt{ }}{\tt{(}}{\tt{no-op}}{\tt{)}}{\tt{)}})\-)\-, \\ 
{\it{code2\/}})\-)\-\index{ok-translation-parameters} \\ 
$\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}}\,(\=\+{\rm{add-code}}\,(\=\+{\rm{translate}}\,(\=\+{\rm{make-cinfo}}\,(\=\+{\rm{append}}\,(\=\+{\rm{code}}\,({\it{cinfo\/}})\index{code}, \\ 
{\rm{list}}\,(\=\+{\rm{list}}\,(\=\+{\tt{'}}{\tt{push-local}}, \\ 
{\rm{if-condition}}\,({\it{stmt\/}})\index{if-condition})\-, \\ 
{\tt{'}}{\tt{(}}\=\+{\tt{fetch-temp-stk}}{\tt{)}}\-, \\ 
{\rm{list}}\,(\=\+{\tt{'}}{\tt{test-bool-and-jump}}, \\ 
{\tt{'}}{\tt{false}}, \\ 
{\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt})\-)\-)\-, \\ 
{\rm{label-alist}}\,({\it{cinfo\/}})\index{label-alist}, \\ 
$1\;+$ ($1\;+$ {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}))\-\index{make-cinfo}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{if-true-branch}}\,({\it{stmt\/}})\index{if-true-branch}, \\ 
{\it{proc-list\/}})\-\index{translate}, \\ 
{\rm{list}}\,(\=\+{\rm{list}}\,(\=\+{\tt{'}}{\tt{jump}}, \\ 
$1\;+$ {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{dl}}, \\ 
{\rm{cons}}\,(\=\+{\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}, \\ 
{\tt{'}}{\tt{(}}\=\+{\tt{nil}} \\ 
{\tt{(}}\=\+{\tt{no-op}}{\tt{)}}\-{\tt{)}}\-)\-)\-)\-)\-\index{add-code}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{if-false-branch}}\,({\it{stmt\/}})\index{if-false-branch}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code}, \\ 
{\rm{cons}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{dl}}, \\ 
{\rm{cons}}\,(\=\+$1\;+$ {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}, \\ 
{\tt{'}}{\tt{(}}{\tt{nil}}{\tt{ }}{\tt{(}}{\tt{no-op}}{\tt{)}}{\tt{)}})\-)\-, \\ 
{\it{code2\/}})\-)\-)\- \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resource-errorp}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{if-false-branch}}\,({\it{stmt\/}})\index{if-false-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{resource-errorp}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  if-true-branch-hyps \\ \index{if-true-branch-hyps}
\=\+(\=\+({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{if-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{r-cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{ok-translation-parameters}}\,({\it{cinfo\/}}, {\it{t-cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}}, {\it{code2\/}})\index{ok-translation-parameters} \\ 
$\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{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resource-errorp}}\,({\rm{mg-meaning-r}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{resource-errorp}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{mg-expression-falsep}}\,({\rm{if-condition}}\,({\it{stmt\/}})\index{if-condition}, {\it{mg-state\/}})\index{mg-expression-falsep}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{ok-mg-statement}}\,(\=\+{\rm{if-true-branch}}\,({\it{stmt\/}})\index{if-true-branch}, \\ 
{\it{r-cond-list\/}}, \\ 
{\it{name-alist\/}}, \\ 
{\it{proc-list\/}})\-\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{ok-translation-parameters}}\,(\=\+{\rm{make-cinfo}}\,(\=\+{\rm{append}}\,(\=\+{\rm{code}}\,({\it{cinfo\/}})\index{code}, \\ 
{\rm{list}}\,(\=\+{\rm{list}}\,(\=\+{\tt{'}}{\tt{push-local}}, \\ 
{\rm{if-condition}}\,({\it{stmt\/}})\index{if-condition})\-, \\ 
{\tt{'}}{\tt{(}}\=\+{\tt{fetch-temp-stk}}{\tt{)}}\-, \\ 
{\rm{list}}\,(\=\+{\tt{'}}{\tt{test-bool-and-jump}}, \\ 
{\tt{'}}{\tt{false}}, \\ 
{\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt})\-)\-)\-, \\ 
{\rm{label-alist}}\,({\it{cinfo\/}})\index{label-alist}, \\ 
$1\;+$ ($1\;+$ {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}))\-\index{make-cinfo}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{if-true-branch}}\,({\it{stmt\/}})\index{if-true-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{cons}}\,(\=\+{\rm{list}}\,(\=\+{\tt{'}}{\tt{jump}}, \\ 
$1\;+$ {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt})\-, \\ 
{\rm{cons}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{dl}}, \\ 
{\rm{cons}}\,(\=\+{\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}, \\ 
{\tt{'}}{\tt{(}}\=\+{\tt{nil}} \\ 
{\tt{(}}{\tt{no-op}}{\tt{)}}{\tt{)}}\-)\-)\-, \\ 
{\rm{append}}\,(\=\+{\rm{code}}\,({\rm{translate}}\,(\=\+{\rm{nullify}}\,({\rm{translate}}\,(\=\+{\rm{make-cinfo}}\,(\=\+{\bf{nil}}, \\ 
{\rm{label-alist}}\,({\it{cinfo\/}})\index{label-alist}, \\ 
$1\;+$ ($1\;+$ {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}))\-\index{make-cinfo}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{if-true-branch}}\,({\it{stmt\/}})\index{if-true-branch}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{nullify}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{if-false-branch}}\,({\it{stmt\/}})\index{if-false-branch}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code}, \\ 
{\rm{cons}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{dl}}, \\ 
{\rm{cons}}\,(\=\+$1\;+$ {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}, \\ 
{\tt{'}}{\tt{(}}\=\+{\tt{nil}} \\ 
{\tt{(}}\=\+{\tt{no-op}}{\tt{)}}\-{\tt{)}}\-)\-)\-, \\ 
{\it{code2\/}})\-)\-)\-)\-)\-\index{ok-translation-parameters} \\ 
$\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}}\,(\=\+{\rm{make-cinfo}}\,(\=\+{\rm{append}}\,(\=\+{\rm{code}}\,({\it{cinfo\/}})\index{code}, \\ 
{\rm{list}}\,(\=\+{\rm{list}}\,(\=\+{\tt{'}}{\tt{push-local}}, \\ 
{\rm{if-condition}}\,({\it{stmt\/}})\index{if-condition})\-, \\ 
{\tt{'}}{\tt{(}}\=\+{\tt{fetch-temp-stk}}{\tt{)}}\-, \\ 
{\rm{list}}\,(\=\+{\tt{'}}{\tt{test-bool-and-jump}}, \\ 
{\tt{'}}{\tt{false}}, \\ 
{\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt})\-)\-)\-, \\ 
{\rm{label-alist}}\,({\it{cinfo\/}})\index{label-alist}, \\ 
$1\;+$ ($1\;+$ {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}))\-\index{make-cinfo}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{if-true-branch}}\,({\it{stmt\/}})\index{if-true-branch}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code}, \\ 
{\rm{cons}}\,(\=\+{\rm{list}}\,({\tt{'}}{\tt{jump}}, $1\;+$ {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}), \\ 
{\rm{cons}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{dl}}, \\ 
{\rm{cons}}\,(\=\+{\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}, \\ 
{\tt{'}}{\tt{(}}{\tt{nil}}{\tt{ }}{\tt{(}}{\tt{no-op}}{\tt{)}}{\tt{)}})\-)\-, \\ 
{\rm{append}}\,(\=\+{\rm{code}}\,({\rm{translate}}\,(\=\+{\rm{nullify}}\,({\rm{translate}}\,(\=\+{\rm{make-cinfo}}\,(\=\+{\bf{nil}}, \\ 
{\rm{label-alist}}\,({\it{cinfo\/}})\index{label-alist}, \\ 
$1\;+$ ($1\;+$ {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}))\-\index{make-cinfo}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{if-true-branch}}\,({\it{stmt\/}})\index{if-true-branch}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{nullify}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{if-false-branch}}\,({\it{stmt\/}})\index{if-false-branch}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code}, \\ 
{\rm{cons}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{dl}}, \\ 
{\rm{cons}}\,(\=\+$1\;+$ {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}, \\ 
{\tt{'}}{\tt{(}}\=\+{\tt{nil}} \\ 
{\tt{(}}{\tt{no-op}}{\tt{)}}{\tt{)}}\-)\-)\-, \\ 
{\it{code2\/}})\-)\-)\-)\-)\-)\- \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resource-errorp}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{if-true-branch}}\,({\it{stmt\/}})\index{if-true-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{resource-errorp}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  if-initial-step1 \\ \index{if-initial-step1}
\=\+(\=\+({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{if-mg}}) \\ 
$\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{ok-mg-statement}}\,({\it{stmt\/}}, {\it{r-cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\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{ok-mg-statep}}\,({\it{mg-state\/}}, {\it{r-cond-list\/}})\index{ok-mg-statep} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\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{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resource-errorp}}\,({\rm{mg-meaning-r}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{resource-errorp}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{p-step}}\,({\rm{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} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{pc}}, {\rm{cons}}\,({\it{subr\/}}, {\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} $+$ {\tt{1}}))\index{tag}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\rm{push}}\,(\=\+{\rm{value}}\,({\rm{if-condition}}\,({\it{stmt\/}})\index{if-condition}, {\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}:  if-initial-step2 \\ \index{if-initial-step2}
\=\+(\=\+({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{if-mg}}) \\ 
$\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{ok-mg-statement}}\,({\it{stmt\/}}, {\it{r-cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\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{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} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\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{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resource-errorp}}\,({\rm{mg-meaning-r}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{resource-errorp}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{p-step}}\,({\rm{p-state}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{pc}}, {\rm{cons}}\,({\it{subr\/}}, {\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} $+$ {\tt{1}}))\index{tag}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\rm{push}}\,(\=\+{\rm{value}}\,({\rm{if-condition}}\,({\it{stmt\/}})\index{if-condition}, {\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}}, {\rm{cons}}\,({\it{subr\/}}, {\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length} $+$ {\tt{2}}))\index{tag}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\rm{push}}\,(\=\+{\rm{rget}}\,(\=\+{\rm{untag}}\,({\rm{value}}\,(\=\+{\rm{if-condition}}\,({\it{stmt\/}})\index{if-condition}, \\ 
{\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}:  boolean-value-maps-down \\ \index{boolean-value-maps-down}
\=\+(\=\+{\rm{boolean-identifierp}}\,({\it{b\/}}, {\it{mg-vars\/}})\index{boolean-identifierp} \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,({\it{mg-vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\it{mg-vars\/}})\index{mg-alistp} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\it{bindings\/}}, {\it{mg-vars\/}})\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\it{mg-vars\/}})\index{all-cars-unique})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{rget}}\,(\=\+{\rm{untag}}\,({\rm{value}}\,({\it{b\/}}, {\it{bindings\/}})\index{value})\index{untag}, \\ 
{\rm{map-down-values}}\,({\it{mg-vars\/}}, {\it{bindings\/}}, {\it{temp-stk\/}})\index{map-down-values})\-\index{rget} \\ 
$=$$\;\;\;\;${\rm{mg-to-p-simple-literal}}\,({\rm{get-m-value}}\,({\it{b\/}}, {\it{mg-vars\/}})\index{get-m-value})\index{mg-to-p-simple-literal})\-\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  if-find-labelp-lemma1 \\ \index{if-find-labelp-lemma1}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{if-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{r-cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{ok-translation-parameters}}\,({\it{cinfo\/}}, {\it{t-cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}}, {\it{code2\/}})\index{ok-translation-parameters})\- \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{find-labelp}}\,(\=\+{\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}, \\ 
{\rm{code}}\,({\rm{translate}}\,(\=\+{\rm{make-cinfo}}\,(\=\+{\rm{append}}\,(\=\+{\rm{code}}\,({\it{cinfo\/}})\index{code}, \\ 
{\rm{list}}\,(\=\+{\rm{list}}\,(\=\+{\tt{'}}{\tt{push-local}}, \\ 
{\rm{if-condition}}\,({\it{stmt\/}})\index{if-condition})\-, \\ 
{\tt{'}}{\tt{(}}\=\+{\tt{fetch-temp-stk}}{\tt{)}}\-, \\ 
{\rm{list}}\,(\=\+{\tt{'}}{\tt{test-bool-and-jump}}, \\ 
{\tt{'}}{\tt{false}}, \\ 
{\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt})\-)\-)\-, \\ 
{\rm{label-alist}}\,({\it{cinfo\/}})\index{label-alist}, \\ 
$1\;+$ ($1\;+$ {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}))\-\index{make-cinfo}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{if-true-branch}}\,({\it{stmt\/}})\index{if-true-branch}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code})\-\index{find-labelp})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  if-initial-step3-false-test \\ \index{if-initial-step3-false-test}
\=\+(\=\+({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{if-mg}}) \\ 
$\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{ok-mg-statement}}\,({\it{stmt\/}}, {\it{r-cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\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{ok-mg-statep}}\,({\it{mg-state\/}}, {\it{r-cond-list\/}})\index{ok-mg-statep} \\ 
$\wedge$$\;\;\;\;${\rm{ok-translation-parameters}}\,({\it{cinfo\/}}, {\it{t-cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}}, {\it{code2\/}})\index{ok-translation-parameters} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\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{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\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$$\;\;\;\;$($\neg$ {\rm{resource-errorp}}\,({\rm{mg-meaning-r}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{resource-errorp}) \\ 
$\wedge$$\;\;\;\;${\rm{mg-expression-falsep}}\,({\rm{if-condition}}\,({\it{stmt\/}})\index{if-condition}, {\it{mg-state\/}})\index{mg-expression-falsep})\- \\ 
$\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{rget}}\,(\=\+{\rm{untag}}\,({\rm{value}}\,(\=\+{\rm{if-condition}}\,({\it{stmt\/}})\index{if-condition}, \\ 
{\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}}, \\ 
{\rm{cons}}\,(\=\+{\it{subr\/}}, \\ 
\=\+{\rm{length}}\,({\rm{code}}\,({\rm{translate}}\,(\=\+{\rm{make-cinfo}}\,(\=\+{\rm{append}}\,(\=\+{\rm{code}}\,({\it{cinfo\/}})\index{code}, \\ 
{\rm{list}}\,(\=\+{\rm{list}}\,(\=\+{\tt{'}}{\tt{push-local}}, \\ 
{\rm{if-condition}}\,({\it{stmt\/}})\index{if-condition})\-, \\ 
{\tt{'}}{\tt{(}}\=\+{\tt{fetch-temp-stk}}{\tt{)}}\-, \\ 
{\rm{list}}\,(\=\+{\tt{'}}{\tt{test-bool-and-jump}}, \\ 
{\tt{'}}{\tt{false}}, \\ 
{\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt})\-)\-)\-, \\ 
{\rm{label-alist}}\,({\it{cinfo\/}})\index{label-alist}, \\ 
$1\;+$ ($1\;+$ {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}))\-\index{make-cinfo}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{if-true-branch}}\,({\it{stmt\/}})\index{if-true-branch}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code})\index{length} \\ 
$+$$\;\;\;\;${\tt{1}}\-)\-)\-\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}}, \\ 
{\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}:  if-initial-step4-false-test \\ \index{if-initial-step4-false-test}
\=\+(\=\+({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{if-mg}}) \\ 
$\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{ok-mg-statement}}\,({\it{stmt\/}}, {\it{r-cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\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{ok-mg-statep}}\,({\it{mg-state\/}}, {\it{r-cond-list\/}})\index{ok-mg-statep} \\ 
$\wedge$$\;\;\;\;${\rm{ok-translation-parameters}}\,({\it{cinfo\/}}, {\it{t-cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}}, {\it{code2\/}})\index{ok-translation-parameters} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\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{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\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$$\;\;\;\;$($\neg$ {\rm{resource-errorp}}\,({\rm{mg-meaning-r}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{resource-errorp}) \\ 
$\wedge$$\;\;\;\;${\rm{mg-expression-falsep}}\,({\rm{if-condition}}\,({\it{stmt\/}})\index{if-condition}, {\it{mg-state\/}})\index{mg-expression-falsep})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{p-step}}\,({\rm{p-state}}\,(\=\+{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,(\=\+{\it{subr\/}}, \\ 
\=\+{\rm{length}}\,({\rm{code}}\,({\rm{translate}}\,(\=\+{\rm{make-cinfo}}\,(\=\+{\rm{append}}\,(\=\+{\rm{code}}\,({\it{cinfo\/}})\index{code}, \\ 
{\rm{list}}\,(\=\+{\rm{list}}\,(\=\+{\tt{'}}{\tt{push-local}}, \\ 
{\rm{if-condition}}\,({\it{stmt\/}})\index{if-condition})\-, \\ 
{\tt{'}}{\tt{(}}\=\+{\tt{fetch-temp-stk}}{\tt{)}}\-, \\ 
{\rm{list}}\,(\=\+{\tt{'}}{\tt{test-bool-and-jump}}, \\ 
{\tt{'}}{\tt{false}}, \\ 
{\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt})\-)\-)\-, \\ 
{\rm{label-alist}}\,({\it{cinfo\/}})\index{label-alist}, \\ 
$1\;+$ ($1\;+$ {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}))\-\index{make-cinfo}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{if-true-branch}}\,({\it{stmt\/}})\index{if-true-branch}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code})\index{length} \\ 
$+$$\;\;\;\;${\tt{1}}\-)\-)\-\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}}, \\ 
{\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{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}}\,({\rm{add-code}}\,(\=\+{\rm{translate}}\,(\=\+{\rm{make-cinfo}}\,(\=\+{\rm{append}}\,(\=\+{\rm{code}}\,({\it{cinfo\/}})\index{code}, \\ 
{\rm{list}}\,(\=\+{\rm{list}}\,(\=\+{\tt{'}}{\tt{push-local}}, \\ 
{\rm{if-condition}}\,({\it{stmt\/}})\index{if-condition})\-, \\ 
{\tt{'}}{\tt{(}}\=\+{\tt{fetch-temp-stk}}{\tt{)}}\-, \\ 
{\rm{list}}\,(\=\+{\tt{'}}{\tt{test-bool-and-jump}}, \\ 
{\tt{'}}{\tt{false}}, \\ 
{\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt})\-)\-)\-, \\ 
{\rm{label-alist}}\,({\it{cinfo\/}})\index{label-alist}, \\ 
$1\;+$ ($1\;+$ {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}))\-\index{make-cinfo}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{if-true-branch}}\,({\it{stmt\/}})\index{if-true-branch}, \\ 
{\it{proc-list\/}})\-\index{translate}, \\ 
{\rm{list}}\,(\=\+{\rm{list}}\,(\=\+{\tt{'}}{\tt{jump}}, \\ 
$1\;+$ {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{dl}}, \\ 
{\rm{cons}}\,(\=\+{\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}, \\ 
{\tt{'}}{\tt{(}}\=\+{\tt{nil}} \\ 
{\tt{(}}\=\+{\tt{no-op}}{\tt{)}}\-{\tt{)}}\-)\-)\-)\-)\-\index{add-code})\index{code})\index{length})\-)\-\index{tag}, \\ 
{\it{t-cond-list\/}})\-\index{map-down})\-\-
\end{tabbing}

%\item 
\begin{verbatim}


(prove-lemma if-step-normal-false-state2-equals-final (rewrite)
      (implies
       (and (not (zerop n))
	    (equal (car stmt) 'if-mg)
	    (not (resources-inadequatep stmt proc-list
					(list (length temp-stk)
					      (p-ctrl-stk-size ctrl-stk))))
	    (ok-mg-statement stmt r-cond-list name-alist proc-list)
	    (mg-vars-list-ok-in-p-state (mg-alist mg-state)
					(bindings (top ctrl-stk))
					temp-stk)
	    (ok-mg-statep mg-state r-cond-list)
            (ok-translation-parameters cinfo t-cond-list stmt proc-list code2)
            (signatures-match (mg-alist mg-state) name-alist)
	    (ok-mg-def-plistp proc-list)
	    (all-cars-unique (mg-alist mg-state))
	    (equal (code (translate-def-body (assoc subr proc-list)
					     proc-list))
		   (append (code (translate cinfo t-cond-list stmt proc-list))
			   code2))
	    (user-defined-procp subr proc-list)
	    (normal mg-state)
	    (no-p-aliasing (bindings (top ctrl-stk)) (mg-alist mg-state))
	    (not (resource-errorp (mg-meaning-r stmt proc-list mg-state n
						(list (length temp-stk)
						      (p-ctrl-stk-size ctrl-stk)))))
	    (MG-EXPRESSION-FALSEP (IF-CONDITION STMT) MG-STATE)
            (normal (mg-meaning-r (if-false-branch stmt) proc-list mg-state (sub1 n)
				  (LIST (LENGTH TEMP-STK)
					(P-CTRL-STK-SIZE CTRL-STK)))))
       (equal 
	(p-step
	  (P-STATE
	   (TAG 'PC
		(CONS SUBR
		      (IF
		       (NORMAL (MG-MEANING-R (IF-FALSE-BRANCH STMT)
					     PROC-LIST MG-STATE
					     (SUB1 N)
					     (LIST (LENGTH TEMP-STK)
						   (P-CTRL-STK-SIZE CTRL-STK))))
		       (LENGTH
			(CODE
			 (TRANSLATE
			  (ADD-CODE
			   (TRANSLATE (MAKE-CINFO (APPEND (CODE CINFO)
							  (LIST (LIST 'PUSH-LOCAL
								      (IF-CONDITION STMT))
								'(FETCH-TEMP-STK)
								(LIST 'TEST-BOOL-AND-JUMP
								      'FALSE
								      (LABEL-CNT CINFO))))
						  (LABEL-ALIST CINFO)
						  (ADD1 (ADD1 (LABEL-CNT CINFO))))
				      T-COND-LIST
				      (IF-TRUE-BRANCH STMT)
				      PROC-LIST)
			   (LIST (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
				 (CONS 'DL
				       (CONS (LABEL-CNT CINFO)
					     '(NIL (NO-OP))))))
			  T-COND-LIST
			  (IF-FALSE-BRANCH STMT)
			  PROC-LIST)))
		       (FIND-LABEL
			(FETCH-LABEL
			 (CC (MG-MEANING-R (IF-FALSE-BRANCH STMT)
					   PROC-LIST MG-STATE
					   (SUB1 N)
					   (LIST (LENGTH TEMP-STK)
						 (P-CTRL-STK-SIZE CTRL-STK))))
			 (LABEL-ALIST
			  (TRANSLATE
			   (ADD-CODE
			    (TRANSLATE (MAKE-CINFO (APPEND (CODE CINFO)
							   (LIST (LIST 'PUSH-LOCAL
								       (IF-CONDITION STMT))
								 '(FETCH-TEMP-STK)
								 (LIST 'TEST-BOOL-AND-JUMP
								       'FALSE
								       (LABEL-CNT CINFO))))
						   (LABEL-ALIST CINFO)
						   (ADD1 (ADD1 (LABEL-CNT CINFO))))
				       T-COND-LIST
				       (IF-TRUE-BRANCH STMT)
				       PROC-LIST)
			    (LIST (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
				  (CONS 'DL
					(CONS (LABEL-CNT CINFO)
					      '(NIL (NO-OP))))))
			   T-COND-LIST
			   (IF-FALSE-BRANCH STMT)
			   PROC-LIST)))
			(APPEND
			 (CODE
			  (TRANSLATE
			   (ADD-CODE
			    (TRANSLATE (MAKE-CINFO (APPEND (CODE CINFO)
							   (LIST (LIST 'PUSH-LOCAL
								       (IF-CONDITION STMT))
								 '(FETCH-TEMP-STK)
								 (LIST 'TEST-BOOL-AND-JUMP
								       'FALSE
								       (LABEL-CNT CINFO))))
						   (LABEL-ALIST CINFO)
						   (ADD1 (ADD1 (LABEL-CNT CINFO))))
				       T-COND-LIST
				       (IF-TRUE-BRANCH STMT)
				       PROC-LIST)
			    (LIST (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
				  (CONS 'DL
					(CONS (LABEL-CNT CINFO)
					      '(NIL (NO-OP))))))
			   T-COND-LIST
			   (IF-FALSE-BRANCH STMT)
			   PROC-LIST))
			 (CONS (CONS 'DL
				     (CONS (ADD1 (LABEL-CNT CINFO))
					   '(NIL (NO-OP))))
			       CODE2))))))
	   CTRL-STK
	   (MAP-DOWN-VALUES
	    (MG-ALIST (MG-MEANING-R (IF-FALSE-BRANCH STMT)
				    PROC-LIST MG-STATE
				    (SUB1 N)
				    (LIST (LENGTH TEMP-STK)
					  (P-CTRL-STK-SIZE CTRL-STK))))
	    (BINDINGS (TOP CTRL-STK))
	    TEMP-STK)
	   (TRANSLATE-PROC-LIST PROC-LIST)
	   (LIST
	    (LIST 'C-C
		  (MG-COND-TO-P-NAT (CC (MG-MEANING-R (IF-FALSE-BRANCH STMT)
						      PROC-LIST MG-STATE
						      (SUB1 N)
						      (LIST (LENGTH TEMP-STK)
							    (P-CTRL-STK-SIZE CTRL-STK))))
				    T-COND-LIST)))
	   (MG-MAX-CTRL-STK-SIZE)
	   (MG-MAX-TEMP-STK-SIZE)
	   (MG-WORD-SIZE)
	   'RUN))
      (P-STATE
       (TAG 'PC
	    (CONS SUBR
		  (IF
		   (NORMAL (MG-MEANING-R STMT PROC-LIST MG-STATE N
					 (LIST (LENGTH TEMP-STK)
					       (P-CTRL-STK-SIZE CTRL-STK))))
		   (LENGTH (CODE (TRANSLATE CINFO T-COND-LIST STMT PROC-LIST)))
		   (FIND-LABEL
		    (FETCH-LABEL (CC (MG-MEANING-R STMT PROC-LIST MG-STATE N
						   (LIST (LENGTH TEMP-STK)
							 (P-CTRL-STK-SIZE CTRL-STK))))
				 (LABEL-ALIST (TRANSLATE CINFO T-COND-LIST STMT
							 PROC-LIST)))
		    (APPEND (CODE (TRANSLATE CINFO T-COND-LIST STMT PROC-LIST))
			    CODE2)))))
       CTRL-STK
       (MAP-DOWN-VALUES (MG-ALIST (MG-MEANING-R STMT PROC-LIST MG-STATE N
						(LIST (LENGTH TEMP-STK)
						      (P-CTRL-STK-SIZE CTRL-STK))))
			(BINDINGS (TOP CTRL-STK))
			TEMP-STK)
       (TRANSLATE-PROC-LIST PROC-LIST)
       (LIST
	(LIST 'C-C
	      (MG-COND-TO-P-NAT (CC (MG-MEANING-R STMT PROC-LIST MG-STATE N
						  (LIST (LENGTH TEMP-STK)
							(P-CTRL-STK-SIZE CTRL-STK))))
				T-COND-LIST)))
       (MG-MAX-CTRL-STK-SIZE)
       (MG-MAX-TEMP-STK-SIZE)
       (MG-WORD-SIZE)
       'RUN)))
   ((INSTRUCTIONS 
     PROMOTE (DIVE 1) X (S LEMMAS) (DIVE 1 1 2)
     (REWRITE TRANSLATE-DEF-BODY-REWRITE) (DIVE 1 1) (REWRITE IF-TRANSLATION-2)
     UP UP (S LEMMAS) UP (S-PROP ADD-CODE) (S LEMMAS) (REWRITE GET-LENGTH-CAR)
     S UP X UP X (DIVE 1) X UP S-PROP X TOP (S LEMMAS) (S-PROP ADD-CODE) PROVE)))
\end{verbatim}


%\item 
\begin{verbatim}


(prove-lemma if-non-normal-false-state2-equals-final (rewrite)
      (implies
       (and (not (zerop n))
	    (equal (car stmt) 'if-mg)
	    (not (resources-inadequatep stmt proc-list
					(list (length temp-stk)
					      (p-ctrl-stk-size ctrl-stk))))
	    (ok-mg-statement stmt r-cond-list name-alist proc-list)
	    (mg-vars-list-ok-in-p-state (mg-alist mg-state)
					(bindings (top ctrl-stk))
					temp-stk)
	    (ok-mg-statep mg-state r-cond-list)
            (ok-translation-parameters cinfo t-cond-list stmt proc-list code2)
            (signatures-match (mg-alist mg-state) name-alist)
	    (ok-mg-def-plistp proc-list)
	    (all-cars-unique (mg-alist mg-state))
	    (equal (code (translate-def-body (assoc subr proc-list)
					     proc-list))
		   (append (code (translate cinfo t-cond-list stmt proc-list))
			   code2))
	    (user-defined-procp subr proc-list)
	    (normal mg-state)
	    (no-p-aliasing (bindings (top ctrl-stk)) (mg-alist mg-state))
	    (not (resource-errorp (mg-meaning-r stmt proc-list mg-state n
						(list (length temp-stk)
						      (p-ctrl-stk-size ctrl-stk)))))
	    (MG-EXPRESSION-FALSEP (IF-CONDITION STMT) MG-STATE)
            (not (normal (mg-meaning-r (if-false-branch stmt) proc-list mg-state (sub1 n)
				  (LIST (LENGTH TEMP-STK)
					(P-CTRL-STK-SIZE CTRL-STK))))))
       (equal 
	  (P-STATE
	   (TAG 'PC
		(CONS SUBR
		      (IF
		       (NORMAL (MG-MEANING-R (IF-FALSE-BRANCH STMT)
					     PROC-LIST MG-STATE
					     (SUB1 N)
					     (LIST (LENGTH TEMP-STK)
						   (P-CTRL-STK-SIZE CTRL-STK))))
		       (LENGTH
			(CODE
			 (TRANSLATE
			  (ADD-CODE
			   (TRANSLATE (MAKE-CINFO (APPEND (CODE CINFO)
							  (LIST (LIST 'PUSH-LOCAL
								      (IF-CONDITION STMT))
								'(FETCH-TEMP-STK)
								(LIST 'TEST-BOOL-AND-JUMP
								      'FALSE
								      (LABEL-CNT CINFO))))
						  (LABEL-ALIST CINFO)
						  (ADD1 (ADD1 (LABEL-CNT CINFO))))
				      T-COND-LIST
				      (IF-TRUE-BRANCH STMT)
				      PROC-LIST)
			   (LIST (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
				 (CONS 'DL
				       (CONS (LABEL-CNT CINFO)
					     '(NIL (NO-OP))))))
			  T-COND-LIST
			  (IF-FALSE-BRANCH STMT)
			  PROC-LIST)))
		       (FIND-LABEL
			(FETCH-LABEL
			 (CC (MG-MEANING-R (IF-FALSE-BRANCH STMT)
					   PROC-LIST MG-STATE
					   (SUB1 N)
					   (LIST (LENGTH TEMP-STK)
						 (P-CTRL-STK-SIZE CTRL-STK))))
			 (LABEL-ALIST
			  (TRANSLATE
			   (ADD-CODE
			    (TRANSLATE (MAKE-CINFO (APPEND (CODE CINFO)
							   (LIST (LIST 'PUSH-LOCAL
								       (IF-CONDITION STMT))
								 '(FETCH-TEMP-STK)
								 (LIST 'TEST-BOOL-AND-JUMP
								       'FALSE
								       (LABEL-CNT CINFO))))
						   (LABEL-ALIST CINFO)
						   (ADD1 (ADD1 (LABEL-CNT CINFO))))
				       T-COND-LIST
				       (IF-TRUE-BRANCH STMT)
				       PROC-LIST)
			    (LIST (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
				  (CONS 'DL
					(CONS (LABEL-CNT CINFO)
					      '(NIL (NO-OP))))))
			   T-COND-LIST
			   (IF-FALSE-BRANCH STMT)
			   PROC-LIST)))
			(APPEND
			 (CODE
			  (TRANSLATE
			   (ADD-CODE
			    (TRANSLATE (MAKE-CINFO (APPEND (CODE CINFO)
							   (LIST (LIST 'PUSH-LOCAL
								       (IF-CONDITION STMT))
								 '(FETCH-TEMP-STK)
								 (LIST 'TEST-BOOL-AND-JUMP
								       'FALSE
								       (LABEL-CNT CINFO))))
						   (LABEL-ALIST CINFO)
						   (ADD1 (ADD1 (LABEL-CNT CINFO))))
				       T-COND-LIST
				       (IF-TRUE-BRANCH STMT)
				       PROC-LIST)
			    (LIST (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
				  (CONS 'DL
					(CONS (LABEL-CNT CINFO)
					      '(NIL (NO-OP))))))
			   T-COND-LIST
			   (IF-FALSE-BRANCH STMT)
			   PROC-LIST))
			 (CONS (CONS 'DL
				     (CONS (ADD1 (LABEL-CNT CINFO))
					   '(NIL (NO-OP))))
			       CODE2))))))
	   CTRL-STK
	   (MAP-DOWN-VALUES
	    (MG-ALIST (MG-MEANING-R (IF-FALSE-BRANCH STMT)
				    PROC-LIST MG-STATE
				    (SUB1 N)
				    (LIST (LENGTH TEMP-STK)
					  (P-CTRL-STK-SIZE CTRL-STK))))
	    (BINDINGS (TOP CTRL-STK))
	    TEMP-STK)
	   (TRANSLATE-PROC-LIST PROC-LIST)
	   (LIST
	    (LIST 'C-C
		  (MG-COND-TO-P-NAT (CC (MG-MEANING-R (IF-FALSE-BRANCH STMT)
						      PROC-LIST MG-STATE
						      (SUB1 N)
						      (LIST (LENGTH TEMP-STK)
							    (P-CTRL-STK-SIZE CTRL-STK))))
				    T-COND-LIST)))
	   (MG-MAX-CTRL-STK-SIZE)
	   (MG-MAX-TEMP-STK-SIZE)
	   (MG-WORD-SIZE)
	   'RUN)
      (P-STATE
       (TAG 'PC
	    (CONS SUBR
		  (IF
		   (NORMAL (MG-MEANING-R STMT PROC-LIST MG-STATE N
					 (LIST (LENGTH TEMP-STK)
					       (P-CTRL-STK-SIZE CTRL-STK))))
		   (LENGTH (CODE (TRANSLATE CINFO T-COND-LIST STMT PROC-LIST)))
		   (FIND-LABEL
		    (FETCH-LABEL (CC (MG-MEANING-R STMT PROC-LIST MG-STATE N
						   (LIST (LENGTH TEMP-STK)
							 (P-CTRL-STK-SIZE CTRL-STK))))
				 (LABEL-ALIST (TRANSLATE CINFO T-COND-LIST STMT
							 PROC-LIST)))
		    (APPEND (CODE (TRANSLATE CINFO T-COND-LIST STMT PROC-LIST))
			    CODE2)))))
       CTRL-STK
       (MAP-DOWN-VALUES (MG-ALIST (MG-MEANING-R STMT PROC-LIST MG-STATE N
						(LIST (LENGTH TEMP-STK)
						      (P-CTRL-STK-SIZE CTRL-STK))))
			(BINDINGS (TOP CTRL-STK))
			TEMP-STK)
       (TRANSLATE-PROC-LIST PROC-LIST)
       (LIST
	(LIST 'C-C
	      (MG-COND-TO-P-NAT (CC (MG-MEANING-R STMT PROC-LIST MG-STATE N
						  (LIST (LENGTH TEMP-STK)
							(P-CTRL-STK-SIZE CTRL-STK))))
				T-COND-LIST)))
       (MG-MAX-CTRL-STK-SIZE)
       (MG-MAX-TEMP-STK-SIZE)
       (MG-WORD-SIZE)
       'RUN)))
   ((INSTRUCTIONS 
     PROMOTE S
     (= (MG-MEANING-R STMT PROC-LIST MG-STATE N (LIST (LENGTH TEMP-STK) 
						      (P-CTRL-STK-SIZE CTRL-STK)))
	(MG-MEANING-R (IF-FALSE-BRANCH STMT) PROC-LIST MG-STATE (SUB1 N)
		      (LIST (LENGTH TEMP-STK) (P-CTRL-STK-SIZE CTRL-STK))) 0)
     SPLIT S S (S LEMMAS) (DIVE 2 2 2 1) (= F) TOP S PROVE (DIVE 1) 
     (REWRITE IF-MEANING-R-2) TOP S)))
\end{verbatim}



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

\addvspace{18pt}

\noindent{\sc Event}:   Disable cddr-length-plistp-2.

\addvspace{18pt}

\noindent{\sc Event}:   Disable simple-typed-literalp-ok-valuep.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  boolean-identifierp-not-false-expressionp \\ \index{boolean-identifierp-not-false-e!xpressionp}
\=\+(\=\+{\rm{boolean-identifierp}}\,({\it{b\/}}, {\it{mg-vars\/}})\index{boolean-identifierp} \\ 
$\wedge$$\;\;\;\;$({\rm{get-m-value}}\,({\it{b\/}}, {\it{mg-vars\/}})\index{get-m-value} $\not=$ {\tt{'}}{\tt{(}}{\tt{boolean-mg}}{\tt{ }}{\tt{false-mg}}{\tt{)}}) \\ 
$\wedge$$\;\;\;\;${\rm{mg-alistp}}\,({\it{mg-vars\/}})\index{mg-alistp})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{get-m-value}}\,({\it{b\/}}, {\it{mg-vars\/}})\index{get-m-value} $=$ {\tt{'}}{\tt{(}}{\tt{boolean-mg}}{\tt{ }}{\tt{true-mg}}{\tt{)}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  if-initial-step3-true-test-equals-true-state1 \\ \index{if-initial-step3-true-test-equa!ls-true-state1}
\=\+(\=\+({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{if-mg}}) \\ 
$\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{ok-mg-statement}}\,({\it{stmt\/}}, {\it{r-cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\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{ok-mg-statep}}\,({\it{mg-state\/}}, {\it{r-cond-list\/}})\index{ok-mg-statep} \\ 
$\wedge$$\;\;\;\;${\rm{ok-translation-parameters}}\,({\it{cinfo\/}}, {\it{t-cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}}, {\it{code2\/}})\index{ok-translation-parameters} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\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{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\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$$\;\;\;\;$($\neg$ {\rm{resource-errorp}}\,({\rm{mg-meaning-r}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{resource-errorp}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{mg-expression-falsep}}\,({\rm{if-condition}}\,({\it{stmt\/}})\index{if-condition}, {\it{mg-state\/}})\index{mg-expression-falsep}))\- \\ 
$\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{rget}}\,(\=\+{\rm{untag}}\,({\rm{value}}\,(\=\+{\rm{if-condition}}\,({\it{stmt\/}})\index{if-condition}, \\ 
{\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{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}}\,({\rm{make-cinfo}}\,(\=\+{\rm{append}}\,(\=\+{\rm{code}}\,({\it{cinfo\/}})\index{code}, \\ 
{\rm{list}}\,(\=\+{\rm{list}}\,(\=\+{\tt{'}}{\tt{push-local}}, \\ 
{\rm{if-condition}}\,({\it{stmt\/}})\index{if-condition})\-, \\ 
{\tt{'}}{\tt{(}}\=\+{\tt{fetch-temp-stk}}{\tt{)}}\-, \\ 
{\rm{list}}\,(\=\+{\tt{'}}{\tt{test-bool-and-jump}}, \\ 
{\tt{'}}{\tt{false}}, \\ 
{\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt})\-)\-)\-, \\ 
{\rm{label-alist}}\,({\it{cinfo\/}})\index{label-alist}, \\ 
$1\;+$ ($1\;+$ {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}))\-\index{make-cinfo})\index{code})\index{length})\-)\-\index{tag}, \\ 
{\it{t-cond-list\/}})\-\index{map-down})\-\-
\end{tabbing}

%\item 
\begin{verbatim}


(prove-lemma if-nonnormal-true-state2-equals-final (rewrite)
      (implies
       (and (not (zerop n))
	    (equal (car stmt) 'if-mg)
	    (not (resources-inadequatep stmt proc-list
					(list (length temp-stk)
					      (p-ctrl-stk-size ctrl-stk))))
	    (ok-mg-statement stmt r-cond-list name-alist proc-list)
	    (mg-vars-list-ok-in-p-state (mg-alist mg-state)
					(bindings (top ctrl-stk))
					temp-stk)
	    (ok-mg-statep mg-state r-cond-list)
            (ok-translation-parameters cinfo t-cond-list stmt proc-list code2)
            (signatures-match (mg-alist mg-state) name-alist)
	    (ok-mg-def-plistp proc-list)
	    (all-cars-unique (mg-alist mg-state))
	    (equal (code (translate-def-body (assoc subr proc-list)
					     proc-list))
		   (append (code (translate cinfo t-cond-list stmt proc-list))
			   code2))
	    (user-defined-procp subr proc-list)
	    (normal mg-state)
	    (no-p-aliasing (bindings (top ctrl-stk)) (mg-alist mg-state))
	    (not (resource-errorp (mg-meaning-r stmt proc-list mg-state n
						(list (length temp-stk)
						      (p-ctrl-stk-size ctrl-stk)))))
	    (not (MG-EXPRESSION-FALSEP (IF-CONDITION STMT) MG-STATE))
            (not (normal (mg-meaning-r (if-true-branch stmt) proc-list mg-state (sub1 n)
				       (LIST (LENGTH TEMP-STK)
					     (P-CTRL-STK-SIZE CTRL-STK))))))
       (equal 
	 (P-STATE
	  (TAG 'PC
	       (CONS SUBR
		     (IF
		      (NORMAL (MG-MEANING-R (IF-TRUE-BRANCH STMT)
					    PROC-LIST MG-STATE
					    (SUB1 N)
					    (LIST (LENGTH TEMP-STK)
						  (P-CTRL-STK-SIZE CTRL-STK))))
		      (LENGTH
		       (CODE (TRANSLATE (MAKE-CINFO (APPEND (CODE CINFO)
							    (LIST (LIST 'PUSH-LOCAL
									(IF-CONDITION STMT))
								  '(FETCH-TEMP-STK)
								  (LIST 'TEST-BOOL-AND-JUMP
									'FALSE
									(LABEL-CNT CINFO))))
						    (LABEL-ALIST CINFO)
						    (ADD1 (ADD1 (LABEL-CNT CINFO))))
					T-COND-LIST
					(IF-TRUE-BRANCH STMT)
					PROC-LIST)))
		      (FIND-LABEL
		       (FETCH-LABEL
			(CC (MG-MEANING-R (IF-TRUE-BRANCH STMT)
					  PROC-LIST MG-STATE
					  (SUB1 N)
					  (LIST (LENGTH TEMP-STK)
						(P-CTRL-STK-SIZE CTRL-STK))))
			(LABEL-ALIST
			 (TRANSLATE (MAKE-CINFO (APPEND (CODE CINFO)
							(LIST (LIST 'PUSH-LOCAL
								    (IF-CONDITION STMT))
							      '(FETCH-TEMP-STK)
							      (LIST 'TEST-BOOL-AND-JUMP
								    'FALSE
								    (LABEL-CNT CINFO))))
						(LABEL-ALIST CINFO)
						(ADD1 (ADD1 (LABEL-CNT CINFO))))
				    T-COND-LIST
				    (IF-TRUE-BRANCH STMT)
				    PROC-LIST)))
		       (APPEND
			(CODE (TRANSLATE (MAKE-CINFO (APPEND (CODE CINFO)
							     (LIST (LIST 'PUSH-LOCAL
									 (IF-CONDITION STMT))
								   '(FETCH-TEMP-STK)
								   (LIST 'TEST-BOOL-AND-JUMP
									 'FALSE
									 (LABEL-CNT CINFO))))
						     (LABEL-ALIST CINFO)
						     (ADD1 (ADD1 (LABEL-CNT CINFO))))
					 T-COND-LIST
					 (IF-TRUE-BRANCH STMT)
					 PROC-LIST))
			(CONS
			 (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
			 (CONS
			  (CONS 'DL
				(CONS (LABEL-CNT CINFO)
				      '(NIL (NO-OP))))
			  (APPEND
			   (CODE
			    (TRANSLATE
			     (NULLIFY (TRANSLATE (MAKE-CINFO NIL
							     (LABEL-ALIST CINFO)
							     (ADD1 (ADD1 (LABEL-CNT CINFO))))
						 T-COND-LIST
						 (IF-TRUE-BRANCH STMT)
						 PROC-LIST))
			     T-COND-LIST
			     (IF-FALSE-BRANCH STMT)
			     PROC-LIST))
			   (CONS (CONS 'DL
				       (CONS (ADD1 (LABEL-CNT CINFO))
					     '(NIL (NO-OP))))
				 CODE2)))))))))
	  CTRL-STK
	  (MAP-DOWN-VALUES
	   (MG-ALIST (MG-MEANING-R (IF-TRUE-BRANCH STMT)
				   PROC-LIST MG-STATE
				   (SUB1 N)
				   (LIST (LENGTH TEMP-STK)
					 (P-CTRL-STK-SIZE CTRL-STK))))
	   (BINDINGS (TOP CTRL-STK))
	   TEMP-STK)
	  (TRANSLATE-PROC-LIST PROC-LIST)
	  (LIST
	   (LIST 'C-C
		 (MG-COND-TO-P-NAT (CC (MG-MEANING-R (IF-TRUE-BRANCH STMT)
						     PROC-LIST MG-STATE
						     (SUB1 N)
						     (LIST (LENGTH TEMP-STK)
							   (P-CTRL-STK-SIZE CTRL-STK))))
				   T-COND-LIST)))
	  (MG-MAX-CTRL-STK-SIZE)
	  (MG-MAX-TEMP-STK-SIZE)
	  (MG-WORD-SIZE)
	  'RUN)
     (P-STATE
      (TAG 'PC
	   (CONS SUBR
		 (IF
		  (NORMAL (MG-MEANING-R STMT PROC-LIST MG-STATE N
					(LIST (LENGTH TEMP-STK)
					      (P-CTRL-STK-SIZE CTRL-STK))))
		  (LENGTH (CODE (TRANSLATE CINFO T-COND-LIST STMT PROC-LIST)))
		  (FIND-LABEL
		   (FETCH-LABEL (CC (MG-MEANING-R STMT PROC-LIST MG-STATE N
						  (LIST (LENGTH TEMP-STK)
							(P-CTRL-STK-SIZE CTRL-STK))))
				(LABEL-ALIST (TRANSLATE CINFO T-COND-LIST STMT
							PROC-LIST)))
		   (APPEND (CODE (TRANSLATE CINFO T-COND-LIST STMT PROC-LIST))
			   CODE2)))))
      CTRL-STK
      (MAP-DOWN-VALUES (MG-ALIST (MG-MEANING-R STMT PROC-LIST MG-STATE N
					       (LIST (LENGTH TEMP-STK)
						     (P-CTRL-STK-SIZE CTRL-STK))))
		       (BINDINGS (TOP CTRL-STK))
		       TEMP-STK)
      (TRANSLATE-PROC-LIST PROC-LIST)
      (LIST
       (LIST 'C-C
	     (MG-COND-TO-P-NAT (CC (MG-MEANING-R STMT PROC-LIST MG-STATE N
						 (LIST (LENGTH TEMP-STK)
						       (P-CTRL-STK-SIZE CTRL-STK))))
			       T-COND-LIST)))
      (MG-MAX-CTRL-STK-SIZE)
      (MG-MAX-TEMP-STK-SIZE)
      (MG-WORD-SIZE)
      'RUN)))
 ((INSTRUCTIONS PROMOTE S
                (= (MG-MEANING-R STMT PROC-LIST MG-STATE N
                                 (LIST (LENGTH TEMP-STK)
                                       (P-CTRL-STK-SIZE CTRL-STK)))
                   (MG-MEANING-R (IF-TRUE-BRANCH STMT)
                                 PROC-LIST MG-STATE
                                 (SUB1 N)
                                 (LIST (LENGTH TEMP-STK)
                                       (P-CTRL-STK-SIZE CTRL-STK)))
                   0)
                S
                (S LEMMAS)
                (DIVE 2 2 2 1)
                (= F)
                TOP S-PROP
                (DIVE 2 2 2 2 1)
                (REWRITE NEW-CODE-APPENDED-TO-OLD1)
                TOP
                (S-PROP ADD-CODE NULLIFY)
                S
                (S LEMMAS)
                (DIVE 2 2 2 2 2 2 2 1 1 1 3)
                (REWRITE CODE-DOESNT-AFFECT-OTHER-FIELDS)
                TOP
                (S-PROP NULLIFY)
                (S LEMMAS)
                X
                (S LEMMAS)
                (DIVE 1)
                (REWRITE IF-MEANING-R-2)
                S TOP S)))
\end{verbatim}


\begin{tabbing}{\sc Theorem}:  if-find-labelp-lemma3 \\ \index{if-find-labelp-lemma3}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{if-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{r-cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{ok-translation-parameters}}\,({\it{cinfo\/}}, {\it{t-cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}}, {\it{code2\/}})\index{ok-translation-parameters})\- \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{find-labelp}}\,(\=\+$1\;+$ {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}, \\ 
{\rm{code}}\,({\rm{translate}}\,(\=\+{\rm{make-cinfo}}\,(\=\+{\rm{append}}\,(\=\+{\rm{code}}\,({\it{cinfo\/}})\index{code}, \\ 
{\rm{list}}\,(\=\+{\rm{list}}\,(\=\+{\tt{'}}{\tt{push-local}}, \\ 
{\rm{if-condition}}\,({\it{stmt\/}})\index{if-condition})\-, \\ 
{\tt{'}}{\tt{(}}\=\+{\tt{fetch-temp-stk}}{\tt{)}}\-, \\ 
{\rm{list}}\,(\=\+{\tt{'}}{\tt{test-bool-and-jump}}, \\ 
{\tt{'}}{\tt{false}}, \\ 
{\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt})\-)\-)\-, \\ 
{\rm{label-alist}}\,({\it{cinfo\/}})\index{label-alist}, \\ 
$1\;+$ ($1\;+$ {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}))\-\index{make-cinfo}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{if-true-branch}}\,({\it{stmt\/}})\index{if-true-branch}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code})\-\index{find-labelp})\-
\end{tabbing}

%\item 
\begin{verbatim}


(prove-lemma if-normal-true-state2-step1 (rewrite)
      (implies
       (and (not (zerop n))
	    (equal (car stmt) 'if-mg)
	    (not (resources-inadequatep stmt proc-list
					(list (length temp-stk)
					      (p-ctrl-stk-size ctrl-stk))))
	    (ok-mg-statement stmt r-cond-list name-alist proc-list)
	    (mg-vars-list-ok-in-p-state (mg-alist mg-state)
					(bindings (top ctrl-stk))
					temp-stk)
	    (ok-mg-statep mg-state r-cond-list)
            (ok-translation-parameters cinfo t-cond-list stmt proc-list code2)
            (signatures-match (mg-alist mg-state) name-alist)
	    (ok-mg-def-plistp proc-list)
	    (all-cars-unique (mg-alist mg-state))
	    (equal (code (translate-def-body (assoc subr proc-list)
					     proc-list))
		   (append (code (translate cinfo t-cond-list stmt proc-list))
			   code2))
	    (user-defined-procp subr proc-list)
	    (normal mg-state)
	    (no-p-aliasing (bindings (top ctrl-stk)) (mg-alist mg-state))
	    (not (resource-errorp (mg-meaning-r stmt proc-list mg-state n
						(list (length temp-stk)
						      (p-ctrl-stk-size ctrl-stk)))))
	    (not (MG-EXPRESSION-FALSEP (IF-CONDITION STMT) MG-STATE))
            (normal (mg-meaning-r (if-true-branch stmt) proc-list mg-state (sub1 n)
				  (LIST (LENGTH TEMP-STK)
					(P-CTRL-STK-SIZE CTRL-STK)))))
       (equal 
         (p-step
	  (P-STATE
	   (TAG 'PC
		(CONS SUBR
		      (IF
		       (NORMAL (MG-MEANING-R (IF-TRUE-BRANCH STMT)
					     PROC-LIST MG-STATE
					     (SUB1 N)
					     (LIST (LENGTH TEMP-STK)
						   (P-CTRL-STK-SIZE CTRL-STK))))
		       (LENGTH
			(CODE (TRANSLATE (MAKE-CINFO (APPEND (CODE CINFO)
							     (LIST (LIST 'PUSH-LOCAL
									 (IF-CONDITION STMT))
								   '(FETCH-TEMP-STK)
								   (LIST 'TEST-BOOL-AND-JUMP
									 'FALSE
									 (LABEL-CNT CINFO))))
						     (LABEL-ALIST CINFO)
						     (ADD1 (ADD1 (LABEL-CNT CINFO))))
					 T-COND-LIST
					 (IF-TRUE-BRANCH STMT)
					 PROC-LIST)))
		       (FIND-LABEL
			(FETCH-LABEL
			 (CC (MG-MEANING-R (IF-TRUE-BRANCH STMT)
					   PROC-LIST MG-STATE
					   (SUB1 N)
					   (LIST (LENGTH TEMP-STK)
						 (P-CTRL-STK-SIZE CTRL-STK))))
			 (LABEL-ALIST
			  (TRANSLATE (MAKE-CINFO (APPEND (CODE CINFO)
							 (LIST (LIST 'PUSH-LOCAL
								     (IF-CONDITION STMT))
							       '(FETCH-TEMP-STK)
							       (LIST 'TEST-BOOL-AND-JUMP
								     'FALSE
								     (LABEL-CNT CINFO))))
						 (LABEL-ALIST CINFO)
						 (ADD1 (ADD1 (LABEL-CNT CINFO))))
				     T-COND-LIST
				     (IF-TRUE-BRANCH STMT)
				     PROC-LIST)))
			(APPEND
			 (CODE (TRANSLATE (MAKE-CINFO (APPEND (CODE CINFO)
							      (LIST (LIST 'PUSH-LOCAL
									  (IF-CONDITION STMT))
								    '(FETCH-TEMP-STK)
								    (LIST 'TEST-BOOL-AND-JUMP
									  'FALSE
									  (LABEL-CNT CINFO))))
						      (LABEL-ALIST CINFO)
						      (ADD1 (ADD1 (LABEL-CNT CINFO))))
					  T-COND-LIST
					  (IF-TRUE-BRANCH STMT)
					  PROC-LIST))
			 (CONS
			  (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
			  (CONS
			   (CONS 'DL
				 (CONS (LABEL-CNT CINFO)
				       '(NIL (NO-OP))))
			   (APPEND
			    (CODE
			     (TRANSLATE
			      (NULLIFY (TRANSLATE (MAKE-CINFO NIL
							      (LABEL-ALIST CINFO)
							      (ADD1 (ADD1 (LABEL-CNT CINFO))))
						  T-COND-LIST
						  (IF-TRUE-BRANCH STMT)
						  PROC-LIST))
			      T-COND-LIST
			      (IF-FALSE-BRANCH STMT)
			      PROC-LIST))
			    (CONS (CONS 'DL
					(CONS (ADD1 (LABEL-CNT CINFO))
					      '(NIL (NO-OP))))
				  CODE2)))))))))
	   CTRL-STK
	   (MAP-DOWN-VALUES
	    (MG-ALIST (MG-MEANING-R (IF-TRUE-BRANCH STMT)
				    PROC-LIST MG-STATE
				    (SUB1 N)
				    (LIST (LENGTH TEMP-STK)
					  (P-CTRL-STK-SIZE CTRL-STK))))
	    (BINDINGS (TOP CTRL-STK))
	    TEMP-STK)
	   (TRANSLATE-PROC-LIST PROC-LIST)
	   (LIST
	    (LIST 'C-C
		  (MG-COND-TO-P-NAT (CC (MG-MEANING-R (IF-TRUE-BRANCH STMT)
						      PROC-LIST MG-STATE
						      (SUB1 N)
						      (LIST (LENGTH TEMP-STK)
							    (P-CTRL-STK-SIZE CTRL-STK))))
				    T-COND-LIST)))
	   (MG-MAX-CTRL-STK-SIZE)
	   (MG-MAX-TEMP-STK-SIZE)
	   (MG-WORD-SIZE)
	   'RUN))
      (P-STATE
       (TAG 'PC
	    (CONS SUBR
		  (PLUS
		   (LENGTH
		    (CODE (TRANSLATE (MAKE-CINFO (APPEND (CODE CINFO)
							 (LIST (LIST 'PUSH-LOCAL
								     (IF-CONDITION STMT))
							       '(FETCH-TEMP-STK)
							       (LIST 'TEST-BOOL-AND-JUMP
								     'FALSE
								     (LABEL-CNT CINFO))))
						 (LABEL-ALIST CINFO)
						 (ADD1 (ADD1 (LABEL-CNT CINFO))))
				     T-COND-LIST
				     (IF-TRUE-BRANCH STMT)
				     PROC-LIST)))
		   (ADD1
		    (ADD1
		     (LENGTH
		      (CODE
		       (TRANSLATE
			(MAKE-CINFO NIL
				    (LABEL-ALIST CINFO)
				    (LABEL-CNT (TRANSLATE (MAKE-CINFO NIL
								      (LABEL-ALIST CINFO)
								      (ADD1 (ADD1 (LABEL-CNT CINFO))))
							  T-COND-LIST
							  (IF-TRUE-BRANCH STMT)
							  PROC-LIST)))
			T-COND-LIST
			(IF-FALSE-BRANCH STMT)
			PROC-LIST))))))))
       CTRL-STK
       (MAP-DOWN-VALUES (MG-ALIST (MG-MEANING-R (IF-TRUE-BRANCH STMT)
						PROC-LIST MG-STATE
						(SUB1 N)
						(LIST (LENGTH TEMP-STK)
						      (P-CTRL-STK-SIZE CTRL-STK))))
			(BINDINGS (TOP CTRL-STK))
			TEMP-STK)
       (TRANSLATE-PROC-LIST PROC-LIST)
       (LIST
	(LIST 'C-C
	      (MG-COND-TO-P-NAT (CC (MG-MEANING-R (IF-TRUE-BRANCH STMT)
						  PROC-LIST MG-STATE
						  (SUB1 N)
						  (LIST (LENGTH TEMP-STK)
							(P-CTRL-STK-SIZE CTRL-STK))))
				T-COND-LIST)))
       (MG-MAX-CTRL-STK-SIZE)
       (MG-MAX-TEMP-STK-SIZE)
       (MG-WORD-SIZE)
       'RUN)))
 ((INSTRUCTIONS PROMOTE
                (DIVE 1)
                X
                (S LEMMAS)
                (DIVE 1 1 2)
                (REWRITE TRANSLATE-DEF-BODY-REWRITE)
                (REWRITE IF-CODE-REWRITE2)
                UP
                (REWRITE GET-LENGTH-CAR)
                S UP X UP X
                (DIVE 1)
                X UP S X
                (S LEMMAS)
                (DIVE 1 2 1)
                (REWRITE DEFINEDP-CAR-ASSOC)
                NX
                (DIVE 2)
                (REWRITE TRANSLATE-DEF-BODY-REWRITE)
                (REWRITE IF-CODE-REWRITE2)
                UP
                (REWRITE FIND-LABEL-APPEND)
                (DIVE 2)
                X
                (DIVE 1)
                X
                (DIVE 1)
                (REWRITE FIND-LABEL-APPEND)
                (DIVE 2)
                X UP
                (REWRITE PLUS-0-REWRITE2)
                S TOP
                (DIVE 1)
                TOP
                (S LEMMAS)
                (S-PROP NULLIFY)
                (S LEMMAS)
                S
                (DIVE 1)
                (REWRITE FIND-LABELP-MONOTONIC-LESSP)
                TOP S
                (S-PROP NULLIFY)
                S
                (REWRITE LABEL-CNT-MONOTONIC3)
                S PROVE
                (S LEMMAS)
                PROVE S
                (DIVE 1)
                (REWRITE IF-FIND-LABELP-LEMMA3)
                TOP S
                (REWRITE CAR-DEFINEDP-DEFINED-PROCP))))
\end{verbatim}


\begin{tabbing}{\sc Theorem}:  if-normal-true-state2-step2-equals-final \\ \index{if-normal-true-state2-step2-equ!als-final}
\=\+(\=\+({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{if-mg}}) \\ 
$\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{ok-mg-statement}}\,({\it{stmt\/}}, {\it{r-cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\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{ok-mg-statep}}\,({\it{mg-state\/}}, {\it{r-cond-list\/}})\index{ok-mg-statep} \\ 
$\wedge$$\;\;\;\;${\rm{ok-translation-parameters}}\,({\it{cinfo\/}}, {\it{t-cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}}, {\it{code2\/}})\index{ok-translation-parameters} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\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{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\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$$\;\;\;\;$($\neg$ {\rm{resource-errorp}}\,({\rm{mg-meaning-r}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{resource-errorp}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{mg-expression-falsep}}\,({\rm{if-condition}}\,({\it{stmt\/}})\index{if-condition}, {\it{mg-state\/}})\index{mg-expression-falsep}) \\ 
$\wedge$$\;\;\;\;${\rm{normal}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{if-true-branch}}\,({\it{stmt\/}})\index{if-true-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\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})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{p-step}}\,({\rm{p-state}}\,(\=\+{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,(\=\+{\it{subr\/}}, \\ 
\=\+{\rm{length}}\,({\rm{code}}\,({\rm{translate}}\,(\=\+{\rm{make-cinfo}}\,(\=\+{\rm{append}}\,(\=\+{\rm{code}}\,({\it{cinfo\/}})\index{code}, \\ 
{\rm{list}}\,(\=\+{\rm{list}}\,(\=\+{\tt{'}}{\tt{push-local}}, \\ 
{\rm{if-condition}}\,({\it{stmt\/}})\index{if-condition})\-, \\ 
{\tt{'}}{\tt{(}}\=\+{\tt{fetch-temp-stk}}{\tt{)}}\-, \\ 
{\rm{list}}\,(\=\+{\tt{'}}{\tt{test-bool-and-jump}}, \\ 
{\tt{'}}{\tt{false}}, \\ 
{\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt})\-)\-)\-, \\ 
{\rm{label-alist}}\,({\it{cinfo\/}})\index{label-alist}, \\ 
$1\;+$ ($1\;+$ {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}))\-\index{make-cinfo}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{if-true-branch}}\,({\it{stmt\/}})\index{if-true-branch}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code})\index{length} \\ 
$+$$\;\;\;\;$($1\;+$ ($1\;+$ {\rm{length}}\,({\rm{code}}\,({\rm{translate}}\,(\=\+{\rm{make-cinfo}}\,(\=\+{\bf{nil}}, \\ 
{\rm{label-alist}}\,({\it{cinfo\/}})\index{label-alist}, \\ 
{\rm{label-cnt}}\,({\rm{translate}}\,(\=\+{\rm{make-cinfo}}\,(\=\+{\bf{nil}}, \\ 
{\rm{label-alist}}\,({\it{cinfo\/}})\index{label-alist}, \\ 
$1\;+$ ($1\;+$ {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}))\-\index{make-cinfo}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{if-true-branch}}\,({\it{stmt\/}})\index{if-true-branch}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{label-cnt})\-\index{make-cinfo}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{if-false-branch}}\,({\it{stmt\/}})\index{if-false-branch}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code})\index{length}))\-)\-)\-\index{tag}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\rm{map-down-values}}\,(\=\+{\rm{mg-alist}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{if-true-branch}}\,({\it{stmt\/}})\index{if-true-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\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}}\,(\=\+{\rm{if-true-branch}}\,({\it{stmt\/}})\index{if-true-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\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})\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}:  if-clock-false-normal \\ \index{if-clock-false-normal}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{if-mg}}) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;${\rm{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resource-errorp}}\,({\rm{mg-meaning-r}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}}, {\it{sizes\/}})\index{mg-meaning-r})\index{resource-errorp}) \\ 
$\wedge$$\;\;\;\;${\rm{mg-expression-falsep}}\,({\rm{if-condition}}\,({\it{stmt\/}})\index{if-condition}, {\it{mg-state\/}})\index{mg-expression-falsep} \\ 
$\wedge$$\;\;\;\;${\rm{normal}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{if-false-branch}}\,({\it{stmt\/}})\index{if-false-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{sizes\/}})\-\index{mg-meaning-r})\index{normal})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{clock}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}})\index{clock} \\ 
$=$$\;\;\;\;$({\tt{5}} $+$ {\rm{clock}}\,({\rm{if-false-branch}}\,({\it{stmt\/}})\index{if-false-branch}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}} $-\;1$)\index{clock}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  if-clock-false-nonnormal \\ \index{if-clock-false-nonnormal}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{if-mg}}) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;${\rm{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resource-errorp}}\,({\rm{mg-meaning-r}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}}, {\it{sizes\/}})\index{mg-meaning-r})\index{resource-errorp}) \\ 
$\wedge$$\;\;\;\;${\rm{mg-expression-falsep}}\,({\rm{if-condition}}\,({\it{stmt\/}})\index{if-condition}, {\it{mg-state\/}})\index{mg-expression-falsep} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{normal}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{if-false-branch}}\,({\it{stmt\/}})\index{if-false-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{sizes\/}})\-\index{mg-meaning-r})\index{normal}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{clock}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}})\index{clock} \\ 
$=$$\;\;\;\;$({\tt{4}} $+$ {\rm{clock}}\,({\rm{if-false-branch}}\,({\it{stmt\/}})\index{if-false-branch}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}} $-\;1$)\index{clock}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  if-clock-true-normal \\ \index{if-clock-true-normal}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{if-mg}}) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;${\rm{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resource-errorp}}\,({\rm{mg-meaning-r}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}}, {\it{sizes\/}})\index{mg-meaning-r})\index{resource-errorp}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{mg-expression-falsep}}\,({\rm{if-condition}}\,({\it{stmt\/}})\index{if-condition}, {\it{mg-state\/}})\index{mg-expression-falsep}) \\ 
$\wedge$$\;\;\;\;${\rm{normal}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{if-true-branch}}\,({\it{stmt\/}})\index{if-true-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{sizes\/}})\-\index{mg-meaning-r})\index{normal})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{clock}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}})\index{clock} \\ 
$=$$\;\;\;\;$({\tt{5}} $+$ {\rm{clock}}\,({\rm{if-true-branch}}\,({\it{stmt\/}})\index{if-true-branch}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}} $-\;1$)\index{clock}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  if-clock-true-nonnormal \\ \index{if-clock-true-nonnormal}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{if-mg}}) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;${\rm{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resource-errorp}}\,({\rm{mg-meaning-r}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}}, {\it{sizes\/}})\index{mg-meaning-r})\index{resource-errorp}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{mg-expression-falsep}}\,({\rm{if-condition}}\,({\it{stmt\/}})\index{if-condition}, {\it{mg-state\/}})\index{mg-expression-falsep}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{normal}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{if-true-branch}}\,({\it{stmt\/}})\index{if-true-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{sizes\/}})\-\index{mg-meaning-r})\index{normal}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{clock}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}})\index{clock} \\ 
$=$$\;\;\;\;$({\tt{3}} $+$ {\rm{clock}}\,({\rm{if-true-branch}}\,({\it{stmt\/}})\index{if-true-branch}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}} $-\;1$)\index{clock}))\-\-
\end{tabbing}

\begin{verbatim};; These are the schemata for the four IF cases.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  if-false-normal-exact-time-schema \\ \index{if-false-normal-exact-time-sche!ma}
\=\+(\=\+({\it{stmt-time\/}} $=$ ({\tt{5}} $+$ {\it{false-time\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{p}}\,({\it{initial\/}}, {\tt{4}})\index{p} $=$ {\it{false-state1\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{p}}\,({\it{false-state1\/}}, {\it{false-time\/}})\index{p} $=$ {\it{false-state2\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{p-step}}\,({\it{false-state2\/}})\index{p-step} $=$ {\it{final\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{p}}\,({\it{initial\/}}, {\it{stmt-time\/}})\index{p} $=$ {\it{final\/}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  if-false-nonnormal-exact-time-schema \\ \index{if-false-nonnormal-exact-time-s!chema}
\=\+(\=\+({\it{stmt-time\/}} $=$ ({\tt{4}} $+$ {\it{false-time\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{p}}\,({\it{initial\/}}, {\tt{4}})\index{p} $=$ {\it{false-state1\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{p}}\,({\it{false-state1\/}}, {\it{false-time\/}})\index{p} $=$ {\it{false-state2\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{false-state2\/}} $=$ {\it{final\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{p}}\,({\it{initial\/}}, {\it{stmt-time\/}})\index{p} $=$ {\it{final\/}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  if-true-normal-exact-time-schema \\ \index{if-true-normal-exact-time-schem!a}
\=\+(\=\+({\it{stmt-time\/}} $=$ ({\tt{5}} $+$ {\it{true-time\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{p}}\,({\it{initial\/}}, {\tt{3}})\index{p} $=$ {\it{true-state1\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{p}}\,({\it{true-state1\/}}, {\it{true-time\/}})\index{p} $=$ {\it{true-state2\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{p}}\,({\it{true-state2\/}}, {\tt{2}})\index{p} $=$ {\it{final\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{p}}\,({\it{initial\/}}, {\it{stmt-time\/}})\index{p} $=$ {\it{final\/}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  if-true-nonnormal-exact-time-schema \\ \index{if-true-nonnormal-exact-time-sc!hema}
\=\+(\=\+({\it{stmt-time\/}} $=$ ({\tt{3}} $+$ {\it{true-time\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{p}}\,({\it{initial\/}}, {\tt{3}})\index{p} $=$ {\it{true-state1\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{p}}\,({\it{true-state1\/}}, {\it{true-time\/}})\index{p} $=$ {\it{true-state2\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{true-state2\/}} $=$ {\it{final\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{p}}\,({\it{initial\/}}, {\it{stmt-time\/}})\index{p} $=$ {\it{final\/}})\-
\end{tabbing}

%\item 
\begin{verbatim}


(prove-lemma if-exact-time-lemma (rewrite)
       (IMPLIES
         (AND (NOT (ZEROP N))
	      (NOT (RESOURCES-INADEQUATEP STMT PROC-LIST
					  (LIST (LENGTH TEMP-STK)
						(P-CTRL-STK-SIZE CTRL-STK))))
	      (EQUAL (CAR STMT) 'IF-MG)
	      (OK-MG-STATEMENT STMT R-COND-LIST NAME-ALIST PROC-LIST)
	      (OK-MG-DEF-PLISTP PROC-LIST)
	      (OK-TRANSLATION-PARAMETERS CINFO T-COND-LIST STMT PROC-LIST CODE2)
	      (OK-MG-STATEP MG-STATE R-COND-LIST)
	      (COND-SUBSETP R-COND-LIST T-COND-LIST)
	      (EQUAL (CODE (TRANSLATE-DEF-BODY (ASSOC SUBR PROC-LIST)
					       PROC-LIST))
		     (APPEND (CODE (TRANSLATE CINFO T-COND-LIST STMT PROC-LIST))
			     CODE2))
	      (USER-DEFINED-PROCP SUBR PROC-LIST)
	      (PLISTP TEMP-STK)
	      (LISTP CTRL-STK)
	      (MG-VARS-LIST-OK-IN-P-STATE (MG-ALIST MG-STATE)
					  (BINDINGS (TOP CTRL-STK))
					  TEMP-STK)
	      (NO-P-ALIASING (BINDINGS (TOP CTRL-STK))
			     (MG-ALIST MG-STATE))
	      (SIGNATURES-MATCH (MG-ALIST MG-STATE)
				NAME-ALIST)
	      (NORMAL MG-STATE)
	      (ALL-CARS-UNIQUE (MG-ALIST MG-STATE))
	      (NOT (RESOURCE-ERRORP (MG-MEANING-R STMT PROC-LIST MG-STATE N
						  (LIST (LENGTH TEMP-STK)
							(P-CTRL-STK-SIZE CTRL-STK)))))
	      (IMPLIES                           ;;; the true branch
	       (AND
		(OK-MG-STATEMENT (IF-TRUE-BRANCH STMT)
				 R-COND-LIST NAME-ALIST PROC-LIST)
		(OK-MG-DEF-PLISTP PROC-LIST)
		(OK-TRANSLATION-PARAMETERS
		 (MAKE-CINFO (APPEND (CODE CINFO)
				     (LIST (LIST 'PUSH-LOCAL
						 (IF-CONDITION STMT))
					   '(FETCH-TEMP-STK)
					   (LIST 'TEST-BOOL-AND-JUMP
						 'FALSE
						 (LABEL-CNT CINFO))))
			     (LABEL-ALIST CINFO)
			     (ADD1 (ADD1 (LABEL-CNT CINFO))))
		 T-COND-LIST
		 (IF-TRUE-BRANCH STMT)
		 PROC-LIST
		 (CONS
		  (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
		  (CONS
		   (CONS 'DL
			 (CONS (LABEL-CNT CINFO)
			       '(NIL (NO-OP))))
		   (APPEND
		    (CODE
		     (TRANSLATE
		      (NULLIFY (TRANSLATE (MAKE-CINFO NIL
						      (LABEL-ALIST CINFO)
						      (ADD1 (ADD1 (LABEL-CNT CINFO))))
					  T-COND-LIST
					  (IF-TRUE-BRANCH STMT)
					  PROC-LIST))
		      T-COND-LIST
		      (IF-FALSE-BRANCH STMT)
		      PROC-LIST))
		    (CONS (CONS 'DL
				(CONS (ADD1 (LABEL-CNT CINFO))
				      '(NIL (NO-OP))))
			  CODE2)))))
		(OK-MG-STATEP MG-STATE R-COND-LIST)
		(COND-SUBSETP R-COND-LIST T-COND-LIST)
		(EQUAL
		 (CODE (TRANSLATE-DEF-BODY (ASSOC SUBR PROC-LIST)
					   PROC-LIST))
		 (APPEND
		  (CODE (TRANSLATE (MAKE-CINFO (APPEND (CODE CINFO)
						       (LIST (LIST 'PUSH-LOCAL
								   (IF-CONDITION STMT))
							     '(FETCH-TEMP-STK)
							     (LIST 'TEST-BOOL-AND-JUMP
								   'FALSE
								   (LABEL-CNT CINFO))))
					       (LABEL-ALIST CINFO)
					       (ADD1 (ADD1 (LABEL-CNT CINFO))))
				   T-COND-LIST
				   (IF-TRUE-BRANCH STMT)
				   PROC-LIST))
		  (CONS
		   (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
		   (CONS
		    (CONS 'DL
			  (CONS (LABEL-CNT CINFO)
				'(NIL (NO-OP))))
		    (APPEND
		     (CODE
		      (TRANSLATE
		       (NULLIFY (TRANSLATE (MAKE-CINFO NIL
						       (LABEL-ALIST CINFO)
						       (ADD1 (ADD1 (LABEL-CNT CINFO))))
					   T-COND-LIST
					   (IF-TRUE-BRANCH STMT)
					   PROC-LIST))
		       T-COND-LIST
		       (IF-FALSE-BRANCH STMT)
		       PROC-LIST))
		     (CONS (CONS 'DL
				 (CONS (ADD1 (LABEL-CNT CINFO))
				       '(NIL (NO-OP))))
			   CODE2))))))
		(USER-DEFINED-PROCP SUBR PROC-LIST)
		(PLISTP TEMP-STK)
		(LISTP CTRL-STK)
		(MG-VARS-LIST-OK-IN-P-STATE (MG-ALIST MG-STATE)
					    (BINDINGS (TOP CTRL-STK))
					    TEMP-STK)
		(NO-P-ALIASING (BINDINGS (TOP CTRL-STK))
			       (MG-ALIST MG-STATE))
		(SIGNATURES-MATCH (MG-ALIST MG-STATE)
				  NAME-ALIST)
		(NORMAL MG-STATE)
		(ALL-CARS-UNIQUE (MG-ALIST MG-STATE))
		(NOT (RESOURCE-ERRORP (MG-MEANING-R (IF-TRUE-BRANCH STMT)
						    PROC-LIST MG-STATE
						    (SUB1 N)
						    (LIST (LENGTH TEMP-STK)
							  (P-CTRL-STK-SIZE CTRL-STK))))))
	       (EQUAL
		(P
		 (MAP-DOWN MG-STATE PROC-LIST CTRL-STK TEMP-STK    ;; true-state1
			   (TAG 'PC
				(CONS SUBR
				      (LENGTH (CODE (MAKE-CINFO (APPEND (CODE CINFO)
									(LIST (LIST 'PUSH-LOCAL
										    (IF-CONDITION STMT))
									      '(FETCH-TEMP-STK)
									      (LIST 'TEST-BOOL-AND-JUMP
										    'FALSE
										    (LABEL-CNT CINFO))))
								(LABEL-ALIST CINFO)
								(ADD1 (ADD1 (LABEL-CNT CINFO))))))))
			   T-COND-LIST)
		 (CLOCK (IF-TRUE-BRANCH STMT)                    ;; true-time
			  PROC-LIST MG-STATE
			  (SUB1 N)))
		(P-STATE;; true-state2
		 (TAG 'PC
		      (CONS SUBR
			    (IF
			     (NORMAL (MG-MEANING-R (IF-TRUE-BRANCH STMT)
						   PROC-LIST MG-STATE
						   (SUB1 N)
						   (LIST (LENGTH TEMP-STK)
							 (P-CTRL-STK-SIZE CTRL-STK))))
			     (LENGTH
			      (CODE (TRANSLATE (MAKE-CINFO (APPEND (CODE CINFO)
								   (LIST (LIST 'PUSH-LOCAL
									       (IF-CONDITION STMT))
									 '(FETCH-TEMP-STK)
									 (LIST 'TEST-BOOL-AND-JUMP
									       'FALSE
									       (LABEL-CNT CINFO))))
							   (LABEL-ALIST CINFO)
							   (ADD1 (ADD1 (LABEL-CNT CINFO))))
					       T-COND-LIST
					       (IF-TRUE-BRANCH STMT)
					       PROC-LIST)))
			     (FIND-LABEL
			      (FETCH-LABEL
			       (CC (MG-MEANING-R (IF-TRUE-BRANCH STMT)
						 PROC-LIST MG-STATE
						 (SUB1 N)
						 (LIST (LENGTH TEMP-STK)
						       (P-CTRL-STK-SIZE CTRL-STK))))
			       (LABEL-ALIST
				(TRANSLATE (MAKE-CINFO (APPEND (CODE CINFO)
							       (LIST (LIST 'PUSH-LOCAL
									   (IF-CONDITION STMT))
								     '(FETCH-TEMP-STK)
								     (LIST 'TEST-BOOL-AND-JUMP
									   'FALSE
									   (LABEL-CNT CINFO))))
						       (LABEL-ALIST CINFO)
						       (ADD1 (ADD1 (LABEL-CNT CINFO))))
					   T-COND-LIST
					   (IF-TRUE-BRANCH STMT)
					   PROC-LIST)))
			      (APPEND
			       (CODE (TRANSLATE (MAKE-CINFO (APPEND (CODE CINFO)
								    (LIST (LIST 'PUSH-LOCAL
										(IF-CONDITION STMT))
									  '(FETCH-TEMP-STK)
									  (LIST 'TEST-BOOL-AND-JUMP
										'FALSE
										(LABEL-CNT CINFO))))
							    (LABEL-ALIST CINFO)
							    (ADD1 (ADD1 (LABEL-CNT CINFO))))
						T-COND-LIST
						(IF-TRUE-BRANCH STMT)
						PROC-LIST))
			       (CONS
				(LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
				(CONS
				 (CONS 'DL
				       (CONS (LABEL-CNT CINFO)
					     '(NIL (NO-OP))))
				 (APPEND
				  (CODE
				   (TRANSLATE
				    (NULLIFY (TRANSLATE (MAKE-CINFO NIL
								    (LABEL-ALIST CINFO)
								    (ADD1 (ADD1 (LABEL-CNT CINFO))))
							T-COND-LIST
							(IF-TRUE-BRANCH STMT)
							PROC-LIST))
				    T-COND-LIST
				    (IF-FALSE-BRANCH STMT)
				    PROC-LIST))
				  (CONS (CONS 'DL
					      (CONS (ADD1 (LABEL-CNT CINFO))
						    '(NIL (NO-OP))))
					CODE2)))))))))
		 CTRL-STK
		 (MAP-DOWN-VALUES
		  (MG-ALIST (MG-MEANING-R (IF-TRUE-BRANCH STMT)
					  PROC-LIST MG-STATE
					  (SUB1 N)
					  (LIST (LENGTH TEMP-STK)
						(P-CTRL-STK-SIZE CTRL-STK))))
		  (BINDINGS (TOP CTRL-STK))
		  TEMP-STK)
		 (TRANSLATE-PROC-LIST PROC-LIST)
		 (LIST
		  (LIST 'C-C
			(MG-COND-TO-P-NAT (CC (MG-MEANING-R (IF-TRUE-BRANCH STMT)
							    PROC-LIST MG-STATE
							    (SUB1 N)
							    (LIST (LENGTH TEMP-STK)
								  (P-CTRL-STK-SIZE CTRL-STK))))
					  T-COND-LIST)))
		 (MG-MAX-CTRL-STK-SIZE)
		 (MG-MAX-TEMP-STK-SIZE)
		 (MG-WORD-SIZE)
		 'RUN)))
	      (IMPLIES
	       (AND
		(OK-MG-STATEMENT (IF-FALSE-BRANCH STMT)
				 R-COND-LIST NAME-ALIST PROC-LIST)
		(OK-MG-DEF-PLISTP PROC-LIST)
		(OK-TRANSLATION-PARAMETERS
		 (ADD-CODE (TRANSLATE (MAKE-CINFO (APPEND (CODE CINFO)
							  (LIST (LIST 'PUSH-LOCAL
								      (IF-CONDITION STMT))
								'(FETCH-TEMP-STK)
								(LIST 'TEST-BOOL-AND-JUMP
								      'FALSE
								      (LABEL-CNT CINFO))))
						  (LABEL-ALIST CINFO)
						  (ADD1 (ADD1 (LABEL-CNT CINFO))))
				      T-COND-LIST
				      (IF-TRUE-BRANCH STMT)
				      PROC-LIST)
			   (LIST (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
				 (CONS 'DL
				       (CONS (LABEL-CNT CINFO)
					     '(NIL (NO-OP))))))
		 T-COND-LIST
		 (IF-FALSE-BRANCH STMT)
		 PROC-LIST
		 (CONS (CONS 'DL
			     (CONS (ADD1 (LABEL-CNT CINFO))
				   '(NIL (NO-OP))))
		       CODE2))
		(OK-MG-STATEP MG-STATE R-COND-LIST)
		(COND-SUBSETP R-COND-LIST T-COND-LIST)
		(EQUAL
		 (CODE (TRANSLATE-DEF-BODY (ASSOC SUBR PROC-LIST)
					   PROC-LIST))
		 (APPEND
		  (CODE
		   (TRANSLATE
		    (ADD-CODE
		     (TRANSLATE (MAKE-CINFO (APPEND (CODE CINFO)
						    (LIST (LIST 'PUSH-LOCAL
								(IF-CONDITION STMT))
							  '(FETCH-TEMP-STK)
							  (LIST 'TEST-BOOL-AND-JUMP
								'FALSE
								(LABEL-CNT CINFO))))
					    (LABEL-ALIST CINFO)
					    (ADD1 (ADD1 (LABEL-CNT CINFO))))
				T-COND-LIST
				(IF-TRUE-BRANCH STMT)
				PROC-LIST)
		     (LIST (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
			   (CONS 'DL
				 (CONS (LABEL-CNT CINFO)
				       '(NIL (NO-OP))))))
		    T-COND-LIST
		    (IF-FALSE-BRANCH STMT)
		    PROC-LIST))
		  (CONS (CONS 'DL
			      (CONS (ADD1 (LABEL-CNT CINFO))
				    '(NIL (NO-OP))))
			CODE2)))
		(USER-DEFINED-PROCP SUBR PROC-LIST)
		(PLISTP TEMP-STK)
		(LISTP CTRL-STK)
		(MG-VARS-LIST-OK-IN-P-STATE (MG-ALIST MG-STATE)
					    (BINDINGS (TOP CTRL-STK))
					    TEMP-STK)
		(NO-P-ALIASING (BINDINGS (TOP CTRL-STK))
			       (MG-ALIST MG-STATE))
		(SIGNATURES-MATCH (MG-ALIST MG-STATE)
				  NAME-ALIST)
		(NORMAL MG-STATE)
		(ALL-CARS-UNIQUE (MG-ALIST MG-STATE))
		(NOT (RESOURCE-ERRORP (MG-MEANING-R (IF-FALSE-BRANCH STMT)
						    PROC-LIST MG-STATE
						    (SUB1 N)
						    (LIST (LENGTH TEMP-STK)
							  (P-CTRL-STK-SIZE CTRL-STK))))))
	       (EQUAL
		(P
		 (MAP-DOWN MG-STATE PROC-LIST CTRL-STK TEMP-STK                     ;; false-state1
			   (TAG 'PC
				(CONS SUBR
				      (LENGTH
				       (CODE
					(ADD-CODE
					 (TRANSLATE (MAKE-CINFO (APPEND (CODE CINFO)
									(LIST (LIST 'PUSH-LOCAL
										    (IF-CONDITION STMT))
									      '(FETCH-TEMP-STK)
									      (LIST 'TEST-BOOL-AND-JUMP
										    'FALSE
										    (LABEL-CNT CINFO))))
								(LABEL-ALIST CINFO)
								(ADD1 (ADD1 (LABEL-CNT CINFO))))
						    T-COND-LIST
						    (IF-TRUE-BRANCH STMT)
						    PROC-LIST)
					 (LIST (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
					       (CONS 'DL
						     (CONS (LABEL-CNT CINFO)
							   '(NIL (NO-OP))))))))))
			   T-COND-LIST)
		 (CLOCK (IF-FALSE-BRANCH STMT)                           ;; false-time
			  PROC-LIST MG-STATE
			  (SUB1 N)))
		(P-STATE;; false-state2
		 (TAG 'PC
		      (CONS SUBR
			    (IF
			     (NORMAL (MG-MEANING-R (IF-FALSE-BRANCH STMT)
						   PROC-LIST MG-STATE
						   (SUB1 N)
						   (LIST (LENGTH TEMP-STK)
							 (P-CTRL-STK-SIZE CTRL-STK))))
			     (LENGTH
			      (CODE
			       (TRANSLATE
				(ADD-CODE
				 (TRANSLATE (MAKE-CINFO (APPEND (CODE CINFO)
								(LIST (LIST 'PUSH-LOCAL
									    (IF-CONDITION STMT))
								      '(FETCH-TEMP-STK)
								      (LIST 'TEST-BOOL-AND-JUMP
									    'FALSE
									    (LABEL-CNT CINFO))))
							(LABEL-ALIST CINFO)
							(ADD1 (ADD1 (LABEL-CNT CINFO))))
					    T-COND-LIST
					    (IF-TRUE-BRANCH STMT)
					    PROC-LIST)
				 (LIST (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
				       (CONS 'DL
					     (CONS (LABEL-CNT CINFO)
						   '(NIL (NO-OP))))))
				T-COND-LIST
				(IF-FALSE-BRANCH STMT)
				PROC-LIST)))
			     (FIND-LABEL
			      (FETCH-LABEL
			       (CC (MG-MEANING-R (IF-FALSE-BRANCH STMT)
						 PROC-LIST MG-STATE
						 (SUB1 N)
						 (LIST (LENGTH TEMP-STK)
						       (P-CTRL-STK-SIZE CTRL-STK))))
			       (LABEL-ALIST
				(TRANSLATE
				 (ADD-CODE
				  (TRANSLATE (MAKE-CINFO (APPEND (CODE CINFO)
								 (LIST (LIST 'PUSH-LOCAL
									     (IF-CONDITION STMT))
								       '(FETCH-TEMP-STK)
								       (LIST 'TEST-BOOL-AND-JUMP
									     'FALSE
									     (LABEL-CNT CINFO))))
							 (LABEL-ALIST CINFO)
							 (ADD1 (ADD1 (LABEL-CNT CINFO))))
					     T-COND-LIST
					     (IF-TRUE-BRANCH STMT)
					     PROC-LIST)
				  (LIST (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
					(CONS 'DL
					      (CONS (LABEL-CNT CINFO)
						    '(NIL (NO-OP))))))
				 T-COND-LIST
				 (IF-FALSE-BRANCH STMT)
				 PROC-LIST)))
			      (APPEND
			       (CODE
				(TRANSLATE
				 (ADD-CODE
				  (TRANSLATE (MAKE-CINFO (APPEND (CODE CINFO)
								 (LIST (LIST 'PUSH-LOCAL
									     (IF-CONDITION STMT))
								       '(FETCH-TEMP-STK)
								       (LIST 'TEST-BOOL-AND-JUMP
									     'FALSE
									     (LABEL-CNT CINFO))))
							 (LABEL-ALIST CINFO)
							 (ADD1 (ADD1 (LABEL-CNT CINFO))))
					     T-COND-LIST
					     (IF-TRUE-BRANCH STMT)
					     PROC-LIST)
				  (LIST (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
					(CONS 'DL
					      (CONS (LABEL-CNT CINFO)
						    '(NIL (NO-OP))))))
				 T-COND-LIST
				 (IF-FALSE-BRANCH STMT)
				 PROC-LIST))
			       (CONS (CONS 'DL
					   (CONS (ADD1 (LABEL-CNT CINFO))
						 '(NIL (NO-OP))))
				     CODE2))))))
		 CTRL-STK
		 (MAP-DOWN-VALUES
		  (MG-ALIST (MG-MEANING-R (IF-FALSE-BRANCH STMT)
					  PROC-LIST MG-STATE
					  (SUB1 N)
					  (LIST (LENGTH TEMP-STK)
						(P-CTRL-STK-SIZE CTRL-STK))))
		  (BINDINGS (TOP CTRL-STK))
		  TEMP-STK)
		 (TRANSLATE-PROC-LIST PROC-LIST)
		 (LIST
		  (LIST 'C-C
			(MG-COND-TO-P-NAT (CC (MG-MEANING-R (IF-FALSE-BRANCH STMT)
							    PROC-LIST MG-STATE
							    (SUB1 N)
							    (LIST (LENGTH TEMP-STK)
								  (P-CTRL-STK-SIZE CTRL-STK))))
					  T-COND-LIST)))
		 (MG-MAX-CTRL-STK-SIZE)
		 (MG-MAX-TEMP-STK-SIZE)
		 (MG-WORD-SIZE)
		 'RUN))))
 (EQUAL
  (P (MAP-DOWN MG-STATE PROC-LIST CTRL-STK TEMP-STK                  ;; initial
               (TAG 'PC
                    (CONS SUBR (LENGTH (CODE CINFO))))
               T-COND-LIST)
     (CLOCK STMT PROC-LIST MG-STATE N))                              ;; stmt-time
  (P-STATE;; final
   (TAG 'PC
	(CONS SUBR
	      (IF
	       (NORMAL (MG-MEANING-R STMT PROC-LIST MG-STATE N
				     (LIST (LENGTH TEMP-STK)
					   (P-CTRL-STK-SIZE CTRL-STK))))
	       (LENGTH (CODE (TRANSLATE CINFO T-COND-LIST STMT PROC-LIST)))
	       (FIND-LABEL
		(FETCH-LABEL (CC (MG-MEANING-R STMT PROC-LIST MG-STATE N
					       (LIST (LENGTH TEMP-STK)
						     (P-CTRL-STK-SIZE CTRL-STK))))
			     (LABEL-ALIST (TRANSLATE CINFO T-COND-LIST STMT
						     PROC-LIST)))
		(APPEND (CODE (TRANSLATE CINFO T-COND-LIST STMT PROC-LIST))
			CODE2)))))
   CTRL-STK
   (MAP-DOWN-VALUES (MG-ALIST (MG-MEANING-R STMT PROC-LIST MG-STATE N
                                            (LIST (LENGTH TEMP-STK)
                                                  (P-CTRL-STK-SIZE CTRL-STK))))
                    (BINDINGS (TOP CTRL-STK))
                    TEMP-STK)
   (TRANSLATE-PROC-LIST PROC-LIST)
   (LIST
    (LIST 'C-C
	  (MG-COND-TO-P-NAT (CC (MG-MEANING-R STMT PROC-LIST MG-STATE N
					      (LIST (LENGTH TEMP-STK)
						    (P-CTRL-STK-SIZE CTRL-STK))))
			    T-COND-LIST)))
   (MG-MAX-CTRL-STK-SIZE)
   (MG-MAX-TEMP-STK-SIZE)
   (MG-WORD-SIZE)
   'RUN)))
 ((INSTRUCTIONS
   (ADD-ABBREVIATION @INITIAL
                     (MAP-DOWN MG-STATE PROC-LIST CTRL-STK TEMP-STK
                               (TAG 'PC
                                    (CONS SUBR (LENGTH (CODE CINFO))))
                               T-COND-LIST))
   (ADD-ABBREVIATION @STMT-TIME
                     (CLOCK STMT PROC-LIST MG-STATE N))
   (ADD-ABBREVIATION @FINAL
    (P-STATE
     (TAG 'PC
	  (CONS SUBR
		(IF
		 (NORMAL (MG-MEANING-R STMT PROC-LIST MG-STATE N
				       (LIST (LENGTH TEMP-STK)
					     (P-CTRL-STK-SIZE CTRL-STK))))
		 (LENGTH (CODE (TRANSLATE CINFO T-COND-LIST STMT PROC-LIST)))
		 (FIND-LABEL
		  (FETCH-LABEL (CC (MG-MEANING-R STMT PROC-LIST MG-STATE N
						 (LIST (LENGTH TEMP-STK)
						       (P-CTRL-STK-SIZE CTRL-STK))))
			       (LABEL-ALIST (TRANSLATE CINFO T-COND-LIST STMT
						       PROC-LIST)))
		  (APPEND (CODE (TRANSLATE CINFO T-COND-LIST STMT PROC-LIST))
			  CODE2)))))
     CTRL-STK
     (MAP-DOWN-VALUES
      (MG-ALIST (MG-MEANING-R STMT PROC-LIST MG-STATE N
			      (LIST (LENGTH TEMP-STK)
				    (P-CTRL-STK-SIZE CTRL-STK))))
      (BINDINGS (TOP CTRL-STK))
      TEMP-STK)
     (TRANSLATE-PROC-LIST PROC-LIST)
     (LIST
      (LIST 'C-C
	    (MG-COND-TO-P-NAT (CC (MG-MEANING-R STMT PROC-LIST MG-STATE N
						(LIST (LENGTH TEMP-STK)
						      (P-CTRL-STK-SIZE CTRL-STK))))
			      T-COND-LIST)))
     (MG-MAX-CTRL-STK-SIZE)
     (MG-MAX-TEMP-STK-SIZE)
     (MG-WORD-SIZE)
     'RUN))
   (ADD-ABBREVIATION @TRUE-STATE1
    (MAP-DOWN MG-STATE PROC-LIST CTRL-STK TEMP-STK
     (TAG 'PC
       (CONS SUBR
             (LENGTH (CODE (MAKE-CINFO (APPEND (CODE CINFO)
                                               (LIST (LIST 'PUSH-LOCAL
                                                           (IF-CONDITION STMT))
                                                     '(FETCH-TEMP-STK)
                                                     (LIST 'TEST-BOOL-AND-JUMP
                                                           'FALSE
                                                           (LABEL-CNT CINFO))))
                                       (LABEL-ALIST CINFO)
                                       (ADD1 (ADD1 (LABEL-CNT CINFO))))))))
     T-COND-LIST))
   (ADD-ABBREVIATION @TRUE-TIME
                     (CLOCK (IF-TRUE-BRANCH STMT)
                            PROC-LIST MG-STATE
                            (SUB1 N)))
   (ADD-ABBREVIATION @TRUE-STATE2
    (P-STATE
     (TAG 'PC
	  (CONS SUBR
		(IF
		 (NORMAL (MG-MEANING-R (IF-TRUE-BRANCH STMT)
				       PROC-LIST MG-STATE
				       (SUB1 N)
				       (LIST (LENGTH TEMP-STK)
					     (P-CTRL-STK-SIZE CTRL-STK))))
		 (LENGTH
		  (CODE (TRANSLATE (MAKE-CINFO (APPEND (CODE CINFO)
						       (LIST (LIST 'PUSH-LOCAL
								   (IF-CONDITION STMT))
							     '(FETCH-TEMP-STK)
							     (LIST 'TEST-BOOL-AND-JUMP
								   'FALSE
								   (LABEL-CNT CINFO))))
					       (LABEL-ALIST CINFO)
					       (ADD1 (ADD1 (LABEL-CNT CINFO))))
				   T-COND-LIST
				   (IF-TRUE-BRANCH STMT)
				   PROC-LIST)))
		 (FIND-LABEL
		  (FETCH-LABEL
		   (CC (MG-MEANING-R (IF-TRUE-BRANCH STMT)
				     PROC-LIST MG-STATE
				     (SUB1 N)
				     (LIST (LENGTH TEMP-STK)
					   (P-CTRL-STK-SIZE CTRL-STK))))
		   (LABEL-ALIST
		    (TRANSLATE (MAKE-CINFO (APPEND (CODE CINFO)
						   (LIST (LIST 'PUSH-LOCAL
							       (IF-CONDITION STMT))
							 '(FETCH-TEMP-STK)
							 (LIST 'TEST-BOOL-AND-JUMP
							       'FALSE
							       (LABEL-CNT CINFO))))
					   (LABEL-ALIST CINFO)
					   (ADD1 (ADD1 (LABEL-CNT CINFO))))
			       T-COND-LIST
			       (IF-TRUE-BRANCH STMT)
			       PROC-LIST)))
		  (APPEND
		   (CODE (TRANSLATE (MAKE-CINFO (APPEND (CODE CINFO)
							(LIST (LIST 'PUSH-LOCAL
								    (IF-CONDITION STMT))
							      '(FETCH-TEMP-STK)
							      (LIST 'TEST-BOOL-AND-JUMP
								    'FALSE
								    (LABEL-CNT CINFO))))
						(LABEL-ALIST CINFO)
						(ADD1 (ADD1 (LABEL-CNT CINFO))))
				    T-COND-LIST
				    (IF-TRUE-BRANCH STMT)
				    PROC-LIST))
		   (CONS
		    (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
		    (CONS
		     (CONS 'DL
			   (CONS (LABEL-CNT CINFO)
				 '(NIL (NO-OP))))
		     (APPEND
		      (CODE
		       (TRANSLATE
			(NULLIFY (TRANSLATE (MAKE-CINFO NIL
							(LABEL-ALIST CINFO)
							(ADD1 (ADD1 (LABEL-CNT CINFO))))
					    T-COND-LIST
					    (IF-TRUE-BRANCH STMT)
					    PROC-LIST))
			T-COND-LIST
			(IF-FALSE-BRANCH STMT)
			PROC-LIST))
		      (CONS (CONS 'DL
				  (CONS (ADD1 (LABEL-CNT CINFO))
					'(NIL (NO-OP))))
			    CODE2)))))))))
     CTRL-STK
     (MAP-DOWN-VALUES
      (MG-ALIST (MG-MEANING-R (IF-TRUE-BRANCH STMT)
			      PROC-LIST MG-STATE
			      (SUB1 N)
			      (LIST (LENGTH TEMP-STK)
				    (P-CTRL-STK-SIZE CTRL-STK))))
      (BINDINGS (TOP CTRL-STK))
      TEMP-STK)
     (TRANSLATE-PROC-LIST PROC-LIST)
     (LIST
      (LIST 'C-C
	    (MG-COND-TO-P-NAT (CC (MG-MEANING-R (IF-TRUE-BRANCH STMT)
						PROC-LIST MG-STATE
						(SUB1 N)
						(LIST (LENGTH TEMP-STK)
						      (P-CTRL-STK-SIZE CTRL-STK))))
			      T-COND-LIST)))
     (MG-MAX-CTRL-STK-SIZE)
     (MG-MAX-TEMP-STK-SIZE)
     (MG-WORD-SIZE)
     'RUN))
   (ADD-ABBREVIATION @FALSE-STATE1
    (MAP-DOWN MG-STATE PROC-LIST CTRL-STK TEMP-STK
     (TAG 'PC
      (CONS SUBR
       (LENGTH
        (CODE
         (ADD-CODE
                (TRANSLATE (MAKE-CINFO (APPEND (CODE CINFO)
                                               (LIST (LIST 'PUSH-LOCAL
                                                           (IF-CONDITION STMT))
                                                     '(FETCH-TEMP-STK)
                                                     (LIST 'TEST-BOOL-AND-JUMP
                                                           'FALSE
                                                           (LABEL-CNT CINFO))))
                                       (LABEL-ALIST CINFO)
                                       (ADD1 (ADD1 (LABEL-CNT CINFO))))
                           T-COND-LIST
                           (IF-TRUE-BRANCH STMT)
                           PROC-LIST)
                (LIST (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
                      (CONS 'DL
                            (CONS (LABEL-CNT CINFO)
                                  '(NIL (NO-OP))))))))))
     T-COND-LIST))
   (ADD-ABBREVIATION @FALSE-TIME
                     (CLOCK (IF-FALSE-BRANCH STMT)
                            PROC-LIST MG-STATE
                            (SUB1 N)))
   (ADD-ABBREVIATION @FALSE-STATE2
    (P-STATE
     (TAG 'PC
      (CONS SUBR
       (IF
        (NORMAL (MG-MEANING-R (IF-FALSE-BRANCH STMT)
                              PROC-LIST MG-STATE
                              (SUB1 N)
                              (LIST (LENGTH TEMP-STK)
                                    (P-CTRL-STK-SIZE CTRL-STK))))
        (LENGTH
         (CODE
          (TRANSLATE
           (ADD-CODE
                (TRANSLATE (MAKE-CINFO (APPEND (CODE CINFO)
                                               (LIST (LIST 'PUSH-LOCAL
                                                           (IF-CONDITION STMT))
                                                     '(FETCH-TEMP-STK)
                                                     (LIST 'TEST-BOOL-AND-JUMP
                                                           'FALSE
                                                           (LABEL-CNT CINFO))))
                                       (LABEL-ALIST CINFO)
                                       (ADD1 (ADD1 (LABEL-CNT CINFO))))
                           T-COND-LIST
                           (IF-TRUE-BRANCH STMT)
                           PROC-LIST)
                (LIST (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
                      (CONS 'DL
                            (CONS (LABEL-CNT CINFO)
                                  '(NIL (NO-OP))))))
           T-COND-LIST
           (IF-FALSE-BRANCH STMT)
           PROC-LIST)))
        (FIND-LABEL
         (FETCH-LABEL
          (CC (MG-MEANING-R (IF-FALSE-BRANCH STMT)
                            PROC-LIST MG-STATE
                            (SUB1 N)
                            (LIST (LENGTH TEMP-STK)
                                  (P-CTRL-STK-SIZE CTRL-STK))))
          (LABEL-ALIST
           (TRANSLATE
            (ADD-CODE
                (TRANSLATE (MAKE-CINFO (APPEND (CODE CINFO)
                                               (LIST (LIST 'PUSH-LOCAL
                                                           (IF-CONDITION STMT))
                                                     '(FETCH-TEMP-STK)
                                                     (LIST 'TEST-BOOL-AND-JUMP
                                                           'FALSE
                                                           (LABEL-CNT CINFO))))
                                       (LABEL-ALIST CINFO)
                                       (ADD1 (ADD1 (LABEL-CNT CINFO))))
                           T-COND-LIST
                           (IF-TRUE-BRANCH STMT)
                           PROC-LIST)
                (LIST (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
                      (CONS 'DL
                            (CONS (LABEL-CNT CINFO)
                                  '(NIL (NO-OP))))))
            T-COND-LIST
            (IF-FALSE-BRANCH STMT)
            PROC-LIST)))
         (APPEND
          (CODE
           (TRANSLATE
            (ADD-CODE
                (TRANSLATE (MAKE-CINFO (APPEND (CODE CINFO)
                                               (LIST (LIST 'PUSH-LOCAL
                                                           (IF-CONDITION STMT))
                                                     '(FETCH-TEMP-STK)
                                                     (LIST 'TEST-BOOL-AND-JUMP
                                                           'FALSE
                                                           (LABEL-CNT CINFO))))
                                       (LABEL-ALIST CINFO)
                                       (ADD1 (ADD1 (LABEL-CNT CINFO))))
                           T-COND-LIST
                           (IF-TRUE-BRANCH STMT)
                           PROC-LIST)
                (LIST (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
                      (CONS 'DL
                            (CONS (LABEL-CNT CINFO)
                                  '(NIL (NO-OP))))))
            T-COND-LIST
            (IF-FALSE-BRANCH STMT)
            PROC-LIST))
          (CONS (CONS 'DL
                      (CONS (ADD1 (LABEL-CNT CINFO))
                            '(NIL (NO-OP))))
                CODE2))))))
     CTRL-STK
     (MAP-DOWN-VALUES
                    (MG-ALIST (MG-MEANING-R (IF-FALSE-BRANCH STMT)
                                            PROC-LIST MG-STATE
                                            (SUB1 N)
                                            (LIST (LENGTH TEMP-STK)
                                                  (P-CTRL-STK-SIZE CTRL-STK))))
                    (BINDINGS (TOP CTRL-STK))
                    TEMP-STK)
     (TRANSLATE-PROC-LIST PROC-LIST)
     (LIST
      (LIST 'C-C
        (MG-COND-TO-P-NAT (CC (MG-MEANING-R (IF-FALSE-BRANCH STMT)
                                            PROC-LIST MG-STATE
                                            (SUB1 N)
                                            (LIST (LENGTH TEMP-STK)
                                                  (P-CTRL-STK-SIZE CTRL-STK))))
                          T-COND-LIST)))
     (MG-MAX-CTRL-STK-SIZE)
     (MG-MAX-TEMP-STK-SIZE)
     (MG-WORD-SIZE)
     'RUN))
   PROMOTE
   (CLAIM (MG-EXPRESSION-FALSEP (IF-CONDITION STMT)
                                MG-STATE)
          0)
   (DROP 19)
   (DEMOTE 19)
   (DIVE 1 1)
   PUSH TOP PROMOTE
   (CLAIM (EQUAL (P @INITIAL 4) @FALSE-STATE1)
          0)
   (CLAIM (NORMAL (MG-MEANING-R (IF-FALSE-BRANCH STMT)
                                PROC-LIST MG-STATE
                                (SUB1 N)
                                (LIST (LENGTH TEMP-STK)
                                      (P-CTRL-STK-SIZE CTRL-STK))))
          0)
   (CLAIM (EQUAL (P-STEP @FALSE-STATE2) @FINAL)
          0)
   (CLAIM (EQUAL @STMT-TIME
                 (PLUS 5 @FALSE-TIME))
          0)
   (DEMOTE 20 21 23 24)
   DROP
   (GENERALIZE ((@FALSE-STATE2 FALSE-STATE2)
                (@FALSE-TIME FALSE-TIME)
                (@FALSE-STATE1 FALSE-STATE1)
                (@TRUE-STATE2 TRUE-STATE2)
                (@TRUE-TIME TRUE-TIME)
                (@TRUE-STATE1 TRUE-STATE1)
                (@FINAL FINAL)
                (@STMT-TIME STMT-TIME)
                (@INITIAL INITIAL)))
   DROP
   (USE-LEMMA IF-FALSE-NORMAL-EXACT-TIME-SCHEMA)
   PROVE
   (CONTRADICT 24)
   (DIVE 1)
   (REWRITE IF-CLOCK-FALSE-NORMAL)
   TOP S
   (CONTRADICT 23)
   (DIVE 1)
   (REWRITE IF-STEP-NORMAL-FALSE-STATE2-EQUALS-FINAL)
   TOP S-PROP
   (CLAIM (EQUAL @FALSE-STATE2 @FINAL) 0)
   (CLAIM (EQUAL @STMT-TIME
                 (PLUS 4 @FALSE-TIME))
          0)
   (DEMOTE 20 21 23 24)
   (GENERALIZE ((@FALSE-STATE2 FALSE-STATE2)
                (@FALSE-TIME FALSE-TIME)
                (@FALSE-STATE1 FALSE-STATE1)
                (@TRUE-STATE2 TRUE-STATE2)
                (@TRUE-TIME TRUE-TIME)
                (@TRUE-STATE1 TRUE-STATE1)
                (@FINAL FINAL)
                (@STMT-TIME STMT-TIME)
                (@INITIAL INITIAL)))
   DROP
   (USE-LEMMA IF-FALSE-NONNORMAL-EXACT-TIME-SCHEMA)
   PROVE
   (CONTRADICT 24)
   (DIVE 1)
   (REWRITE IF-CLOCK-FALSE-NONNORMAL)
   TOP S
   (CONTRADICT 23)
   (DIVE 1)
   (REWRITE IF-NON-NORMAL-FALSE-STATE2-EQUALS-FINAL)
   TOP S-PROP
   (CONTRADICT 21)
   (DROP 20 21)
   (DIVE 1)
   (REWRITE P-ADD1-3)
   (DIVE 1)
   (REWRITE IF-INITIAL-STEP1)
   UP
   (REWRITE P-ADD1-3)
   (DIVE 1)
   (REWRITE IF-INITIAL-STEP2)
   UP
   (REWRITE P-ADD1-3)
   (DIVE 1)
   (REWRITE IF-INITIAL-STEP3-FALSE-TEST)
   UP
   (REWRITE P-ADD1-3)
   (REWRITE P-0-UNWINDING-LEMMA)
   (REWRITE IF-INITIAL-STEP4-FALSE-TEST)
   TOP S-PROP SPLIT
   (REWRITE IF-FALSE-BRANCH-HYPS)
   (REWRITE IF-FALSE-BRANCH-HYPS)
   (DIVE 1)
   (REWRITE IF-FALSE-BRANCH-HYPS)
   TOP S
   (DIVE 1)
   (REWRITE IF-FALSE-BRANCH-HYPS)
   TOP S
   (DROP 20)
   (DEMOTE 19)
   (DIVE 1 1)
   PUSH TOP PROMOTE
   (CLAIM (EQUAL (P @INITIAL 3) @TRUE-STATE1)
          0)
   (CLAIM (NORMAL (MG-MEANING-R (IF-TRUE-BRANCH STMT)
                                PROC-LIST MG-STATE
                                (SUB1 N)
                                (LIST (LENGTH TEMP-STK)
                                      (P-CTRL-STK-SIZE CTRL-STK))))
          0)
   (CLAIM (EQUAL (P @TRUE-STATE2 2) @FINAL)
          0)
   (CLAIM (EQUAL @STMT-TIME (PLUS 5 @TRUE-TIME))
          0)
   (DEMOTE 20 21 23 24)
   (GENERALIZE ((@FALSE-STATE2 FALSE-STATE2)
                (@FALSE-TIME FALSE-TIME)
                (@FALSE-STATE1 FALSE-STATE1)
                (@TRUE-STATE2 TRUE-STATE2)
                (@TRUE-TIME TRUE-TIME)
                (@TRUE-STATE1 TRUE-STATE1)
                (@FINAL FINAL)
                (@STMT-TIME STMT-TIME)
                (@INITIAL INITIAL)))
   DROP
   (USE-LEMMA IF-TRUE-NORMAL-EXACT-TIME-SCHEMA)
   PROVE
   (CONTRADICT 24)
   (DIVE 1)
   (REWRITE IF-CLOCK-TRUE-NORMAL)
   TOP S
   (CONTRADICT 23)
   (DROP 20 21 23)
   (DIVE 1)
   (REWRITE P-ADD1-3)
   (REWRITE P-ADD1-3)
   (REWRITE P-0-UNWINDING-LEMMA)
   (DIVE 1)
   (REWRITE IF-NORMAL-TRUE-STATE2-STEP1)
   UP
   (REWRITE IF-NORMAL-TRUE-STATE2-STEP2-EQUALS-FINAL)
   TOP S-PROP
   (CLAIM (EQUAL @TRUE-STATE2 @FINAL) 0)
   (CLAIM (EQUAL @STMT-TIME (PLUS 3 @TRUE-TIME))
          0)
   (DEMOTE 20 21 23 24)
   (GENERALIZE ((@FALSE-STATE2 FALSE-STATE2)
                (@FALSE-TIME FALSE-TIME)
                (@FALSE-STATE1 FALSE-STATE1)
                (@TRUE-STATE2 TRUE-STATE2)
                (@TRUE-TIME TRUE-TIME)
                (@TRUE-STATE1 TRUE-STATE1)
                (@FINAL FINAL)
                (@STMT-TIME STMT-TIME)
                (@INITIAL INITIAL)))
   DROP
   (USE-LEMMA IF-TRUE-NONNORMAL-EXACT-TIME-SCHEMA)
   PROVE
   (CONTRADICT 24)
   (DIVE 1)
   (REWRITE IF-CLOCK-TRUE-NONNORMAL)
   TOP S
   (CONTRADICT 23)
   (DIVE 1)
   (REWRITE IF-NONNORMAL-TRUE-STATE2-EQUALS-FINAL)
   TOP S-PROP
   (CONTRADICT 21)
   (DIVE 1)
   (REWRITE P-ADD1-3)
   (REWRITE P-ADD1-3)
   (REWRITE P-ADD1-3)
   (REWRITE P-0-UNWINDING-LEMMA)
   (DIVE 1 1)
   (REWRITE IF-INITIAL-STEP1)
   UP
   (REWRITE IF-INITIAL-STEP2)
   UP
   (REWRITE IF-INITIAL-STEP3-TRUE-TEST-EQUALS-TRUE-STATE1)
   UP S SPLIT
   (REWRITE IF-TRUE-BRANCH-HYPS)
   (REWRITE IF-TRUE-BRANCH-HYPS)
   (DIVE 1)
   (REWRITE IF-TRUE-BRANCH-HYPS)
   TOP S
   (DIVE 1)
   (REWRITE IF-TRUE-BRANCH-HYPS)
   TOP S)))
\end{verbatim}



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

\addvspace{18pt}

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