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

\addvspace{18pt}

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

\end{verbatim}\begin{tabbing}{\sc Theorem}:  loop-translation-2 \\ \index{loop-translation-2}
\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{loop-mg}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{translate}}\,({\it{cinfo\/}}, {\it{cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}})\index{translate} \\ 
$=$$\;\;\;\;${\rm{discard-label}}\,({\rm{add-code}}\,(\=\+{\rm{translate}}\,(\=\+{\rm{make-cinfo}}\,(\=\+{\rm{append}}\,(\=\+{\rm{code}}\,({\it{cinfo\/}})\index{code}, \\ 
{\rm{list}}\,({\rm{list}}\,(\=\+{\tt{'}}{\tt{dl}}, \\ 
{\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}, \\ 
{\bf{nil}}, \\ 
{\tt{'}}{\tt{(}}\=\+{\tt{no-op}}{\tt{)}}\-)\-))\-, \\ 
{\rm{cons}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{leave}}, \\ 
$1\;+$ {\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{loop-body}}\,({\it{stmt\/}})\index{loop-body}, \\ 
{\it{proc-list\/}})\-\index{translate}, \\ 
{\rm{list}}\,(\=\+{\rm{list}}\,({\tt{'}}{\tt{jump}}, {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}), \\ 
{\rm{list}}\,(\=\+{\tt{'}}{\tt{dl}}, \\ 
$1\;+$ {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}, \\ 
{\bf{nil}}, \\ 
{\tt{'}}{\tt{(}}\=\+{\tt{push-constant}} \\ 
{\tt{(}}{\tt{nat}}{\tt{ }}{\tt{2}}{\tt{)}}{\tt{)}}\-)\-, \\ 
{\tt{'}}{\tt{(}}{\tt{pop-global}}{\tt{ }}{\tt{c-c}}{\tt{)}})\-)\-\index{add-code})\index{discard-label})\-\-
\end{tabbing}

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


\noindent{\sc Event}:   Disable loop-meaning-r-2.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  loop-body-doesnt-halt \\ \index{loop-body-doesnt-halt}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{loop-mg}}) \\ 
$\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}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{mg-psw}}\,({\rm{mg-meaning-r}}\,({\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, {\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}:  loop-sub1-body-doesnt-halt \\ \index{loop-sub1-body-doesnt-halt}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{loop-mg}}) \\ 
$\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{normal}}\,({\rm{mg-meaning-r}}\,({\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}} $-\;1$, {\it{sizes\/}})\index{mg-meaning-r})\index{normal})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{mg-psw}}\,({\rm{mg-meaning-r}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{mg-meaning-r}}\,(\=\+{\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{sizes\/}})\-\index{mg-meaning-r}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{sizes\/}})\-\index{mg-meaning-r})\index{mg-psw} \\ 
$=$$\;\;\;\;${\tt{'}}{\tt{run}})\-\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  clock-equivalence-loop-case \\ \index{clock-equivalence-loop-case}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{loop-mg}}) \\ 
$\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}))\- \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{resource-errorp}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{sizes\/}})\-\index{mg-meaning-r})\index{resource-errorp})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  loop-body-exact-time-hyps \\ \index{loop-body-exact-time-hyps}
\=\+(\=\+({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resources-inadequatep}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{resources-inadequatep}) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{loop-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{r-cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-translation-parameters}}\,({\it{cinfo\/}}, {\it{t-cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}}, {\it{code2\/}})\index{ok-translation-parameters} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statep}}\,({\it{mg-state\/}}, {\it{r-cond-list\/}})\index{ok-mg-statep} \\ 
$\wedge$$\;\;\;\;${\rm{cond-subsetp}}\,({\it{r-cond-list\/}}, {\it{t-cond-list\/}})\index{cond-subsetp} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{code}}\,({\rm{translate-def-body}}\,({\rm{assoc}}\,({\it{subr\/}}, {\it{proc-list\/}}), {\it{proc-list\/}})\index{translate-def-body})\index{code} \\ 
$=$$\;\;\;\;${\rm{append}}\,(\=\+{\rm{code}}\,({\rm{translate}}\,({\it{cinfo\/}}, {\it{t-cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}})\index{translate})\index{code}, \\ 
{\it{code2\/}})\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{user-defined-procp}}\,({\it{subr\/}}, {\it{proc-list\/}})\index{user-defined-procp} \\ 
$\wedge$$\;\;\;\;${\rm{plistp}}\,({\it{temp-stk\/}})\index{plistp} \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\it{ctrl-stk\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,(\=\+{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, \\ 
{\it{temp-stk\/}})\-\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, {\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match} \\ 
$\wedge$$\;\;\;\;${\rm{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resource-errorp}}\,({\rm{mg-meaning-r}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{resource-errorp}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{ok-mg-statement}}\,(\=\+{\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, \\ 
{\rm{cons}}\,({\tt{'}}{\tt{leave}}, {\it{r-cond-list\/}}), \\ 
{\it{name-alist\/}}, \\ 
{\it{proc-list\/}})\-\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-translation-parameters}}\,(\=\+{\rm{make-cinfo}}\,(\=\+{\rm{append}}\,(\=\+{\rm{code}}\,({\it{cinfo\/}})\index{code}, \\ 
{\rm{list}}\,({\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{cons}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{leave}}, \\ 
$1\;+$ {\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{loop-body}}\,({\it{stmt\/}})\index{loop-body}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{cons}}\,(\=\+{\rm{list}}\,({\tt{'}}{\tt{jump}}, {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}), \\ 
{\rm{cons}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{dl}}, \\ 
{\rm{cons}}\,(\=\+$1\;+$ {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}, \\ 
{\tt{'}}{\tt{(}}\=\+{\tt{nil}} \\ 
{\tt{(}}\=\+{\tt{push-constant}} \\ 
{\tt{(}}{\tt{nat}}{\tt{ }}{\tt{2}}{\tt{)}}{\tt{)}}\-{\tt{)}}\-)\-)\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}\=\+{\tt{pop-global}}{\tt{ }}{\tt{c-c}}{\tt{)}}\-, \\ 
{\it{code2\/}})\-)\-)\-)\-\index{ok-translation-parameters} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statep}}\,({\it{mg-state\/}}, {\rm{cons}}\,({\tt{'}}{\tt{leave}}, {\it{r-cond-list\/}}))\index{ok-mg-statep} \\ 
$\wedge$$\;\;\;\;${\rm{cond-subsetp}}\,({\rm{cons}}\,({\tt{'}}{\tt{leave}}, {\it{r-cond-list\/}}), {\it{t-cond-list\/}})\index{cond-subsetp} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{code}}\,({\rm{translate-def-body}}\,({\rm{assoc}}\,({\it{subr\/}}, {\it{proc-list\/}}), {\it{proc-list\/}})\index{translate-def-body})\index{code} \\ 
$=$$\;\;\;\;${\rm{append}}\,(\=\+{\rm{code}}\,({\rm{translate}}\,(\=\+{\rm{make-cinfo}}\,(\=\+{\rm{append}}\,(\=\+{\rm{code}}\,({\it{cinfo\/}})\index{code}, \\ 
{\rm{list}}\,({\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{cons}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{leave}}, \\ 
$1\;+$ {\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{loop-body}}\,({\it{stmt\/}})\index{loop-body}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code}, \\ 
{\rm{cons}}\,(\=\+{\rm{list}}\,({\tt{'}}{\tt{jump}}, {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}), \\ 
{\rm{cons}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{dl}}, \\ 
{\rm{cons}}\,(\=\+$1\;+$ {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}, \\ 
{\tt{'}}{\tt{(}}\=\+{\tt{nil}} \\ 
{\tt{(}}\=\+{\tt{push-constant}} \\ 
{\tt{(}}{\tt{nat}}{\tt{ }}{\tt{2}}{\tt{)}}{\tt{)}}\-{\tt{)}}\-)\-)\-, \\ 
{\rm{cons}}\,({\tt{'}}{\tt{(}}{\tt{pop-global}}{\tt{ }}{\tt{c-c}}{\tt{)}}, {\it{code2\/}}))\-)\-)\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{user-defined-procp}}\,({\it{subr\/}}, {\it{proc-list\/}})\index{user-defined-procp} \\ 
$\wedge$$\;\;\;\;${\rm{plistp}}\,({\it{temp-stk\/}})\index{plistp} \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\it{ctrl-stk\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,(\=\+{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, \\ 
{\it{temp-stk\/}})\-\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, {\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match} \\ 
$\wedge$$\;\;\;\;${\rm{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resource-errorp}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, \\ 
{\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}:  cond-list-superset-preserves-ok-mg-statement \\ \index{cond-list-superset-preserves-ok!-mg-statement}
\=\+(\=\+{\rm{subset}}\,({\it{cond-list1\/}}, {\it{cond-list2\/}})\index{subset} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{cond-list1\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{cond-list2\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  adding-leave-preserves-statement-okness-begin-case \\ \index{adding-leave-preserves-statement!-okness-begin-case}
\=\+{\rm{ok-mg-statement}}\,(\=\+{\rm{begin-body}}\,({\it{stmt\/}})\index{begin-body}, \\ 
{\rm{cons}}\,({\tt{'}}{\tt{leave}}, {\rm{append}}\,({\rm{when-labels}}\,({\it{stmt\/}})\index{when-labels}, {\it{cond-list\/}})), \\ 
{\it{name-alist\/}}, \\ 
{\it{proc-list\/}})\-\index{ok-mg-statement} \\ 
$\rightarrow$$\;\;\;\;${\rm{ok-mg-statement}}\,(\=\+{\rm{begin-body}}\,({\it{stmt\/}})\index{begin-body}, \\ 
{\rm{append}}\,({\rm{when-labels}}\,({\it{stmt\/}})\index{when-labels}, {\rm{cons}}\,({\tt{'}}{\tt{leave}}, {\it{cond-list\/}})), \\ 
{\it{name-alist\/}}, \\ 
{\it{proc-list\/}})\-\index{ok-mg-statement}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  adding-leave-preserves-statement-okness \\ \index{adding-leave-preserves-statement!-okness}
\=\+{\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\rightarrow$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\rm{cons}}\,({\tt{'}}{\tt{leave}}, {\it{cond-list\/}}), {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  loop-sub1-body-exact-time-hyps \\ \index{loop-sub1-body-exact-time-hyps}
\=\+(\=\+({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resources-inadequatep}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{resources-inadequatep}) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{loop-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{r-cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-translation-parameters}}\,({\it{cinfo\/}}, {\it{t-cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}}, {\it{code2\/}})\index{ok-translation-parameters} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statep}}\,({\it{mg-state\/}}, {\it{r-cond-list\/}})\index{ok-mg-statep} \\ 
$\wedge$$\;\;\;\;${\rm{cond-subsetp}}\,({\it{r-cond-list\/}}, {\it{t-cond-list\/}})\index{cond-subsetp} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{code}}\,({\rm{translate-def-body}}\,({\rm{assoc}}\,({\it{subr\/}}, {\it{proc-list\/}}), {\it{proc-list\/}})\index{translate-def-body})\index{code} \\ 
$=$$\;\;\;\;${\rm{append}}\,(\=\+{\rm{code}}\,({\rm{translate}}\,({\it{cinfo\/}}, {\it{t-cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}})\index{translate})\index{code}, \\ 
{\it{code2\/}})\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{user-defined-procp}}\,({\it{subr\/}}, {\it{proc-list\/}})\index{user-defined-procp} \\ 
$\wedge$$\;\;\;\;${\rm{plistp}}\,({\it{temp-stk\/}})\index{plistp} \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\it{ctrl-stk\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,(\=\+{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, \\ 
{\it{temp-stk\/}})\-\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, {\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match} \\ 
$\wedge$$\;\;\;\;${\rm{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resource-errorp}}\,({\rm{mg-meaning-r}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{resource-errorp}) \\ 
$\wedge$$\;\;\;\;${\rm{normal}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, \\ 
{\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{ok-mg-statement}}\,({\it{stmt\/}}, {\rm{cons}}\,({\tt{'}}{\tt{leave}}, {\it{r-cond-list\/}}), {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-translation-parameters}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{code2\/}})\-\index{ok-translation-parameters} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statep}}\,(\=\+{\rm{mg-meaning-r}}\,(\=\+{\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, \\ 
{\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}, \\ 
{\rm{cons}}\,({\tt{'}}{\tt{leave}}, {\it{r-cond-list\/}}))\-\index{ok-mg-statep} \\ 
$\wedge$$\;\;\;\;${\rm{cond-subsetp}}\,({\rm{cons}}\,({\tt{'}}{\tt{leave}}, {\it{r-cond-list\/}}), {\it{t-cond-list\/}})\index{cond-subsetp} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{code}}\,({\rm{translate-def-body}}\,({\rm{assoc}}\,({\it{subr\/}}, {\it{proc-list\/}}), {\it{proc-list\/}})\index{translate-def-body})\index{code} \\ 
$=$$\;\;\;\;${\rm{append}}\,(\=\+{\rm{code}}\,({\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code}, \\ 
{\it{code2\/}})\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{user-defined-procp}}\,({\it{subr\/}}, {\it{proc-list\/}})\index{user-defined-procp} \\ 
$\wedge$$\;\;\;\;${\rm{plistp}}\,({\it{temp-stk\/}})\index{plistp} \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\it{ctrl-stk\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,(\=\+{\rm{mg-alist}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, \\ 
{\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{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,(\=\+{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, \\ 
{\rm{mg-alist}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, \\ 
{\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})\-\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,(\=\+{\rm{mg-alist}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, \\ 
{\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}, \\ 
{\it{name-alist\/}})\-\index{signatures-match} \\ 
$\wedge$$\;\;\;\;${\rm{normal}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, \\ 
{\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} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, \\ 
{\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})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resource-errorp}}\,({\rm{mg-meaning-r}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{mg-meaning-r}}\,(\=\+{\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, \\ 
{\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}, \\ 
{\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}:  loop-clock-nonnormal-nonleave \\ \index{loop-clock-nonnormal-nonleave}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{loop-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{normal}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{sizes\/}})\-\index{mg-meaning-r})\index{normal}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{cc}}\,({\rm{mg-meaning-r}}\,({\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}} $-\;1$, {\it{sizes\/}})\index{mg-meaning-r})\index{cc} \\ 
$\not=$$\;\;\;\;${\tt{'}}{\tt{leave}})\-)\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{clock}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}})\index{clock} \\ 
$=$$\;\;\;\;$($1\;+$ {\rm{clock}}\,({\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}} $-\;1$)\index{clock}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  loop-clock-normal \\ \index{loop-clock-normal}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{loop-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{normal}}\,({\rm{mg-meaning-r}}\,({\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, {\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} \\ 
$=$$\;\;\;\;$($1\;+$ (\=\+($1\;+$ {\rm{clock}}\,({\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}} $-\;1$)\index{clock}) \\ 
$+$$\;\;\;\;${\rm{clock}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{mg-meaning-r}}\,(\=\+{\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{sizes\/}})\-\index{mg-meaning-r}, \\ 
{\it{n\/}} $-\;1$)\-\index{clock})\-))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  loop-clock-nonnormal-leave \\ \index{loop-clock-nonnormal-leave}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{loop-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{normal}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{sizes\/}})\-\index{mg-meaning-r})\index{normal}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{cc}}\,({\rm{mg-meaning-r}}\,({\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}} $-\;1$, {\it{sizes\/}})\index{mg-meaning-r})\index{cc} \\ 
$=$$\;\;\;\;${\tt{'}}{\tt{leave}})\-)\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{clock}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}})\index{clock} \\ 
$=$$\;\;\;\;$({\tt{3}} $+$ {\rm{clock}}\,({\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}} $-\;1$)\index{clock}))\-\-
\end{tabbing}
	    
\begin{tabbing}{\sc Theorem}:  loop-step-initial-equals-state1 \\ \index{loop-step-initial-equals-state1}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{loop-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{r-cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-translation-parameters}}\,({\it{cinfo\/}}, {\it{t-cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}}, {\it{code2\/}})\index{ok-translation-parameters} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{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})\- \\ 
$\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{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{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{cons}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{leave}}, \\ 
$1\;+$ {\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}

\begin{tabbing}{\sc Theorem}:  nonleave-nonnormal-body-meaning-preserved \\ \index{nonleave-nonnormal-body-meaning!-preserved}
\=\+(\=\+({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;${\rm{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{loop-mg}}) \\ 
$\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{normal}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{sizes\/}})\-\index{mg-meaning-r})\index{normal}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{cc}}\,({\rm{mg-meaning-r}}\,({\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}} $-\;1$, {\it{sizes\/}})\index{mg-meaning-r})\index{cc} \\ 
$\not=$$\;\;\;\;${\tt{'}}{\tt{leave}})\-)\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{mg-meaning-r}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}}, {\it{sizes\/}})\index{mg-meaning-r} \\ 
$=$$\;\;\;\;${\rm{mg-meaning-r}}\,({\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}} $-\;1$, {\it{sizes\/}})\index{mg-meaning-r})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  loop-code-rewrite \\ \index{loop-code-rewrite}
\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{loop-mg}}) \\ 
$\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{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{cons}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{leave}}, \\ 
$1\;+$ {\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{loop-body}}\,({\it{stmt\/}})\index{loop-body}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code}, \\ 
{\rm{cons}}\,(\=\+{\rm{list}}\,({\tt{'}}{\tt{jump}}, {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}), \\ 
{\rm{cons}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{dl}}, \\ 
{\rm{cons}}\,(\=\+$1\;+$ {\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt}, \\ 
{\tt{'}}{\tt{(}}\=\+{\tt{nil}} \\ 
{\tt{(}}{\tt{push-constant}}{\tt{ }}{\tt{(}}{\tt{nat}}{\tt{ }}{\tt{2}}{\tt{)}}{\tt{)}}{\tt{)}}\-)\-)\-, \\ 
{\rm{cons}}\,({\tt{'}}{\tt{(}}{\tt{pop-global}}{\tt{ }}{\tt{c-c}}{\tt{)}}, {\it{code2\/}}))\-)\-)\-)\-\-
\end{tabbing}

%\item 
\begin{verbatim}


(prove-lemma loop-nonnormal-nonleave-state2-equals-final (rewrite)
       (IMPLIES
	(AND (NOT (ZEROP N))
	     (equal (car STMT) 'LOOP-MG)
	     (NORMAL 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 (NORMAL (MG-MEANING-R (LOOP-BODY STMT) proc-list MG-STATE (sub1 n)
					(list (length temp-stk) (p-ctrl-stk-size ctrl-stk)))))
	     (not (equal (cc (MG-MEANING-R (LOOP-BODY STMT) proc-list MG-STATE (sub1 N)
					   (list (length temp-stk) (p-ctrl-stk-size ctrl-stk))))
			 'leave)))
	(equal 
	 (P-STATE
	  (TAG 'PC
	       (CONS SUBR
		     (IF
		      (NORMAL (MG-MEANING-R (LOOP-BODY 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 (CONS 'DL
								   (CONS (LABEL-CNT CINFO)
									 '(NIL (NO-OP))))))
					       (CONS (CONS 'LEAVE
							   (ADD1 (LABEL-CNT CINFO)))
						     (LABEL-ALIST CINFO))
					       (ADD1 (ADD1 (LABEL-CNT CINFO))))
				   T-COND-LIST
				   (LOOP-BODY STMT)
				   PROC-LIST)))
		      (FIND-LABEL
		       (FETCH-LABEL
			(CC (MG-MEANING-R (LOOP-BODY 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 (CONS 'DL
								    (CONS (LABEL-CNT CINFO)
									  '(NIL (NO-OP))))))
						(CONS (CONS 'LEAVE
							    (ADD1 (LABEL-CNT CINFO)))
						      (LABEL-ALIST CINFO))
						(ADD1 (ADD1 (LABEL-CNT CINFO))))
				    T-COND-LIST
				    (LOOP-BODY STMT)
				    PROC-LIST)))
		       (APPEND
			(CODE
			 (TRANSLATE (MAKE-CINFO (APPEND (CODE CINFO)
							(LIST (CONS 'DL
								    (CONS (LABEL-CNT CINFO)
									  '(NIL (NO-OP))))))
						(CONS (CONS 'LEAVE
							    (ADD1 (LABEL-CNT CINFO)))
						      (LABEL-ALIST CINFO))
						(ADD1 (ADD1 (LABEL-CNT CINFO))))
				    T-COND-LIST
				    (LOOP-BODY STMT)
				    PROC-LIST))
			(CONS (LIST 'JUMP (LABEL-CNT CINFO))
			      (CONS (CONS 'DL
					  (CONS (ADD1 (LABEL-CNT CINFO))
						'(NIL (PUSH-CONSTANT (NAT 2)))))
				    (CONS '(POP-GLOBAL C-C) CODE2))))))))
	  CTRL-STK
	  (MAP-DOWN-VALUES
	   (MG-ALIST (MG-MEANING-R (LOOP-BODY 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 (LOOP-BODY 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;; 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 PROMOTE
            (= (MG-MEANING-R STMT PROC-LIST MG-STATE N
                             (LIST (LENGTH TEMP-STK)
                                   (P-CTRL-STK-SIZE CTRL-STK)))
               (MG-MEANING-R (LOOP-BODY STMT)
                             PROC-LIST MG-STATE
                             (SUB1 N)
                             (LIST (LENGTH TEMP-STK)
                                   (P-CTRL-STK-SIZE CTRL-STK)))
               0)
            S
            (S LEMMAS)
            (ENABLE DISCARD-LABEL ADD-CODE)
            S
            (DIVE 2 2 2 1 1 2 1)
            TOP
            (S LEMMAS)
            (DIVE 1 2 2 1 1)
            X TOP S
            (DIVE 1)
            (REWRITE NONLEAVE-NONNORMAL-BODY-MEANING-PRESERVED)
            TOP S)))
\end{verbatim}


\begin{tabbing}{\sc Theorem}:  loop-leave-body-meaning-preserved \\ \index{loop-leave-body-meaning-preserve!d}
\=\+(\=\+({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;${\rm{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{loop-mg}}) \\ 
$\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{cc}}\,({\rm{mg-meaning-r}}\,({\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}} $-\;1$, {\it{sizes\/}})\index{mg-meaning-r})\index{cc} \\ 
$=$$\;\;\;\;${\tt{'}}{\tt{leave}})\-)\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{mg-meaning-r}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}}, {\it{sizes\/}})\index{mg-meaning-r} \\ 
$=$$\;\;\;\;${\rm{set-condition}}\,(\=\+{\rm{mg-meaning-r}}\,(\=\+{\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{sizes\/}})\-\index{mg-meaning-r}, \\ 
{\tt{'}}{\tt{normal}})\-\index{set-condition})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  loop-find-labelp-lemma1 \\ \index{loop-find-labelp-lemma1}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{loop-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{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{cons}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{leave}}, \\ 
$1\;+$ {\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{loop-body}}\,({\it{stmt\/}})\index{loop-body}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code})\-\index{find-labelp})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  loop-find-labelp-lemma2 \\ \index{loop-find-labelp-lemma2}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{loop-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}}\,({\it{cinfo\/}})\index{code})\index{find-labelp})\-
\end{tabbing}

%\item 
\begin{verbatim}


(prove-lemma loop-leave-state2-step1-effect (rewrite)
      (IMPLIES 
       (AND (NOT (ZEROP N))
	    (NOT (RESOURCES-INADEQUATEP STMT PROC-LIST
					(LIST (LENGTH TEMP-STK)
					      (P-CTRL-STK-SIZE CTRL-STK))))
	    (EQUAL (CAR STMT) 'LOOP-MG)
	    (OK-MG-STATEMENT STMT R-COND-LIST NAME-ALIST PROC-LIST)
	    (OK-MG-DEF-PLISTP PROC-LIST)
	    (OK-TRANSLATION-PARAMETERS CINFO T-COND-LIST STMT PROC-LIST CODE2)
	    (OK-MG-STATEP MG-STATE R-COND-LIST)
	    (COND-SUBSETP R-COND-LIST T-COND-LIST)
	    (EQUAL (CODE (TRANSLATE-DEF-BODY (ASSOC SUBR PROC-LIST)
					     PROC-LIST))
		   (APPEND (CODE (TRANSLATE CINFO T-COND-LIST STMT PROC-LIST))
			   CODE2))
	    (USER-DEFINED-PROCP SUBR PROC-LIST)
	    (PLISTP TEMP-STK)
	    (LISTP CTRL-STK)
	    (MG-VARS-LIST-OK-IN-P-STATE (MG-ALIST MG-STATE)
					(BINDINGS (TOP CTRL-STK))
					TEMP-STK)
	    (NO-P-ALIASING (BINDINGS (TOP CTRL-STK))
			   (MG-ALIST MG-STATE))
	    (SIGNATURES-MATCH (MG-ALIST MG-STATE)
			      NAME-ALIST)
	    (NORMAL MG-STATE)
	    (ALL-CARS-UNIQUE (MG-ALIST MG-STATE))
	    (NOT (RESOURCE-ERRORP (MG-MEANING-R STMT PROC-LIST MG-STATE N
						(LIST (LENGTH TEMP-STK)
						      (P-CTRL-STK-SIZE CTRL-STK)))))
            (equal (cc (mg-meaning-r (loop-body stmt) proc-list mg-state (sub1 n) 
				     (list (length temp-stk)
					   (p-ctrl-stk-size ctrl-stk))))
		   'leave))
      (equal 
       (p-step
 	(P-STATE
	 (TAG 'PC
	      (CONS SUBR
		    (IF (NORMAL (MG-MEANING-R (LOOP-BODY 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 (CONS 'DL
								     (CONS (LABEL-CNT CINFO)
									   '(NIL (NO-OP))))))
						 (CONS (CONS 'LEAVE
							     (ADD1 (LABEL-CNT CINFO)))
						       (LABEL-ALIST CINFO))
						 (ADD1 (ADD1 (LABEL-CNT CINFO))))
				     T-COND-LIST
				     (LOOP-BODY STMT)
				     PROC-LIST)))
			(FIND-LABEL
			 (FETCH-LABEL
			  (CC (MG-MEANING-R (LOOP-BODY 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 (CONS 'DL
								      (CONS (LABEL-CNT CINFO)
									    '(NIL (NO-OP))))))
						  (CONS (CONS 'LEAVE
							      (ADD1 (LABEL-CNT CINFO)))
							(LABEL-ALIST CINFO))
						  (ADD1 (ADD1 (LABEL-CNT CINFO))))
				      T-COND-LIST
				      (LOOP-BODY STMT)
				      PROC-LIST)))
			 (APPEND
			  (CODE
			   (TRANSLATE (MAKE-CINFO (APPEND (CODE CINFO)
							  (LIST (CONS 'DL
								      (CONS (LABEL-CNT CINFO)
									    '(NIL (NO-OP))))))
						  (CONS (CONS 'LEAVE
							      (ADD1 (LABEL-CNT CINFO)))
							(LABEL-ALIST CINFO))
						  (ADD1 (ADD1 (LABEL-CNT CINFO))))
				      T-COND-LIST
				      (LOOP-BODY STMT)
				      PROC-LIST))
			  (CONS (LIST 'JUMP (LABEL-CNT CINFO))
				(CONS (CONS 'DL
					    (CONS (ADD1 (LABEL-CNT CINFO))
						  '(NIL (PUSH-CONSTANT (NAT 2)))))
				      (CONS '(POP-GLOBAL C-C) CODE2))))))))
	 CTRL-STK
	 (MAP-DOWN-VALUES
	  (MG-ALIST (MG-MEANING-R (LOOP-BODY 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 (LOOP-BODY 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 (CONS 'DL
								    (CONS (LABEL-CNT CINFO)
									  '(NIL (NO-OP))))))
						(CONS (CONS 'LEAVE
							    (ADD1 (LABEL-CNT CINFO)))
						      (LABEL-ALIST CINFO))
						(ADD1 (ADD1 (LABEL-CNT CINFO))))
				    T-COND-LIST
				    (LOOP-BODY STMT)
				    PROC-LIST)))
		  2)))
      CTRL-STK
      (PUSH '(NAT 2)
	    (MAP-DOWN-VALUES (MG-ALIST (MG-MEANING-R (LOOP-BODY 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 'LEAVE T-COND-LIST)))
      (MG-MAX-CTRL-STK-SIZE)
      (MG-MAX-TEMP-STK-SIZE)
      (MG-WORD-SIZE)
      'RUN)))
 ((INSTRUCTIONS PROMOTE
                (DIVE 1)
                S
                (= (CC (MG-MEANING-R (LOOP-BODY STMT)
                                     PROC-LIST MG-STATE
                                     (SUB1 N)
                                     (CONS (LENGTH TEMP-STK)
                                           (CONS (P-CTRL-STK-SIZE CTRL-STK)
                                                 'NIL))))
                   'LEAVE
                   0)
                S
                (S LEMMAS)
                (DIVE 1 1 1 2 2)
                (REWRITE FIND-LABEL-APPEND)
                (DIVE 2)
                X
                (DIVE 1)
                X UP TOP
                (DIVE 1)
                S
                (S LEMMAS)
                (DIVE 1 1 2)
                (REWRITE TRANSLATE-DEF-BODY-REWRITE)
                (DIVE 1 1)
                (REWRITE LOOP-TRANSLATION-2)
                UP
                (S LEMMAS)
                UP UP
                (S LEMMAS)
                (REWRITE GET-LENGTH-PLUS)
                X UP
                (S LEMMAS)
                UP X
                (DIVE 1)
                X
                (DIVE 1)
                (REWRITE MAP-DOWN-VALUES-PRESERVES-LENGTH)
                UP
                (REWRITE RESOURCES-ADEQUATE-TEMP-STK-NOT-MAX)
                UP S X
                (S LEMMAS)
                (DIVE 1 2 2 1)
                (REWRITE FIND-LABEL-APPEND)
                (DIVE 2)
                X
                (DIVE 1)
                X TOP
                (S LEMMAS)
                (DIVE 1)
                (REWRITE LOOP-FIND-LABELP-LEMMA1)
                TOP S
                (DIVE 1 1)
                (REWRITE MG-MEANING-EQUIVALENCE)
                TOP
                (REWRITE SIGNATURES-MATCH-PRESERVES-MG-VARS-LIST-OK
                         (($X (MG-ALIST MG-STATE))))
                (REWRITE MG-MEANING-PRESERVES-SIGNATURES-MATCH)
                (REWRITE OK-MG-STATEP-ALIST-PLISTP)
                (PROVE (ENABLE LOOP-BODY-DOESNT-HALT))
                (DIVE 1 1)
                (REWRITE MG-MEANING-EQUIVALENCE)
                TOP
                (REWRITE MG-MEANING-PRESERVES-MG-ALISTP
                         (($R-COND-LIST (CONS 'LEAVE R-COND-LIST))))
                (REWRITE LOOP-BODY-EXACT-TIME-HYPS)
                (REWRITE OK-LOOP-STATEMENT)
                (PROVE (ENABLE LOOP-BODY-DOESNT-HALT))
                (DIVE 1)
                (REWRITE LOOP-FIND-LABELP-LEMMA1)
                TOP S)))
\end{verbatim}


%\item 
\begin{verbatim}


(prove-lemma loop-leave-state2-step2-effect (rewrite)
      (IMPLIES 
       (AND (NOT (ZEROP N))
	    (NOT (RESOURCES-INADEQUATEP STMT PROC-LIST
					(LIST (LENGTH TEMP-STK)
					      (P-CTRL-STK-SIZE CTRL-STK))))
	    (EQUAL (CAR STMT) 'LOOP-MG)
	    (OK-MG-STATEMENT STMT R-COND-LIST NAME-ALIST PROC-LIST)
	    (OK-MG-DEF-PLISTP PROC-LIST)
	    (OK-TRANSLATION-PARAMETERS CINFO T-COND-LIST STMT PROC-LIST CODE2)
	    (OK-MG-STATEP MG-STATE R-COND-LIST)
	    (COND-SUBSETP R-COND-LIST T-COND-LIST)
	    (EQUAL (CODE (TRANSLATE-DEF-BODY (ASSOC SUBR PROC-LIST)
					     PROC-LIST))
		   (APPEND (CODE (TRANSLATE CINFO T-COND-LIST STMT PROC-LIST))
			   CODE2))
	    (USER-DEFINED-PROCP SUBR PROC-LIST)
	    (PLISTP TEMP-STK)
	    (LISTP CTRL-STK)
	    (MG-VARS-LIST-OK-IN-P-STATE (MG-ALIST MG-STATE)
					(BINDINGS (TOP CTRL-STK))
					TEMP-STK)
	    (NO-P-ALIASING (BINDINGS (TOP CTRL-STK))
			   (MG-ALIST MG-STATE))
	    (SIGNATURES-MATCH (MG-ALIST MG-STATE)
			      NAME-ALIST)
	    (NORMAL MG-STATE)
	    (ALL-CARS-UNIQUE (MG-ALIST MG-STATE))
	    (NOT (RESOURCE-ERRORP (MG-MEANING-R STMT PROC-LIST MG-STATE N
						(LIST (LENGTH TEMP-STK)
						      (P-CTRL-STK-SIZE CTRL-STK)))))
            (equal (cc (mg-meaning-r (loop-body stmt) proc-list mg-state (sub1 n) 
				     (list (length temp-stk)
					   (p-ctrl-stk-size ctrl-stk))))
		   'leave))
       (equal 
	(p-step
         (P-STATE
	  (TAG 'PC
	       (CONS SUBR
		     (PLUS
		      (LENGTH
		       (CODE (TRANSLATE (MAKE-CINFO (APPEND (CODE CINFO)
							    (LIST (CONS 'DL
									(CONS (LABEL-CNT CINFO)
									      '(NIL (NO-OP))))))
						    (CONS (CONS 'LEAVE
								(ADD1 (LABEL-CNT CINFO)))
							  (LABEL-ALIST CINFO))
						    (ADD1 (ADD1 (LABEL-CNT CINFO))))
					T-COND-LIST
					(LOOP-BODY STMT)
					PROC-LIST)))
		      2)))
	  CTRL-STK
	  (PUSH '(NAT 2)
		(MAP-DOWN-VALUES (MG-ALIST (MG-MEANING-R (LOOP-BODY 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 'LEAVE T-COND-LIST)))
	  (MG-MAX-CTRL-STK-SIZE)
	  (MG-MAX-TEMP-STK-SIZE)
	  (MG-WORD-SIZE)
	  'RUN))
      (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 PROMOTE
             (DIVE 1)
             X
             (S LEMMAS)
             (DIVE 1 1 2)
             (REWRITE TRANSLATE-DEF-BODY-REWRITE)
             (REWRITE LOOP-CODE-REWRITE)
             UP
             (REWRITE GET-LENGTH-PLUS)
             X X UP X UP X
             (DIVE 1)
             X UP S-PROP X
             (S LEMMAS)
             S UP S
             (= (MG-MEANING-R STMT PROC-LIST MG-STATE N
                              (LIST (LENGTH TEMP-STK)
                                    (P-CTRL-STK-SIZE CTRL-STK)))
                (SET-CONDITION (MG-MEANING-R (LOOP-BODY STMT)
                                             PROC-LIST MG-STATE
                                             (SUB1 N)
                                             (LIST (LENGTH TEMP-STK)
                                                   (P-CTRL-STK-SIZE CTRL-STK)))
                               'NORMAL)
                0)
             SPLIT
             (ENABLE MG-COND-TO-P-NAT)
             S S
             (ENABLE LENGTH-CONS)
             (S LEMMAS)
             S
             (DIVE 1)
             (REWRITE LOOP-LEAVE-BODY-MEANING-PRESERVED)
             TOP S)))
\end{verbatim}


%\item 
\begin{verbatim}


(prove-lemma loop-normal-body-step-state2-equals-state3 (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) 'LOOP-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)))))
            (normal (mg-meaning-r (loop-body 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 (LOOP-BODY 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 (CONS 'DL
								   (CONS (LABEL-CNT CINFO)
									 '(NIL (NO-OP))))))
					       (CONS (CONS 'LEAVE
							   (ADD1 (LABEL-CNT CINFO)))
						     (LABEL-ALIST CINFO))
					       (ADD1 (ADD1 (LABEL-CNT CINFO))))
				   T-COND-LIST
				   (LOOP-BODY STMT)
				   PROC-LIST)))
		      (FIND-LABEL
		       (FETCH-LABEL
			(CC (MG-MEANING-R (LOOP-BODY 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 (CONS 'DL
								    (CONS (LABEL-CNT CINFO)
									  '(NIL (NO-OP))))))
						(CONS (CONS 'LEAVE
							    (ADD1 (LABEL-CNT CINFO)))
						      (LABEL-ALIST CINFO))
						(ADD1 (ADD1 (LABEL-CNT CINFO))))
				    T-COND-LIST
				    (LOOP-BODY STMT)
				    PROC-LIST)))
		       (APPEND
			(CODE
			 (TRANSLATE (MAKE-CINFO (APPEND (CODE CINFO)
							(LIST (CONS 'DL
								    (CONS (LABEL-CNT CINFO)
									  '(NIL (NO-OP))))))
						(CONS (CONS 'LEAVE
							    (ADD1 (LABEL-CNT CINFO)))
						      (LABEL-ALIST CINFO))
						(ADD1 (ADD1 (LABEL-CNT CINFO))))
				    T-COND-LIST
				    (LOOP-BODY STMT)
				    PROC-LIST))
			(CONS (LIST 'JUMP (LABEL-CNT CINFO))
			      (CONS (CONS 'DL
					  (CONS (ADD1 (LABEL-CNT CINFO))
						'(NIL (PUSH-CONSTANT (NAT 2)))))
				    (CONS '(POP-GLOBAL C-C) CODE2))))))))
	  CTRL-STK
	  (MAP-DOWN-VALUES
	   (MG-ALIST (MG-MEANING-R (LOOP-BODY 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 (LOOP-BODY 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))
	(MAP-DOWN (MG-MEANING-R (LOOP-BODY STMT);; state3
				PROC-LIST MG-STATE
				(SUB1 N)
				(LIST (LENGTH TEMP-STK)
				      (P-CTRL-STK-SIZE CTRL-STK)))
		  PROC-LIST CTRL-STK TEMP-STK
		  (TAG 'PC
		       (CONS SUBR (LENGTH (CODE CINFO))))
		  T-COND-LIST)))
     ((INSTRUCTIONS
       PROMOTE (DIVE 1) S X (S LEMMAS) (DIVE 1 1 2) (REWRITE TRANSLATE-DEF-BODY-REWRITE)
       (REWRITE LOOP-CODE-REWRITE) UP (REWRITE GET-LENGTH-CAR) S UP (ENABLE LABELLEDP)
       X UP X (DIVE 1) X UP S-PROP X (S LEMMAS) (DIVE 1 2 1) (REWRITE DEFINEDP-CAR-ASSOC)
       NX (DIVE 2) (REWRITE TRANSLATE-DEF-BODY-REWRITE) (REWRITE LOOP-CODE-REWRITE) (DIVE 1)
       (REWRITE NEW-CODE-APPENDED-TO-OLD1) UP UP (S LEMMAS) (REWRITE FIND-LABEL-APPEND) 
       (DIVE 2) X UP (REWRITE PLUS-0-REWRITE) S TOP S (DIVE 1) 
       (REWRITE LOOP-FIND-LABELP-LEMMA2) TOP S PROVE (REWRITE CAR-DEFINEDP-DEFINED-PROCP))))
\end{verbatim}


\begin{tabbing}{\sc Theorem}:  loop-never-leave \\ \index{loop-never-leave}
\=\+(({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{loop-mg}}) $\wedge$ {\rm{normal}}\,({\it{mg-state\/}})\index{normal}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{cc}}\,({\rm{mg-meaning-r}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}}, {\it{sizes\/}})\index{mg-meaning-r})\index{cc} $\not=$ {\tt{'}}{\tt{leave}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  loop-normal-body-state4-equals-final \\ \index{loop-normal-body-state4-equals-!final}
\=\+(\=\+({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resources-inadequatep}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{resources-inadequatep}) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{loop-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{r-cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-translation-parameters}}\,({\it{cinfo\/}}, {\it{t-cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}}, {\it{code2\/}})\index{ok-translation-parameters} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statep}}\,({\it{mg-state\/}}, {\it{r-cond-list\/}})\index{ok-mg-statep} \\ 
$\wedge$$\;\;\;\;${\rm{cond-subsetp}}\,({\it{r-cond-list\/}}, {\it{t-cond-list\/}})\index{cond-subsetp} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{code}}\,({\rm{translate-def-body}}\,({\rm{assoc}}\,({\it{subr\/}}, {\it{proc-list\/}}), {\it{proc-list\/}})\index{translate-def-body})\index{code} \\ 
$=$$\;\;\;\;${\rm{append}}\,(\=\+{\rm{code}}\,({\rm{translate}}\,({\it{cinfo\/}}, {\it{t-cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}})\index{translate})\index{code}, \\ 
{\it{code2\/}})\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{user-defined-procp}}\,({\it{subr\/}}, {\it{proc-list\/}})\index{user-defined-procp} \\ 
$\wedge$$\;\;\;\;${\rm{plistp}}\,({\it{temp-stk\/}})\index{plistp} \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\it{ctrl-stk\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,(\=\+{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, \\ 
{\it{temp-stk\/}})\-\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, {\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match} \\ 
$\wedge$$\;\;\;\;${\rm{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resource-errorp}}\,({\rm{mg-meaning-r}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{resource-errorp}) \\ 
$\wedge$$\;\;\;\;${\rm{normal}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, \\ 
{\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-state}}\,(\=\+{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,(\=\+{\it{subr\/}}, \\ 
\=\+{\bf if }{\rm{normal}}\,({\rm{mg-meaning-r}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{mg-meaning-r}}\,(\=\+{\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, \\ 
{\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}, \\ 
{\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} \\ 
{\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\/}}, \\ 
{\rm{mg-meaning-r}}\,(\=\+{\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, \\ 
{\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}, \\ 
{\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}, \\ 
{\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\/}}, \\ 
{\rm{mg-meaning-r}}\,(\=\+{\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, \\ 
{\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}, \\ 
{\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}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{mg-meaning-r}}\,(\=\+{\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, \\ 
{\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}, \\ 
{\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} \\ 
$=$$\;\;\;\;${\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}:  loop-nonnormal-nonleave-exact-time-schema \\ \index{loop-nonnormal-nonleave-exact-ti!me-schema}
\=\+(\=\+({\it{stmt-time\/}} $=$ ($1\;+$ {\it{body-time\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{p-step}}\,({\it{initial\/}})\index{p-step} $=$ {\it{state1\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{p}}\,({\it{state1\/}}, {\it{body-time\/}})\index{p} $=$ {\it{state2\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{state2\/}} $=$ {\it{final\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{p}}\,({\it{initial\/}}, {\it{stmt-time\/}})\index{p} $=$ {\it{final\/}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  loop-leave-body-exact-time-schema \\ \index{loop-leave-body-exact-time-sche!ma}
\=\+(\=\+({\it{stmt-time\/}} $=$ ({\tt{3}} $+$ {\it{body-time\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{p-step}}\,({\it{initial\/}})\index{p-step} $=$ {\it{state1\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{p}}\,({\it{state1\/}}, {\it{body-time\/}})\index{p} $=$ {\it{state2\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{p}}\,({\it{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}:  loop-normal-body-exact-time-schema \\ \index{loop-normal-body-exact-time-sche!ma}
\=\+(\=\+({\it{stmt-time\/}} $=$ ($1\;+$ (($1\;+$ {\it{body-time\/}}) $+$ {\it{loop-sub1-time\/}}))) \\ 
$\wedge$$\;\;\;\;$({\rm{p}}\,({\it{state1\/}}, {\it{body-time\/}})\index{p} $=$ {\it{state2\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{p}}\,({\it{state3\/}}, {\it{loop-sub1-time\/}})\index{p} $=$ {\it{state4\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{p-step}}\,({\it{initial\/}})\index{p-step} $=$ {\it{state1\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{p-step}}\,({\it{state2\/}})\index{p-step} $=$ {\it{state3\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{state4\/}} $=$ {\it{final\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{p}}\,({\it{initial\/}}, {\it{stmt-time\/}})\index{p} $=$ {\it{final\/}})\-
\end{tabbing}

%\item 
\begin{verbatim}


(prove-lemma loop-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) 'LOOP-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
	     (AND
	      (OK-MG-STATEMENT (LOOP-BODY STMT)
			       (CONS 'LEAVE R-COND-LIST)
			       NAME-ALIST PROC-LIST)
	      (OK-MG-DEF-PLISTP PROC-LIST)
	      (OK-TRANSLATION-PARAMETERS
	       (MAKE-CINFO (APPEND (CODE CINFO)
				   (LIST (CONS 'DL
					       (CONS (LABEL-CNT CINFO)
						     '(NIL (NO-OP))))))
			   (CONS (CONS 'LEAVE
				       (ADD1 (LABEL-CNT CINFO)))
				 (LABEL-ALIST CINFO))
			   (ADD1 (ADD1 (LABEL-CNT CINFO))))
	       T-COND-LIST
	       (LOOP-BODY STMT)
	       PROC-LIST
	       (CONS (LIST 'JUMP (LABEL-CNT CINFO))
		     (CONS (CONS 'DL
				 (CONS (ADD1 (LABEL-CNT CINFO))
				       '(NIL (PUSH-CONSTANT (NAT 2)))))
			   (CONS '(POP-GLOBAL C-C) CODE2))))
	      (OK-MG-STATEP MG-STATE
			    (CONS 'LEAVE R-COND-LIST))
	      (COND-SUBSETP (CONS 'LEAVE 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 (CONS 'DL
								 (CONS (LABEL-CNT CINFO)
								       '(NIL (NO-OP))))))
					     (CONS (CONS 'LEAVE
							 (ADD1 (LABEL-CNT CINFO)))
						   (LABEL-ALIST CINFO))
					     (ADD1 (ADD1 (LABEL-CNT CINFO))))
				 T-COND-LIST
				 (LOOP-BODY STMT)
				 PROC-LIST))
		(CONS (LIST 'JUMP (LABEL-CNT CINFO))
		      (CONS (CONS 'DL
				  (CONS (ADD1 (LABEL-CNT CINFO))
					'(NIL (PUSH-CONSTANT (NAT 2)))))
			    (CONS '(POP-GLOBAL C-C) 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 (LOOP-BODY 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          ;; state1
			 (TAG 'PC
			      (CONS SUBR
				    (LENGTH (CODE (MAKE-CINFO (APPEND (CODE CINFO)
								      (LIST (CONS 'DL
										  (CONS (LABEL-CNT CINFO)
											'(NIL (NO-OP))))))
							      (CONS (CONS 'LEAVE
									  (ADD1 (LABEL-CNT CINFO)))
								    (LABEL-ALIST CINFO))
							      (ADD1 (ADD1 (LABEL-CNT CINFO))))))))
			 T-COND-LIST)
	       (CLOCK (LOOP-BODY STMT) PROC-LIST MG-STATE (SUB1 N)))   ;; body-time
	      (P-STATE;; state2
	       (TAG 'PC
		    (CONS SUBR
			  (IF
			   (NORMAL (MG-MEANING-R (LOOP-BODY 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 (CONS 'DL
									(CONS (LABEL-CNT CINFO)
									      '(NIL (NO-OP))))))
						    (CONS (CONS 'LEAVE
								(ADD1 (LABEL-CNT CINFO)))
							  (LABEL-ALIST CINFO))
						    (ADD1 (ADD1 (LABEL-CNT CINFO))))
					T-COND-LIST
					(LOOP-BODY STMT)
					PROC-LIST)))
			   (FIND-LABEL
			    (FETCH-LABEL
			     (CC (MG-MEANING-R (LOOP-BODY 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 (CONS 'DL
									 (CONS (LABEL-CNT CINFO)
									       '(NIL (NO-OP))))))
						     (CONS (CONS 'LEAVE
								 (ADD1 (LABEL-CNT CINFO)))
							   (LABEL-ALIST CINFO))
						     (ADD1 (ADD1 (LABEL-CNT CINFO))))
					 T-COND-LIST
					 (LOOP-BODY STMT)
					 PROC-LIST)))
			    (APPEND
			     (CODE
			      (TRANSLATE (MAKE-CINFO (APPEND (CODE CINFO)
							     (LIST (CONS 'DL
									 (CONS (LABEL-CNT CINFO)
									       '(NIL (NO-OP))))))
						     (CONS (CONS 'LEAVE
								 (ADD1 (LABEL-CNT CINFO)))
							   (LABEL-ALIST CINFO))
						     (ADD1 (ADD1 (LABEL-CNT CINFO))))
					 T-COND-LIST
					 (LOOP-BODY STMT)
					 PROC-LIST))
			     (CONS (LIST 'JUMP (LABEL-CNT CINFO))
				   (CONS (CONS 'DL
					       (CONS (ADD1 (LABEL-CNT CINFO))
						     '(NIL (PUSH-CONSTANT (NAT 2)))))
					 (CONS '(POP-GLOBAL C-C) CODE2))))))))
	       CTRL-STK
	       (MAP-DOWN-VALUES
		(MG-ALIST (MG-MEANING-R (LOOP-BODY 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 (LOOP-BODY 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 STMT
			       (CONS 'LEAVE 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-MEANING-R (LOOP-BODY STMT)
					  PROC-LIST MG-STATE
					  (SUB1 N)
					  (LIST (LENGTH TEMP-STK)
						(P-CTRL-STK-SIZE CTRL-STK)))
			    (CONS 'LEAVE R-COND-LIST))
	      (COND-SUBSETP (CONS 'LEAVE 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-MEANING-R (LOOP-BODY STMT)
				       PROC-LIST MG-STATE
				       (SUB1 N)
				       (LIST (LENGTH TEMP-STK)
					     (P-CTRL-STK-SIZE CTRL-STK))))
	       (BINDINGS (TOP CTRL-STK))
	       TEMP-STK)
	      (NO-P-ALIASING (BINDINGS (TOP CTRL-STK))
			     (MG-ALIST (MG-MEANING-R (LOOP-BODY STMT)
						     PROC-LIST MG-STATE
						     (SUB1 N)
						     (LIST (LENGTH TEMP-STK)
							   (P-CTRL-STK-SIZE CTRL-STK)))))
	      (SIGNATURES-MATCH
	       (MG-ALIST (MG-MEANING-R (LOOP-BODY STMT)
				       PROC-LIST MG-STATE
				       (SUB1 N)
				       (LIST (LENGTH TEMP-STK)
					     (P-CTRL-STK-SIZE CTRL-STK))))
	       NAME-ALIST)
	      (NORMAL (MG-MEANING-R (LOOP-BODY STMT)
				    PROC-LIST MG-STATE
				    (SUB1 N)
				    (LIST (LENGTH TEMP-STK)
					  (P-CTRL-STK-SIZE CTRL-STK))))
	      (ALL-CARS-UNIQUE
	       (MG-ALIST (MG-MEANING-R (LOOP-BODY STMT)
				       PROC-LIST MG-STATE
				       (SUB1 N)
				       (LIST (LENGTH TEMP-STK)
					     (P-CTRL-STK-SIZE CTRL-STK)))))
	      (NOT
	       (RESOURCE-ERRORP
		(MG-MEANING-R STMT PROC-LIST
			      (MG-MEANING-R (LOOP-BODY STMT)
					    PROC-LIST MG-STATE
					    (SUB1 N)
					    (LIST (LENGTH TEMP-STK)
						  (P-CTRL-STK-SIZE CTRL-STK)))
			      (SUB1 N)
			      (LIST (LENGTH TEMP-STK)
				    (P-CTRL-STK-SIZE CTRL-STK))))))
	     (EQUAL
	      (P (MAP-DOWN (MG-MEANING-R (LOOP-BODY STMT)                         ;; state3
					 PROC-LIST MG-STATE
					 (SUB1 N)
					 (LIST (LENGTH TEMP-STK)
					       (P-CTRL-STK-SIZE CTRL-STK)))
			   PROC-LIST CTRL-STK TEMP-STK
			   (TAG 'PC
				(CONS SUBR (LENGTH (CODE CINFO))))
			   T-COND-LIST)
		 (CLOCK STMT PROC-LIST                                           ;; loop-sub1-time
			(MG-MEANING-R (LOOP-BODY STMT)
				      PROC-LIST MG-STATE
				      (SUB1 N)
				      (LIST (LENGTH TEMP-STK)
					    (P-CTRL-STK-SIZE CTRL-STK)))
			(SUB1 N)))
	      (P-STATE;; state4
	       (TAG 'PC
		    (CONS SUBR
			  (IF
			   (NORMAL (MG-MEANING-R STMT PROC-LIST
						 (MG-MEANING-R (LOOP-BODY STMT)
							       PROC-LIST MG-STATE
							       (SUB1 N)
							       (LIST (LENGTH TEMP-STK)
								     (P-CTRL-STK-SIZE CTRL-STK)))
						 (SUB1 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-MEANING-R (LOOP-BODY STMT)
							     PROC-LIST MG-STATE
							     (SUB1 N)
							     (LIST (LENGTH TEMP-STK)
								   (P-CTRL-STK-SIZE CTRL-STK)))
					       (SUB1 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-MEANING-R (LOOP-BODY STMT)
						      PROC-LIST MG-STATE
						      (SUB1 N)
						      (LIST (LENGTH TEMP-STK)
							    (P-CTRL-STK-SIZE CTRL-STK)))
					(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 STMT PROC-LIST
					 (MG-MEANING-R (LOOP-BODY STMT)
						       PROC-LIST MG-STATE
						       (SUB1 N)
						       (LIST (LENGTH TEMP-STK)
							     (P-CTRL-STK-SIZE CTRL-STK)))
					 (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 @STATE1
    (MAP-DOWN MG-STATE PROC-LIST CTRL-STK TEMP-STK
     (TAG 'PC
      (CONS SUBR
         (LENGTH (CODE (MAKE-CINFO (APPEND (CODE CINFO)
                                           (LIST (CONS 'DL
                                                       (CONS (LABEL-CNT CINFO)
                                                             '(NIL (NO-OP))))))
                                   (CONS (CONS 'LEAVE
                                               (ADD1 (LABEL-CNT CINFO)))
                                         (LABEL-ALIST CINFO))
                                   (ADD1 (ADD1 (LABEL-CNT CINFO))))))))
     T-COND-LIST))
   (ADD-ABBREVIATION @BODY-TIME
                     (CLOCK (LOOP-BODY STMT)
                            PROC-LIST MG-STATE
                            (SUB1 N)))
   (ADD-ABBREVIATION @STATE2
    (P-STATE
     (TAG 'PC
	  (CONS SUBR
		(IF
		 (NORMAL (MG-MEANING-R (LOOP-BODY 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 (CONS 'DL
							      (CONS (LABEL-CNT CINFO)
								    '(NIL (NO-OP))))))
					  (CONS (CONS 'LEAVE
						      (ADD1 (LABEL-CNT CINFO)))
						(LABEL-ALIST CINFO))
					  (ADD1 (ADD1 (LABEL-CNT CINFO))))
			      T-COND-LIST
			      (LOOP-BODY STMT)
			      PROC-LIST)))
		 (FIND-LABEL
		  (FETCH-LABEL
		   (CC (MG-MEANING-R (LOOP-BODY 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 (CONS 'DL
							       (CONS (LABEL-CNT CINFO)
								     '(NIL (NO-OP))))))
					   (CONS (CONS 'LEAVE
						       (ADD1 (LABEL-CNT CINFO)))
						 (LABEL-ALIST CINFO))
					   (ADD1 (ADD1 (LABEL-CNT CINFO))))
			       T-COND-LIST
			       (LOOP-BODY STMT)
			       PROC-LIST)))
		  (APPEND
		   (CODE
		    (TRANSLATE (MAKE-CINFO (APPEND (CODE CINFO)
						   (LIST (CONS 'DL
							       (CONS (LABEL-CNT CINFO)
								     '(NIL (NO-OP))))))
					   (CONS (CONS 'LEAVE
						       (ADD1 (LABEL-CNT CINFO)))
						 (LABEL-ALIST CINFO))
					   (ADD1 (ADD1 (LABEL-CNT CINFO))))
			       T-COND-LIST
			       (LOOP-BODY STMT)
			       PROC-LIST))
		   (CONS (LIST 'JUMP (LABEL-CNT CINFO))
			 (CONS (CONS 'DL
				     (CONS (ADD1 (LABEL-CNT CINFO))
					   '(NIL (PUSH-CONSTANT (NAT 2)))))
			       (CONS '(POP-GLOBAL C-C) CODE2))))))))
     CTRL-STK
     (MAP-DOWN-VALUES
      (MG-ALIST (MG-MEANING-R (LOOP-BODY 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 (LOOP-BODY 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 @STATE3
                     (MAP-DOWN (MG-MEANING-R (LOOP-BODY STMT)
                                             PROC-LIST MG-STATE
                                             (SUB1 N)
                                             (LIST (LENGTH TEMP-STK)
                                                   (P-CTRL-STK-SIZE CTRL-STK)))
                               PROC-LIST CTRL-STK TEMP-STK
                               (TAG 'PC
                                    (CONS SUBR (LENGTH (CODE CINFO))))
                               T-COND-LIST))
   (ADD-ABBREVIATION @LOOP-SUB1-TIME
                     (CLOCK STMT PROC-LIST
                            (MG-MEANING-R (LOOP-BODY STMT)
                                          PROC-LIST MG-STATE
                                          (SUB1 N)
                                          (LIST (LENGTH TEMP-STK)
                                                (P-CTRL-STK-SIZE CTRL-STK)))
                            (SUB1 N)))
   (ADD-ABBREVIATION @STATE4
    (P-STATE
     (TAG 'PC
	  (CONS SUBR
		(IF
		 (NORMAL (MG-MEANING-R STMT PROC-LIST
				       (MG-MEANING-R (LOOP-BODY STMT)
						     PROC-LIST MG-STATE
						     (SUB1 N)
						     (LIST (LENGTH TEMP-STK)
							   (P-CTRL-STK-SIZE CTRL-STK)))
				       (SUB1 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-MEANING-R (LOOP-BODY STMT)
						   PROC-LIST MG-STATE
						   (SUB1 N)
						   (LIST (LENGTH TEMP-STK)
							 (P-CTRL-STK-SIZE CTRL-STK)))
				     (SUB1 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-MEANING-R (LOOP-BODY STMT)
					    PROC-LIST MG-STATE
					    (SUB1 N)
					    (LIST (LENGTH TEMP-STK)
						  (P-CTRL-STK-SIZE CTRL-STK)))
			      (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 STMT PROC-LIST
                               (MG-MEANING-R (LOOP-BODY STMT)
                                             PROC-LIST MG-STATE
                                             (SUB1 N)
                                             (LIST (LENGTH TEMP-STK)
                                                   (P-CTRL-STK-SIZE CTRL-STK)))
                               (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
   (DEMOTE 19)
   (DIVE 1 1)
   PUSH TOP PROMOTE
   (CLAIM (EQUAL (P-STEP @INITIAL) @STATE1)
          0)
   (CLAIM (NOT (NORMAL (MG-MEANING-R (LOOP-BODY STMT)
                                     PROC-LIST MG-STATE
                                     (SUB1 N)
                                     (LIST (LENGTH TEMP-STK)
                                           (P-CTRL-STK-SIZE CTRL-STK)))))
          0)
   (DROP 19)
   (CLAIM (NOT (EQUAL (CC (MG-MEANING-R (LOOP-BODY STMT)
                                        PROC-LIST MG-STATE
                                        (SUB1 N)
                                        (LIST (LENGTH TEMP-STK)
                                              (P-CTRL-STK-SIZE CTRL-STK))))
                      'LEAVE))
          0)
   (CLAIM (EQUAL @STATE2 @FINAL) 0)
   (CLAIM (EQUAL @STMT-TIME (ADD1 @BODY-TIME))
          0)
   (DEMOTE 19 20 23 24)
   DROP
   (GENERALIZE ((@STATE4 STATE4)
                (@LOOP-SUB1-TIME LOOP-SUB1-TIME)
                (@STATE3 STATE3)
                (@STATE2 STATE2)
                (@BODY-TIME BODY-TIME)
                (@STATE1 STATE1)
                (@FINAL FINAL)
                (@STMT-TIME STMT-TIME)
                (@INITIAL INITIAL)))
   (USE-LEMMA LOOP-NONNORMAL-NONLEAVE-EXACT-TIME-SCHEMA)
   DEMOTE
   (S-PROP AND OR NOT IMPLIES FIX ZEROP IFF NLISTP)
   (CONTRADICT 24)
   (DROP 19 23 24)
   (DIVE 1)
   (REWRITE LOOP-CLOCK-NONNORMAL-NONLEAVE)
   TOP S
   (CONTRADICT 23)
   (DROP 19 20 23)
   (DIVE 1)
   (REWRITE LOOP-NONNORMAL-NONLEAVE-STATE2-EQUALS-FINAL)
   TOP S-PROP
   (CLAIM (EQUAL (P @STATE2 2) @FINAL) 0)
   (CLAIM (EQUAL @STMT-TIME (PLUS 3 @BODY-TIME))
          0)
   (DEMOTE 19 20 23 24)
   DROP
   (GENERALIZE ((@STATE4 STATE4)
                (@LOOP-SUB1-TIME LOOP-SUB1-TIME)
                (@STATE3 STATE3)
                (@STATE2 STATE2)
                (@BODY-TIME BODY-TIME)
                (@STATE1 STATE1)
                (@FINAL FINAL)
                (@STMT-TIME STMT-TIME)
                (@INITIAL INITIAL)))
   DROP
   (USE-LEMMA LOOP-LEAVE-BODY-EXACT-TIME-SCHEMA)
   PROVE
   (CONTRADICT 24)
   (DIVE 1)
   (REWRITE LOOP-CLOCK-NONNORMAL-LEAVE)
   TOP S-PROP
   (CONTRADICT 23)
   (DIVE 1)
   (REWRITE P-ADD1-3)
   (REWRITE P-ADD1-3)
   (REWRITE P-0-UNWINDING-LEMMA)
   (DIVE 1)
   (REWRITE LOOP-LEAVE-STATE2-STEP1-EFFECT)
   UP
   (REWRITE LOOP-LEAVE-STATE2-STEP2-EFFECT)
   TOP S-PROP
   (DEMOTE 19)
   (DIVE 1 1)
   PUSH TOP PROMOTE
   (CLAIM (EQUAL @STMT-TIME
                 (ADD1 (PLUS (ADD1 @BODY-TIME)
                             @LOOP-SUB1-TIME)))
          0)
   (CLAIM (EQUAL (P-STEP @STATE2) @STATE3)
          0)
   (CLAIM (EQUAL @STATE4 @FINAL) 0)
   (DEMOTE 19 20 22 23 24 25)
   DROP
   (GENERALIZE ((@STATE4 STATE4)
                (@LOOP-SUB1-TIME LOOP-SUB1-TIME)
                (@STATE3 STATE3)
                (@STATE2 STATE2)
                (@BODY-TIME BODY-TIME)
                (@STATE1 STATE1)
                (@FINAL FINAL)
                (@STMT-TIME STMT-TIME)
                (@INITIAL INITIAL)))
   DROP
   (USE-LEMMA LOOP-NORMAL-BODY-EXACT-TIME-SCHEMA)
   PROVE
   (CONTRADICT 25)
   (DROP 19 20 22 23 24 25)
   (DIVE 1)
   (REWRITE LOOP-NORMAL-BODY-STATE4-EQUALS-FINAL)
   TOP S-PROP
   (CONTRADICT 24)
   (DIVE 1)
   (REWRITE LOOP-NORMAL-BODY-STEP-STATE2-EQUALS-STATE3)
   TOP S-PROP
   (CONTRADICT 23)
   (DIVE 1)
   (REWRITE LOOP-CLOCK-NORMAL
            (($SIZES (LIST (LENGTH TEMP-STK)
                           (P-CTRL-STK-SIZE CTRL-STK)))))
   UP S
   (USE-LEMMA LOOP-SUB1-BODY-EXACT-TIME-HYPS)
   SPLIT
   (CONTRADICT 21)
   (DIVE 1)
   (REWRITE LOOP-STEP-INITIAL-EQUALS-STATE1)
   TOP S-PROP
   (DROP 19)
   (USE-LEMMA LOOP-BODY-EXACT-TIME-HYPS)
   DEMOTE
   (S-PROP AND OR NOT IMPLIES FIX ZEROP IFF NLISTP))))
\end{verbatim}



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

\addvspace{18pt}

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