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

\addvspace{18pt}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                           ;;
;;                      EXACT-TIME LEMMA SIGNAL CASE                         ;;
;;                                                                           ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

\end{verbatim}
\noindent{\sc Event}:   Enable labelledp.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  instrs-unlabel \\ \index{instrs-unlabel}
\=\+({\rm{unlabel}}\,({\rm{cons}}\,({\tt{'}}{\tt{push-constant}}, {\it{y\/}}))\index{unlabel} $=$ {\rm{cons}}\,({\tt{'}}{\tt{push-constant}}, {\it{y\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{unlabel}}\,({\rm{cons}}\,({\tt{'}}{\tt{pop-global}}, {\it{y\/}}))\index{unlabel} $=$ {\rm{cons}}\,({\tt{'}}{\tt{pop-global}}, {\it{y\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{unlabel}}\,({\rm{cons}}\,({\tt{'}}{\tt{jump}}, {\it{y\/}}))\index{unlabel} $=$ {\rm{cons}}\,({\tt{'}}{\tt{jump}}, {\it{y\/}}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  signal-meaning-r-2 \\ \index{signal-meaning-r-2}
\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{signal-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{set-condition}}\,({\it{mg-state\/}}, {\rm{signalled-condition}}\,({\it{stmt\/}})\index{signalled-condition})\index{set-condition}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  signal-translation2 \\ \index{signal-translation2}
\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{signal-mg}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{translate}}\,({\it{cinfo\/}}, {\it{cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}})\index{translate} \\ 
$=$$\;\;\;\;${\rm{make-cinfo}}\,(\=\+{\rm{append}}\,(\=\+{\rm{code}}\,({\it{cinfo\/}})\index{code}, \\ 
{\rm{list}}\,(\=\+{\rm{list}}\,(\=\+{\tt{'}}{\tt{push-constant}}, \\ 
{\rm{mg-cond-to-p-nat}}\,(\=\+{\rm{signalled-condition}}\,({\it{stmt\/}})\index{signalled-condition}, \\ 
{\it{cond-list\/}})\-\index{mg-cond-to-p-nat})\-, \\ 
{\rm{list}}\,({\tt{'}}{\tt{pop-global}}, {\tt{'}}{\tt{c-c}}), \\ 
{\rm{list}}\,(\=\+{\tt{'}}{\tt{jump}}, \\ 
{\rm{fetch-label}}\,(\=\+{\rm{signalled-condition}}\,({\it{stmt\/}})\index{signalled-condition}, \\ 
{\rm{label-alist}}\,({\it{cinfo\/}})\index{label-alist})\-\index{fetch-label})\-)\-)\-, \\ 
{\rm{label-alist}}\,({\it{cinfo\/}})\index{label-alist}, \\ 
{\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt})\-\index{make-cinfo})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  exact-time-lemma-signal-case-steps-1-3 \\ \index{exact-time-lemma-signal-case-step!s-1-3}
\=\+(\=\+({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resources-inadequatep}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{resources-inadequatep}) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{stmt\/}}) $\not=$ {\tt{'}}{\tt{no-op-mg}}) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{signal-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{r-cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-translation-parameters}}\,({\it{cinfo\/}}, {\it{t-cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}}, {\it{code2\/}})\index{ok-translation-parameters} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statep}}\,({\it{mg-state\/}}, {\it{r-cond-list\/}})\index{ok-mg-statep} \\ 
$\wedge$$\;\;\;\;${\rm{cond-subsetp}}\,({\it{r-cond-list\/}}, {\it{t-cond-list\/}})\index{cond-subsetp} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{code}}\,({\rm{translate-def-body}}\,({\rm{assoc}}\,({\it{subr\/}}, {\it{proc-list\/}}), {\it{proc-list\/}})\index{translate-def-body})\index{code} \\ 
$=$$\;\;\;\;${\rm{append}}\,(\=\+{\rm{code}}\,({\rm{translate}}\,({\it{cinfo\/}}, {\it{t-cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}})\index{translate})\index{code}, \\ 
{\it{code2\/}})\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{user-defined-procp}}\,({\it{subr\/}}, {\it{proc-list\/}})\index{user-defined-procp} \\ 
$\wedge$$\;\;\;\;${\rm{plistp}}\,({\it{temp-stk\/}})\index{plistp} \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\it{ctrl-stk\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,(\=\+{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, \\ 
{\it{temp-stk\/}})\-\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, {\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match} \\ 
$\wedge$$\;\;\;\;${\rm{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resource-errorp}}\,({\rm{mg-meaning-r}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{resource-errorp}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{p-step}}\,({\rm{p-step}}\,({\rm{p-step}}\,({\rm{map-down}}\,(\=\+{\it{mg-state\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\it{temp-stk\/}}, \\ 
{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,({\it{subr\/}}, {\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length}))\-\index{tag}, \\ 
{\it{t-cond-list\/}})\-\index{map-down})\index{p-step})\index{p-step})\index{p-step} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,(\=\+{\it{subr\/}}, \\ 
\=\+{\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 exact-time-lemma-signal-case-steps-1-3.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  exact-time-lemma-signal-case \\ \index{exact-time-lemma-signal-case}
\=\+(\=\+({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resources-inadequatep}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{resources-inadequatep}) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{stmt\/}}) $\not=$ {\tt{'}}{\tt{no-op-mg}}) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{signal-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{r-cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-translation-parameters}}\,({\it{cinfo\/}}, {\it{t-cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}}, {\it{code2\/}})\index{ok-translation-parameters} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statep}}\,({\it{mg-state\/}}, {\it{r-cond-list\/}})\index{ok-mg-statep} \\ 
$\wedge$$\;\;\;\;${\rm{cond-subsetp}}\,({\it{r-cond-list\/}}, {\it{t-cond-list\/}})\index{cond-subsetp} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{code}}\,({\rm{translate-def-body}}\,({\rm{assoc}}\,({\it{subr\/}}, {\it{proc-list\/}}), {\it{proc-list\/}})\index{translate-def-body})\index{code} \\ 
$=$$\;\;\;\;${\rm{append}}\,(\=\+{\rm{code}}\,({\rm{translate}}\,({\it{cinfo\/}}, {\it{t-cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}})\index{translate})\index{code}, \\ 
{\it{code2\/}})\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{user-defined-procp}}\,({\it{subr\/}}, {\it{proc-list\/}})\index{user-defined-procp} \\ 
$\wedge$$\;\;\;\;${\rm{plistp}}\,({\it{temp-stk\/}})\index{plistp} \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\it{ctrl-stk\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,(\=\+{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, \\ 
{\it{temp-stk\/}})\-\index{mg-vars-list-ok-in-p-state} \\ 
$\wedge$$\;\;\;\;${\rm{no-p-aliasing}}\,({\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, {\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{no-p-aliasing} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match} \\ 
$\wedge$$\;\;\;\;${\rm{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resource-errorp}}\,({\rm{mg-meaning-r}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{resource-errorp}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{p}}\,(\=\+{\rm{map-down}}\,(\=\+{\it{mg-state\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\it{temp-stk\/}}, \\ 
{\rm{tag}}\,({\tt{'}}{\tt{pc}}, {\rm{cons}}\,({\it{subr\/}}, {\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length}))\index{tag}, \\ 
{\it{t-cond-list\/}})\-\index{map-down}, \\ 
{\rm{clock}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}})\index{clock})\-\index{p} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,(\=\+{\it{subr\/}}, \\ 
\=\+{\bf if }{\rm{normal}}\,({\rm{mg-meaning-r}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{normal} \\ 
{\bf then }{\rm{length}}\,({\rm{code}}\,({\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code})\index{length} \\ 
{\bf else }{\rm{find-label}}\,(\=\+{\rm{fetch-label}}\,(\=\+{\rm{cc}}\,({\rm{mg-meaning-r}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{cc}, \\ 
{\rm{label-alist}}\,({\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{label-alist})\-\index{fetch-label}, \\ 
{\rm{append}}\,(\=\+{\rm{code}}\,({\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code}, \\ 
{\it{code2\/}})\-)\-\index{find-label}$\;${\bf  endif}\-)\-)\-\index{tag}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\rm{map-down-values}}\,(\=\+{\rm{mg-alist}}\,({\rm{mg-meaning-r}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{mg-alist}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, \\ 
{\it{temp-stk\/}})\-\index{map-down-values}, \\ 
{\rm{translate-proc-list}}\,({\it{proc-list\/}})\index{translate-proc-list}, \\ 
{\rm{list}}\,({\rm{list}}\,(\=\+{\tt{'}}{\tt{c-c}}, \\ 
{\rm{mg-cond-to-p-nat}}\,(\=\+{\rm{cc}}\,({\rm{mg-meaning-r}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{cc}, \\ 
{\it{t-cond-list\/}})\-\index{mg-cond-to-p-nat})\-), \\ 
{\sc{mg-max-ctrl-stk-size}}\index{mg-max-ctrl-stk-size}, \\ 
{\sc{mg-max-temp-stk-size}}\index{mg-max-temp-stk-size}, \\ 
{\sc{mg-word-size}}\index{mg-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state})\-\-
\end{tabbing}


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

\addvspace{18pt}


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

\addvspace{18pt}

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