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

\addvspace{18pt}

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

\end{verbatim}\begin{tabbing}{\sc Theorem}:  prog2-meaning-r-2 \\ \index{prog2-meaning-r-2}
\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{prog2-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{mg-meaning-r}}\,(\=\+{\rm{prog2-right-branch}}\,({\it{stmt\/}})\index{prog2-right-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{mg-meaning-r}}\,(\=\+{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{sizes\/}})\-\index{mg-meaning-r}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{sizes\/}})\-\index{mg-meaning-r}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mg-meaning-r-prog2-left-non-normal \\ \index{mg-meaning-r-prog2-left-non-nor!mal}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{prog2-mg}}) \\ 
$\wedge$$\;\;\;\;$({\rm{cc}}\,({\it{mg-state\/}})\index{cc} $=$ {\tt{'}}{\tt{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{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{sizes\/}})\-\index{mg-meaning-r})\index{normal}))\- \\ 
$\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{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{sizes\/}})\-\index{mg-meaning-r})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  prog2-translation-2 \\ \index{prog2-translation-2}
\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{prog2-mg}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{translate}}\,({\it{cinfo\/}}, {\it{cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}})\index{translate} \\ 
$=$$\;\;\;\;${\rm{translate}}\,(\=\+{\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{cond-list\/}}, \\ 
{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}})\-\index{translate}, \\ 
{\it{cond-list\/}}, \\ 
{\rm{prog2-right-branch}}\,({\it{stmt\/}})\index{prog2-right-branch}, \\ 
{\it{proc-list\/}})\-\index{translate})\-\-
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  prog2-right-branch-doesnt-halt \\ \index{prog2-right-branch-doesnt-halt}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{prog2-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;${\rm{normal}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{sizes\/}})\-\index{mg-meaning-r})\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{prog2-right-branch}}\,({\it{stmt\/}})\index{prog2-right-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{mg-meaning-r}}\,(\=\+{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\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-prog2-left-non-normal \\ \index{clock-prog2-left-non-normal}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{prog2-mg}}) \\ 
$\wedge$$\;\;\;\;$({\rm{cc}}\,({\it{mg-state\/}})\index{cc} $=$ {\tt{'}}{\tt{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{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{sizes\/}})\-\index{mg-meaning-r})\index{normal}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{clock}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}})\index{clock} \\ 
$=$$\;\;\;\;${\rm{clock}}\,({\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}} $-\;1$)\index{clock})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  prog2-code-rewrite \\ \index{prog2-code-rewrite}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{prog2-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-translation-parameters}}\,({\it{cinfo\/}}, {\it{t-cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}}, {\it{y\/}})\index{ok-translation-parameters})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{append}}\,(\=\+{\rm{code}}\,({\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code}, \\ 
{\rm{append}}\,(\=\+{\rm{code}}\,({\rm{translate}}\,(\=\+{\rm{nullify}}\,({\rm{translate}}\,(\=\+{\rm{nullify}}\,({\it{cinfo\/}})\index{nullify}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{nullify}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{prog2-right-branch}}\,({\it{stmt\/}})\index{prog2-right-branch}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code}, \\ 
{\it{y\/}})\-)\- \\ 
$=$$\;\;\;\;${\rm{append}}\,({\rm{code}}\,({\rm{translate}}\,({\it{cinfo\/}}, {\it{t-cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}})\index{translate})\index{code}, {\it{y\/}}))\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable prog2-code-rewrite.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  prog2-left-branch-translation-parameters-ok \\ \index{prog2-left-branch-translation-p!arameters-ok}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{prog2-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-translation-parameters}}\,({\it{cinfo\/}}, {\it{t-cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}}, {\it{code2\/}})\index{ok-translation-parameters})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{ok-translation-parameters}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{append}}\,(\=\+{\rm{code}}\,({\rm{translate}}\,(\=\+{\rm{nullify}}\,({\rm{translate}}\,(\=\+{\rm{nullify}}\,({\it{cinfo\/}})\index{nullify}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{nullify}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{prog2-right-branch}}\,({\it{stmt\/}})\index{prog2-right-branch}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code}, \\ 
{\it{code2\/}})\-)\-\index{ok-translation-parameters}\-
\end{tabbing}


\noindent{\sc Event}:   Disable prog2-left-branch-translation-parameters-ok.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  prog2-left-branch-code-body-rewrite \\ \index{prog2-left-branch-code-body-rew!rite}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{prog2-mg}}) \\ 
$\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\/}})\-)\-)\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\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\/}}, \\ 
{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code}, \\ 
{\rm{append}}\,(\=\+{\rm{code}}\,({\rm{translate}}\,(\=\+{\rm{nullify}}\,({\rm{translate}}\,(\=\+{\rm{nullify}}\,({\it{cinfo\/}})\index{nullify}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{nullify}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{prog2-right-branch}}\,({\it{stmt\/}})\index{prog2-right-branch}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code}, \\ 
{\it{code2\/}})\-)\-)\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable prog2-left-branch-code-body-rewrite.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  prog2-nonnormal-left-state2-equals-final \\ \index{prog2-nonnormal-left-state2-equ!als-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{prog2-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$$\;\;\;\;$($\neg$ {\rm{normal}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{normal}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{p-state}}\,(\=\+{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,(\=\+{\it{subr\/}}, \\ 
\=\+{\bf if }{\rm{normal}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{normal} \\ 
{\bf then }{\rm{length}}\,({\rm{code}}\,({\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code})\index{length} \\ 
{\bf else }{\rm{find-label}}\,(\=\+{\rm{fetch-label}}\,(\=\+{\rm{cc}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{cc}, \\ 
{\rm{label-alist}}\,({\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{label-alist})\-\index{fetch-label}, \\ 
{\rm{append}}\,(\=\+{\rm{code}}\,({\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code}, \\ 
{\rm{append}}\,(\=\+{\rm{code}}\,({\rm{translate}}\,(\=\+{\rm{nullify}}\,({\rm{translate}}\,(\=\+{\rm{nullify}}\,({\it{cinfo\/}})\index{nullify}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{nullify}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{prog2-right-branch}}\,({\it{stmt\/}})\index{prog2-right-branch}, \\ 
{\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}}\,(\=\+{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{mg-alist}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, \\ 
{\it{temp-stk\/}})\-\index{map-down-values}, \\ 
{\rm{translate-proc-list}}\,({\it{proc-list\/}})\index{translate-proc-list}, \\ 
{\rm{list}}\,({\rm{list}}\,(\=\+{\tt{'}}{\tt{c-c}}, \\ 
{\rm{mg-cond-to-p-nat}}\,(\=\+{\rm{cc}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{cc}, \\ 
{\it{t-cond-list\/}})\-\index{mg-cond-to-p-nat})\-), \\ 
{\sc{mg-max-ctrl-stk-size}}\index{mg-max-ctrl-stk-size}, \\ 
{\sc{mg-max-temp-stk-size}}\index{mg-max-temp-stk-size}, \\ 
{\sc{mg-word-size}}\index{mg-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,(\=\+{\it{subr\/}}, \\ 
\=\+{\bf if }{\rm{normal}}\,({\rm{mg-meaning-r}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{normal} \\ 
{\bf then }{\rm{length}}\,({\rm{code}}\,({\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code})\index{length} \\ 
{\bf else }{\rm{find-label}}\,(\=\+{\rm{fetch-label}}\,(\=\+{\rm{cc}}\,({\rm{mg-meaning-r}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{cc}, \\ 
{\rm{label-alist}}\,({\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{label-alist})\-\index{fetch-label}, \\ 
{\rm{append}}\,(\=\+{\rm{code}}\,({\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code}, \\ 
{\it{code2\/}})\-)\-\index{find-label}$\;${\bf  endif}\-)\-)\-\index{tag}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\rm{map-down-values}}\,(\=\+{\rm{mg-alist}}\,({\rm{mg-meaning-r}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{mg-alist}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, \\ 
{\it{temp-stk\/}})\-\index{map-down-values}, \\ 
{\rm{translate-proc-list}}\,({\it{proc-list\/}})\index{translate-proc-list}, \\ 
{\rm{list}}\,({\rm{list}}\,(\=\+{\tt{'}}{\tt{c-c}}, \\ 
{\rm{mg-cond-to-p-nat}}\,(\=\+{\rm{cc}}\,({\rm{mg-meaning-r}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{cc}, \\ 
{\it{t-cond-list\/}})\-\index{mg-cond-to-p-nat})\-), \\ 
{\sc{mg-max-ctrl-stk-size}}\index{mg-max-ctrl-stk-size}, \\ 
{\sc{mg-max-temp-stk-size}}\index{mg-max-temp-stk-size}, \\ 
{\sc{mg-word-size}}\index{mg-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable prog2-nonnormal-left-state2-equals-final.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  prog2-right-branch-translation-parameters-ok \\ \index{prog2-right-branch-translation-p!arameters-ok}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{prog2-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-translation-parameters}}\,({\it{cinfo\/}}, {\it{t-cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}}, {\it{code2\/}})\index{ok-translation-parameters})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{ok-translation-parameters}}\,(\=\+{\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}})\-\index{translate}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{prog2-right-branch}}\,({\it{stmt\/}})\index{prog2-right-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{code2\/}})\-\index{ok-translation-parameters}\-
\end{tabbing}


\noindent{\sc Event}:   Disable prog2-right-branch-translation-parameters-ok.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  prog2-right-branch-hyps \\ \index{prog2-right-branch-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{prog2-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{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\rm{list}}\,({\rm{length}}\,({\it{temp-stk\/}})\index{length}, {\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size}))\-\index{mg-meaning-r})\index{normal})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{ok-mg-statement}}\,(\=\+{\rm{prog2-right-branch}}\,({\it{stmt\/}})\index{prog2-right-branch}, \\ 
{\it{r-cond-list\/}}, \\ 
{\it{name-alist\/}}, \\ 
{\it{proc-list\/}})\-\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{ok-translation-parameters}}\,(\=\+{\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}})\-\index{translate}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{prog2-right-branch}}\,({\it{stmt\/}})\index{prog2-right-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{code2\/}})\-\index{ok-translation-parameters} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statep}}\,(\=\+{\rm{mg-meaning-r}}\,(\=\+{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r}, \\ 
{\it{r-cond-list\/}})\-\index{ok-mg-statep} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{code}}\,({\rm{translate-def-body}}\,({\rm{assoc}}\,({\it{subr\/}}, {\it{proc-list\/}}), {\it{proc-list\/}})\index{translate-def-body})\index{code} \\ 
$=$$\;\;\;\;${\rm{append}}\,(\=\+{\rm{code}}\,({\rm{translate}}\,(\=\+{\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}})\-\index{translate}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{prog2-right-branch}}\,({\it{stmt\/}})\index{prog2-right-branch}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code}, \\ 
{\it{code2\/}})\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,(\=\+{\rm{mg-alist}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{mg-alist}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, \\ 
{\it{temp-stk\/}})\-\index{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{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{mg-alist})\-\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,(\=\+{\rm{mg-alist}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{mg-alist}, \\ 
{\it{name-alist\/}})\-\index{signatures-match} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{mg-alist})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resource-errorp}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{prog2-right-branch}}\,({\it{stmt\/}})\index{prog2-right-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{mg-meaning-r}}\,(\=\+{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r}, \\ 
{\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}:  prog2-state2-equals-state3 \\ \index{prog2-state2-equals-state3}
\=\+(\=\+({\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{prog2-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{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\rm{list}}\,({\rm{length}}\,({\it{temp-stk\/}})\index{length}, {\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size}))\-\index{mg-meaning-r})\index{normal})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{p-state}}\,(\=\+{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,(\=\+{\it{subr\/}}, \\ 
\=\+{\bf if }{\rm{normal}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{normal} \\ 
{\bf then }{\rm{length}}\,({\rm{code}}\,({\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code})\index{length} \\ 
{\bf else }{\rm{find-label}}\,(\=\+{\rm{fetch-label}}\,(\=\+{\rm{cc}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{cc}, \\ 
{\rm{label-alist}}\,({\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{label-alist})\-\index{fetch-label}, \\ 
{\rm{append}}\,(\=\+{\rm{code}}\,({\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code}, \\ 
{\rm{append}}\,(\=\+{\rm{code}}\,({\rm{translate}}\,(\=\+{\rm{nullify}}\,({\rm{translate}}\,(\=\+{\rm{nullify}}\,({\it{cinfo\/}})\index{nullify}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{nullify}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{prog2-right-branch}}\,({\it{stmt\/}})\index{prog2-right-branch}, \\ 
{\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}}\,(\=\+{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{mg-alist}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, \\ 
{\it{temp-stk\/}})\-\index{map-down-values}, \\ 
{\rm{translate-proc-list}}\,({\it{proc-list\/}})\index{translate-proc-list}, \\ 
{\rm{list}}\,({\rm{list}}\,(\=\+{\tt{'}}{\tt{c-c}}, \\ 
{\rm{mg-cond-to-p-nat}}\,(\=\+{\rm{cc}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{cc}, \\ 
{\it{t-cond-list\/}})\-\index{mg-cond-to-p-nat})\-), \\ 
{\sc{mg-max-ctrl-stk-size}}\index{mg-max-ctrl-stk-size}, \\ 
{\sc{mg-max-temp-stk-size}}\index{mg-max-temp-stk-size}, \\ 
{\sc{mg-word-size}}\index{mg-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state} \\ 
$=$$\;\;\;\;${\rm{map-down}}\,(\=\+{\rm{mg-meaning-r}}\,(\=\+{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r}, \\ 
{\it{proc-list\/}}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\it{temp-stk\/}}, \\ 
{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,(\=\+{\it{subr\/}}, \\ 
{\rm{length}}\,({\rm{code}}\,({\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code})\index{length})\-)\-\index{tag}, \\ 
{\it{t-cond-list\/}})\-\index{map-down})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable prog2-state2-equals-state3.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  prog2-state4-equals-final \\ \index{prog2-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{prog2-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{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\rm{list}}\,({\rm{length}}\,({\it{temp-stk\/}})\index{length}, {\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size}))\-\index{mg-meaning-r})\index{normal})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{p-state}}\,(\=\+{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,(\=\+{\it{subr\/}}, \\ 
\=\+{\bf if }{\rm{normal}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{prog2-right-branch}}\,({\it{stmt\/}})\index{prog2-right-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{mg-meaning-r}}\,(\=\+{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r}, \\ 
{\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}}\,(\=\+{\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}})\-\index{translate}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{prog2-right-branch}}\,({\it{stmt\/}})\index{prog2-right-branch}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code})\index{length} \\ 
{\bf else }{\rm{find-label}}\,(\=\+{\rm{fetch-label}}\,(\=\+{\rm{cc}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{prog2-right-branch}}\,({\it{stmt\/}})\index{prog2-right-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{mg-meaning-r}}\,(\=\+{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r}, \\ 
{\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}}\,(\=\+{\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}})\-\index{translate}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{prog2-right-branch}}\,({\it{stmt\/}})\index{prog2-right-branch}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{label-alist})\-\index{fetch-label}, \\ 
{\rm{append}}\,(\=\+{\rm{code}}\,({\rm{translate}}\,(\=\+{\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}})\-\index{translate}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{prog2-right-branch}}\,({\it{stmt\/}})\index{prog2-right-branch}, \\ 
{\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}}\,(\=\+{\rm{prog2-right-branch}}\,({\it{stmt\/}})\index{prog2-right-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{mg-meaning-r}}\,(\=\+{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{mg-alist}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, \\ 
{\it{temp-stk\/}})\-\index{map-down-values}, \\ 
{\rm{translate-proc-list}}\,({\it{proc-list\/}})\index{translate-proc-list}, \\ 
{\rm{list}}\,({\rm{list}}\,(\=\+{\tt{'}}{\tt{c-c}}, \\ 
{\rm{mg-cond-to-p-nat}}\,(\=\+{\rm{cc}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{prog2-right-branch}}\,({\it{stmt\/}})\index{prog2-right-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{mg-meaning-r}}\,(\=\+{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r}, \\ 
{\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}


\noindent{\sc Event}:   Disable prog2-state4-equals-final.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  prog2-normal-left-exact-time-schema \\ \index{prog2-normal-left-exact-time-sc!hema}
\=\+(\=\+({\it{stmt-time\/}} $=$ ({\it{left-time\/}} $+$ {\it{right-time\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{p}}\,({\it{initial\/}}, {\it{left-time\/}})\index{p} $=$ {\it{state2\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{state2\/}} $=$ {\it{state3\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{p}}\,({\it{state3\/}}, {\it{right-time\/}})\index{p} $=$ {\it{state4\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{state4\/}} $=$ {\it{final\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{p}}\,({\it{initial\/}}, {\it{stmt-time\/}})\index{p} $=$ {\it{final\/}})\-
\end{tabbing}


\noindent{\sc Event}:   Disable prog2-normal-left-exact-time-schema.

\addvspace{18pt}

%\item 
\begin{verbatim}


(prove-lemma exact-time-lemma-prog2-case (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) 'prog2-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 (prog2-left-branch stmt)
			   r-cond-list name-alist proc-list)
	  (ok-mg-def-plistp proc-list)
	  (ok-translation-parameters cinfo t-cond-list
				     (prog2-left-branch stmt)
				     proc-list
				     (append (code (translate (nullify (translate (nullify cinfo)
										  t-cond-list
										  (prog2-left-branch stmt)
										  proc-list))
							      t-cond-list
							      (prog2-right-branch 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
			     (prog2-left-branch stmt)
			     proc-list))
	    (append (code (translate (nullify (translate (nullify cinfo)
							 t-cond-list
							 (prog2-left-branch stmt)
							 proc-list))
				     t-cond-list
				     (prog2-right-branch 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 (prog2-left-branch stmt)
					      proc-list mg-state
					      (sub1 n)
					      (list (length temp-stk)
						    (p-ctrl-stk-size ctrl-stk))))))
	 (equal
	  (p (map-down mg-state proc-list ctrl-stk temp-stk               ;; state1
		       (tag 'pc
			    (cons subr (length (code cinfo))))
		       t-cond-list)
	     (clock (prog2-left-branch stmt)                             ;; left-time
		    proc-list mg-state
		    (sub1 n)))
	  (p-state;; state2
	   (tag 'pc
		(cons subr
		      (if
			  (normal (mg-meaning-r (prog2-left-branch stmt)
						proc-list mg-state
						(sub1 n)
						(list (length temp-stk)
						      (p-ctrl-stk-size ctrl-stk))))
			  (length (code (translate cinfo t-cond-list
						   (prog2-left-branch stmt)
						   proc-list)))
			(find-label
			 (fetch-label (cc (mg-meaning-r (prog2-left-branch stmt)
							proc-list mg-state
							(sub1 n)
							(list (length temp-stk)
							      (p-ctrl-stk-size ctrl-stk))))
				      (label-alist (translate cinfo t-cond-list
							      (prog2-left-branch stmt)
							      proc-list)))
			 (append
			  (code (translate cinfo t-cond-list
					   (prog2-left-branch stmt)
					   proc-list))
			  (append (code (translate (nullify (translate (nullify cinfo)
								       t-cond-list
								       (prog2-left-branch stmt)
								       proc-list))
						   t-cond-list
						   (prog2-right-branch stmt)
						   proc-list))
				  code2))))))
	   ctrl-stk
	   (map-down-values
	    (mg-alist (mg-meaning-r (prog2-left-branch stmt)
				    proc-list mg-state
				    (sub1 n)
				    (list (length temp-stk)
					  (p-ctrl-stk-size ctrl-stk))))
	    (bindings (top ctrl-stk))
	    temp-stk)
	   (translate-proc-list proc-list)
	   (list
	    (list 'c-c
		  (mg-cond-to-p-nat (cc (mg-meaning-r (prog2-left-branch stmt)
						      proc-list mg-state
						      (sub1 n)
						      (list (length temp-stk)
							    (p-ctrl-stk-size ctrl-stk))))
				    t-cond-list)))
	   (MG-MAX-CTRL-STK-SIZE)
	   (MG-MAX-TEMP-STK-SIZE)
	   (MG-WORD-SIZE)
	   'run)))
	(implies
	 (and
	  (ok-mg-statement (prog2-right-branch stmt)
			   r-cond-list name-alist proc-list)
	  (ok-mg-def-plistp proc-list)
	  (ok-translation-parameters (translate cinfo t-cond-list
						(prog2-left-branch stmt)
						proc-list)
				     t-cond-list
				     (prog2-right-branch stmt)
				     proc-list code2)
	  (ok-mg-statep (mg-meaning-r (prog2-left-branch stmt)
				      proc-list mg-state
				      (sub1 n)
				      (list (length temp-stk)
					    (p-ctrl-stk-size ctrl-stk)))
			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 (translate cinfo t-cond-list
						     (prog2-left-branch stmt)
						     proc-list)
					  t-cond-list
					  (prog2-right-branch 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 (prog2-left-branch 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 (prog2-left-branch stmt)
						 proc-list mg-state
						 (sub1 n)
						 (list (length temp-stk)
						       (p-ctrl-stk-size ctrl-stk)))))
	  (signatures-match
	   (mg-alist (mg-meaning-r (prog2-left-branch stmt)
				   proc-list mg-state
				   (sub1 n)
				   (list (length temp-stk)
					 (p-ctrl-stk-size ctrl-stk))))
	   name-alist)
	  (normal (mg-meaning-r (prog2-left-branch 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 (prog2-left-branch stmt)
				   proc-list mg-state
				   (sub1 n)
				   (list (length temp-stk)
					 (p-ctrl-stk-size ctrl-stk)))))
	  (not
	   (resource-errorp
	    (mg-meaning-r (prog2-right-branch stmt)
			  proc-list
			  (mg-meaning-r (prog2-left-branch 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 (prog2-left-branch 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 (translate cinfo t-cond-list
							   (prog2-left-branch stmt)
							   proc-list)))))
		       t-cond-list)
	     (clock (prog2-right-branch stmt)                              ;; right-time
		    proc-list
		    (mg-meaning-r (prog2-left-branch 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 (prog2-right-branch stmt)
						proc-list
						(mg-meaning-r (prog2-left-branch 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 (translate cinfo t-cond-list
							      (prog2-left-branch stmt)
							      proc-list)
						   t-cond-list
						   (prog2-right-branch stmt)
						   proc-list)))
			(find-label
			 (fetch-label
			  (cc (mg-meaning-r (prog2-right-branch stmt)
					    proc-list
					    (mg-meaning-r (prog2-left-branch 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 (translate cinfo t-cond-list
							     (prog2-left-branch stmt)
							     proc-list)
						  t-cond-list
						  (prog2-right-branch stmt)
						  proc-list)))
			 (append (code (translate (translate cinfo t-cond-list
							     (prog2-left-branch stmt)
							     proc-list)
						  t-cond-list
						  (prog2-right-branch stmt)
						  proc-list))
				 code2)))))
	   ctrl-stk
	   (map-down-values
	    (mg-alist (mg-meaning-r (prog2-right-branch stmt)
				    proc-list
				    (mg-meaning-r (prog2-left-branch 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 (prog2-right-branch stmt)
				     proc-list
				     (mg-meaning-r (prog2-left-branch 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 @left-time
                     (clock (prog2-left-branch stmt)
                            proc-list mg-state
                            (sub1 n)))
   (add-abbreviation @state2
    (p-state
     (tag 'pc
	  (cons subr
		(if
		    (normal (mg-meaning-r (prog2-left-branch stmt)
					  proc-list mg-state
					  (sub1 n)
					  (list (length temp-stk)
						(p-ctrl-stk-size ctrl-stk))))
		    (length (code (translate cinfo t-cond-list
					     (prog2-left-branch stmt)
					     proc-list)))
		  (find-label
		   (fetch-label (cc (mg-meaning-r (prog2-left-branch stmt)
						  proc-list mg-state
						  (sub1 n)
						  (list (length temp-stk)
							(p-ctrl-stk-size ctrl-stk))))
				(label-alist (translate cinfo t-cond-list
							(prog2-left-branch stmt)
							proc-list)))
		   (append
		    (code (translate cinfo t-cond-list
				     (prog2-left-branch stmt)
				     proc-list))
		    (append (code (translate (nullify (translate (nullify cinfo)
								 t-cond-list
								 (prog2-left-branch stmt)
								 proc-list))
					     t-cond-list
					     (prog2-right-branch stmt)
					     proc-list))
			    code2))))))
     ctrl-stk
     (map-down-values
      (mg-alist (mg-meaning-r (prog2-left-branch stmt)
			      proc-list mg-state
			      (sub1 n)
			      (list (length temp-stk)
				    (p-ctrl-stk-size ctrl-stk))))
      (bindings (top ctrl-stk))
      temp-stk)
     (translate-proc-list proc-list)
     (list
      (list 'c-c
	    (mg-cond-to-p-nat (cc (mg-meaning-r (prog2-left-branch stmt)
						proc-list mg-state
						(sub1 n)
						(list (length temp-stk)
						      (p-ctrl-stk-size ctrl-stk))))
			      t-cond-list)))
     (MG-MAX-CTRL-STK-SIZE)
     (MG-MAX-TEMP-STK-SIZE)
     (MG-WORD-SIZE)
     'run))
   (add-abbreviation @state3
         (map-down (mg-meaning-r (prog2-left-branch 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 (translate cinfo t-cond-list
                                                       (prog2-left-branch stmt)
                                                       proc-list)))))
                   t-cond-list))
   (add-abbreviation @right-time
                     (clock (prog2-right-branch stmt)
                            proc-list
                            (mg-meaning-r (prog2-left-branch 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 (prog2-right-branch stmt)
					  proc-list
					  (mg-meaning-r (prog2-left-branch 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 (translate cinfo t-cond-list
							(prog2-left-branch stmt)
							proc-list)
					     t-cond-list
					     (prog2-right-branch stmt)
					     proc-list)))
		  (find-label
		   (fetch-label
		    (cc (mg-meaning-r (prog2-right-branch stmt)
				      proc-list
				      (mg-meaning-r (prog2-left-branch 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 (translate cinfo t-cond-list
						       (prog2-left-branch stmt)
						       proc-list)
					    t-cond-list
					    (prog2-right-branch stmt)
					    proc-list)))
		   (append (code (translate (translate cinfo t-cond-list
						       (prog2-left-branch stmt)
						       proc-list)
					    t-cond-list
					    (prog2-right-branch stmt)
					    proc-list))
			   code2)))))
     ctrl-stk
     (map-down-values
      (mg-alist (mg-meaning-r (prog2-right-branch stmt)
			      proc-list
			      (mg-meaning-r (prog2-left-branch 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 (prog2-right-branch stmt)
                               proc-list
                               (mg-meaning-r (prog2-left-branch 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 (not (normal (mg-meaning-r (prog2-left-branch stmt)
                                     proc-list mg-state
                                     (sub1 n)
                                     (list (length temp-stk)
                                           (p-ctrl-stk-size ctrl-stk)))))
          0)
   (drop 19)
   (claim (equal @state2 @final) 0)
   (claim (equal @stmt-time @left-time)
          0)
   (demote 19 21 22)
   drop
   (generalize ((@right-time right-time)
                (@left-time left-time)
                (@state4 state4)
                (@state3 state3)
                (@state2 state2)
                (@final final)
                (@stmt-time stmt-time)
                (@initial initial)))
   prove
   (contradict 22)
   (dive 1)
   (rewrite clock-prog2-left-non-normal
            (($sizes (list (length temp-stk)
                           (p-ctrl-stk-size ctrl-stk)))))
   up s
   (demote 16)
   s
   (contradict 21)
   (dive 1)
   (rewrite prog2-nonnormal-left-state2-equals-final)
   top s-prop
   (demote 19)
   (dive 1 1)
   push top promote
   (claim (equal @stmt-time
                 (plus @left-time @right-time))
          0)
   (claim (equal @state2 @state3) 0)
   (claim (equal @state4 @final) 0)
   (demote 19 21 22 23 24)
   drop
   (generalize ((@right-time right-time)
                (@left-time left-time)
                (@state4 state4)
                (@state3 state3)
                (@state2 state2)
                (@final final)
                (@stmt-time stmt-time)
                (@initial initial)))
   (use-lemma prog2-normal-left-exact-time-schema)
   prove
   (contradict 24)
   (dive 1)
   (rewrite prog2-state4-equals-final)
   drop top prove
   (contradict 23)
   (dive 1)
   (rewrite prog2-state2-equals-state3)
   top s
   (contradict 22)
   (dive 1)
   (rewrite clock-prog2)
   s up
   (rewrite plus-equality-lemma1)
   (dive 2 3)
   (rewrite mg-meaning-equivalence)
   top s s
   (dive 1)
   (rewrite prog2-left-branch-doesnt-halt)
   top s split
   (rewrite prog2-right-branch-hyps)
   (rewrite prog2-right-branch-hyps)
   (rewrite prog2-right-branch-hyps)
   (dive 1)
   (rewrite prog2-right-branch-hyps)
   top s
   (rewrite prog2-right-branch-hyps)
   (rewrite prog2-right-branch-hyps)
   (rewrite prog2-right-branch-hyps)
   (rewrite prog2-right-branch-hyps)
   (dive 1)
   (rewrite prog2-right-branch-hyps)
   top s
   (drop 19)
   split
   (rewrite ok-prog2-statement)
   (rewrite prog2-left-branch-translation-parameters-ok)
   (dive 1)
   (rewrite prog2-left-branch-code-body-rewrite)
   up s s
   (dive 1)
   (rewrite prog2-left-branch-doesnt-halt)
   top s)))
\end{verbatim}



\noindent{\sc Event}:   Disable exact-time-lemma-prog2-case.

\addvspace{18pt}


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

\addvspace{18pt}

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