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

\addvspace{18pt}

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

\end{verbatim}\begin{tabbing}{\sc Theorem}:  normal-not-legal-begin-label \\ \index{normal-not-legal-begin-label}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{begin-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{r-cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement})\- \\ 
$\rightarrow$$\;\;\;\;$(({\tt{'}}{\tt{normal}} $\in$ {\rm{when-labels}}\,({\it{stmt\/}})\index{when-labels}) $=$ {\bf{f}})\-
\end{tabbing}

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

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


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

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  begin-body-doesnt-halt \\ \index{begin-body-doesnt-halt}
\=\+(\=\+({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{begin-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{begin-body}}\,({\it{stmt\/}})\index{begin-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}:  begin-when-arm-doesnt-halt \\ \index{begin-when-arm-doesnt-halt}
\=\+(\=\+({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{begin-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{cc}}\,({\rm{mg-meaning-r}}\,({\rm{begin-body}}\,({\it{stmt\/}})\index{begin-body}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}} $-\;1$, {\it{sizes\/}})\index{mg-meaning-r})\index{cc} \\ 
$\in$$\;\;\;\;${\rm{when-labels}}\,({\it{stmt\/}})\index{when-labels})\- \\ 
$\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{when-handler}}\,({\it{stmt\/}})\index{when-handler}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{mg-state}}\,(\=\+{\tt{'}}{\tt{normal}}, \\ 
{\rm{mg-alist}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{begin-body}}\,({\it{stmt\/}})\index{begin-body}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{sizes\/}})\-\index{mg-meaning-r})\index{mg-alist}, \\ 
{\rm{mg-psw}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{begin-body}}\,({\it{stmt\/}})\index{begin-body}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{sizes\/}})\-\index{mg-meaning-r})\index{mg-psw})\-\index{mg-state}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{sizes\/}})\-\index{mg-meaning-r})\index{mg-psw} \\ 
$=$$\;\;\;\;${\tt{'}}{\tt{run}})\-\-
\end{tabbing}

%\item 
\begin{verbatim}


(prove-lemma begin-code-rewrite1 (rewrite)
       (IMPLIES
	(AND (EQUAL (CAR STMT) 'BEGIN-MG)
	     (OK-MG-STATEMENT STMT R-COND-LIST NAME-ALIST PROC-LIST))
        (equal (APPEND (CODE (TRANSLATE CINFO T-COND-LIST STMT PROC-LIST))
		       CODE2)
	       (APPEND
		(CODE (TRANSLATE (MAKE-CINFO (CODE CINFO)
					     (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
								       (LABEL-CNT CINFO))
						     (LABEL-ALIST CINFO))
					     (ADD1 (ADD1 (LABEL-CNT CINFO))))
				 T-COND-LIST
				 (BEGIN-BODY STMT)
				 PROC-LIST))
		(CONS
		 (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
		 (CONS
		  (CONS 'DL
			(CONS (LABEL-CNT CINFO)
			      '(NIL (PUSH-CONSTANT (NAT 2)))))
		  (CONS
		   '(POP-GLOBAL C-C)
		   (APPEND
		    (CODE
		     (TRANSLATE
		      (NULLIFY
		       (SET-LABEL-ALIST
			(TRANSLATE
			 (MAKE-CINFO (CODE CINFO)
				     (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
							       (LABEL-CNT CINFO))
					     (LABEL-ALIST CINFO))
				     (ADD1 (ADD1 (LABEL-CNT CINFO))))
			 T-COND-LIST
			 (BEGIN-BODY STMT)
			 PROC-LIST)
			(LABEL-ALIST CINFO)))
		      T-COND-LIST
		      (WHEN-HANDLER STMT)
		      PROC-LIST))
		    (CONS (CONS 'DL
				(CONS (ADD1 (LABEL-CNT CINFO))
				      '(NIL (NO-OP))))
			  CODE2))))))))
   ((INSTRUCTIONS 
     PROMOTE (DIVE 1 1 1) (REWRITE BEGIN-TRANSLATION-2) UP UP
     (S LEMMAS) (DIVE 1) (REWRITE NEW-CODE-APPENDED-TO-OLD1) (S LEMMAS)
     UP UP (S LEMMAS) X (S LEMMAS))))
\end{verbatim}


\begin{tabbing}{\sc Theorem}:  begin-labels-subset-r-cond-list \\ \index{begin-labels-subset-r-cond-list}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{begin-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{r-cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{cond-subsetp}}\,({\rm{when-labels}}\,({\it{stmt\/}})\index{when-labels}, {\it{r-cond-list\/}})\index{cond-subsetp}\-
\end{tabbing}

%\item 
\begin{verbatim}


(prove-lemma begin-body-hyps (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) 'BEGIN-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))))))
       (AND (OK-MG-STATEMENT (BEGIN-BODY STMT) (APPEND (WHEN-LABELS STMT) R-COND-LIST) 
			     NAME-ALIST PROC-LIST)
	    (OK-TRANSLATION-PARAMETERS
	     (MAKE-CINFO (CODE CINFO)
			 (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
						   (LABEL-CNT CINFO))
				 (LABEL-ALIST CINFO))
			 (ADD1 (ADD1 (LABEL-CNT CINFO))))
	     T-COND-LIST
	     (BEGIN-BODY STMT)
	     PROC-LIST
	     (CONS
	      (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
	      (CONS
	       (CONS 'DL
		     (CONS (LABEL-CNT CINFO)
			   '(NIL (PUSH-CONSTANT (NAT 2)))))
	       (CONS
		'(POP-GLOBAL C-C)
		(APPEND
		 (CODE
		  (TRANSLATE
		   (NULLIFY
		    (SET-LABEL-ALIST
		     (TRANSLATE
		      (MAKE-CINFO (CODE CINFO)
				  (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
							    (LABEL-CNT CINFO))
					  (LABEL-ALIST CINFO))
				  (ADD1 (ADD1 (LABEL-CNT CINFO))))
		      T-COND-LIST
		      (BEGIN-BODY STMT)
		      PROC-LIST)
		     (LABEL-ALIST CINFO)))
		   T-COND-LIST
		   (WHEN-HANDLER STMT)
		   PROC-LIST))
		 (CONS (CONS 'DL
			     (CONS (ADD1 (LABEL-CNT CINFO))
				   '(NIL (NO-OP))))
		       CODE2))))))
	    (OK-MG-STATEP MG-STATE (APPEND (WHEN-LABELS STMT) R-COND-LIST))
	    (COND-SUBSETP (APPEND (WHEN-LABELS STMT) R-COND-LIST) T-COND-LIST)
	    (EQUAL
	     (CODE (TRANSLATE-DEF-BODY (ASSOC SUBR PROC-LIST)
				       PROC-LIST))
	     (APPEND
	      (CODE (TRANSLATE (MAKE-CINFO (CODE CINFO)
					   (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
								     (LABEL-CNT CINFO))
						   (LABEL-ALIST CINFO))
					   (ADD1 (ADD1 (LABEL-CNT CINFO))))
			       T-COND-LIST
			       (BEGIN-BODY STMT)
			       PROC-LIST))
	      (CONS
	       (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
	       (CONS
		(CONS 'DL
		      (CONS (LABEL-CNT CINFO)
			    '(NIL (PUSH-CONSTANT (NAT 2)))))
		(CONS
		 '(POP-GLOBAL C-C)
		 (APPEND
		  (CODE
		   (TRANSLATE
		    (NULLIFY
		     (SET-LABEL-ALIST
		      (TRANSLATE
		       (MAKE-CINFO (CODE CINFO)
				   (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
							     (LABEL-CNT CINFO))
					   (LABEL-ALIST CINFO))
				   (ADD1 (ADD1 (LABEL-CNT CINFO))))
		       T-COND-LIST
		       (BEGIN-BODY STMT)
		       PROC-LIST)
		      (LABEL-ALIST CINFO)))
		    T-COND-LIST
		    (WHEN-HANDLER STMT)
		    PROC-LIST))
		  (CONS (CONS 'DL
			      (CONS (ADD1 (LABEL-CNT CINFO))
				    '(NIL (NO-OP))))
			CODE2)))))))
	    (NOT (RESOURCE-ERRORP (MG-MEANING-R (BEGIN-BODY STMT)
						  PROC-LIST MG-STATE
						  (SUB1 N)
						  (LIST (LENGTH TEMP-STK)
							(P-CTRL-STK-SIZE CTRL-STK)))))))
     ((INSTRUCTIONS 
       PROMOTE SPLIT (PROVE (ENABLE OK-MG-STATEMENT)) X SPLIT (DEMOTE 6) (DIVE 1)
       X-DUMB (DIVE 2 2) X (DIVE 1) (REWRITE BEGIN-CODE-REWRITE1) TOP PROVE
       (PROVE (ENABLE OK-TRANSLATION-PARAMETERS)) 
       (PROVE (ENABLE OK-TRANSLATION-PARAMETERS)) X (PROVE (ENABLE OK-MG-STATEP))
       (REWRITE COND-SUBSETP-APPEND) (REWRITE BEGIN-LABELS-SUBSET-R-COND-LIST)
       (DIVE 1) = (REWRITE BEGIN-CODE-REWRITE1) UP S S (DIVE 1)
       (REWRITE BEGIN-BODY-DOESNT-HALT) TOP S)))
\end{verbatim}


%\item 
\begin{verbatim}


(prove-lemma begin-when-handler-hyps (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) 'BEGIN-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)))))
            (not (normal (mg-meaning-r (begin-body stmt) proc-list mg-state (sub1 n)
				       (LIST (LENGTH TEMP-STK)
					     (P-CTRL-STK-SIZE CTRL-STK)))))
            (member (cc (mg-meaning-r (begin-body stmt) proc-list mg-state (sub1 n)
				      (LIST (LENGTH TEMP-STK)
					    (P-CTRL-STK-SIZE CTRL-STK))))
		    (when-labels stmt)))
       (AND (OK-MG-STATEMENT (WHEN-HANDLER STMT) R-COND-LIST NAME-ALIST PROC-LIST)
	    (OK-TRANSLATION-PARAMETERS
	     (ADD-CODE
	      (SET-LABEL-ALIST
	       (TRANSLATE (MAKE-CINFO (CODE CINFO)
				      (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
								(LABEL-CNT CINFO))
					      (LABEL-ALIST CINFO))
				      (ADD1 (ADD1 (LABEL-CNT CINFO))))
			  T-COND-LIST
			  (BEGIN-BODY STMT)
			  PROC-LIST)
	       (LABEL-ALIST CINFO))
	      (CONS (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
		    (CONS (CONS 'DL
				(CONS (LABEL-CNT CINFO)
				      '(NIL (PUSH-CONSTANT (NAT 2)))))
			  '((POP-GLOBAL C-C)))))
	     T-COND-LIST
	     (WHEN-HANDLER STMT)
	     PROC-LIST
	     (CONS (CONS 'DL
			 (CONS (ADD1 (LABEL-CNT CINFO))
			       '(NIL (NO-OP))))
		   CODE2))
	    (OK-MG-STATEP
	     (SET-CONDITION (MG-MEANING-R (BEGIN-BODY STMT)
					  PROC-LIST MG-STATE
					  (SUB1 N)
					  (LIST (LENGTH TEMP-STK)
						(P-CTRL-STK-SIZE CTRL-STK)))
			    'NORMAL)
	     R-COND-LIST)
	    (EQUAL
	     (CODE (TRANSLATE-DEF-BODY (ASSOC SUBR PROC-LIST)
				       PROC-LIST))
	     (APPEND
	      (CODE
	       (TRANSLATE
		(ADD-CODE
		 (SET-LABEL-ALIST
		  (TRANSLATE (MAKE-CINFO (CODE CINFO)
					 (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
								   (LABEL-CNT CINFO))
						 (LABEL-ALIST CINFO))
					 (ADD1 (ADD1 (LABEL-CNT CINFO))))
			     T-COND-LIST
			     (BEGIN-BODY STMT)
			     PROC-LIST)
		  (LABEL-ALIST CINFO))
		 (CONS (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
		       (CONS (CONS 'DL
				   (CONS (LABEL-CNT CINFO)
					 '(NIL (PUSH-CONSTANT (NAT 2)))))
			     '((POP-GLOBAL C-C)))))
		T-COND-LIST
		(WHEN-HANDLER STMT)
		PROC-LIST))
	      (CONS (CONS 'DL
			  (CONS (ADD1 (LABEL-CNT CINFO))
				'(NIL (NO-OP))))
		    CODE2)))
	    (MG-VARS-LIST-OK-IN-P-STATE
	     (MG-ALIST (SET-CONDITION (MG-MEANING-R (BEGIN-BODY STMT)
						    PROC-LIST MG-STATE
						    (SUB1 N)
						    (LIST (LENGTH TEMP-STK)
							  (P-CTRL-STK-SIZE CTRL-STK)))
				      'NORMAL))
	     (BINDINGS (TOP CTRL-STK))
	     TEMP-STK)
	    (NO-P-ALIASING
	     (BINDINGS (TOP CTRL-STK))
	     (MG-ALIST (SET-CONDITION (MG-MEANING-R (BEGIN-BODY STMT)
						    PROC-LIST MG-STATE
						    (SUB1 N)
						    (LIST (LENGTH TEMP-STK)
							  (P-CTRL-STK-SIZE CTRL-STK)))
				      'NORMAL)))
	    (SIGNATURES-MATCH
	     (MG-ALIST (SET-CONDITION (MG-MEANING-R (BEGIN-BODY STMT)
						    PROC-LIST MG-STATE
						    (SUB1 N)
						    (LIST (LENGTH TEMP-STK)
							  (P-CTRL-STK-SIZE CTRL-STK)))
				      'NORMAL))
	     NAME-ALIST)
	    (NORMAL (SET-CONDITION (MG-MEANING-R (BEGIN-BODY STMT)
						 PROC-LIST MG-STATE
						 (SUB1 N)
						 (LIST (LENGTH TEMP-STK)
						       (P-CTRL-STK-SIZE CTRL-STK)))
				   'NORMAL))
	    (ALL-CARS-UNIQUE
	     (MG-ALIST (SET-CONDITION (MG-MEANING-R (BEGIN-BODY STMT)
						    PROC-LIST MG-STATE
						    (SUB1 N)
						    (LIST (LENGTH TEMP-STK)
							  (P-CTRL-STK-SIZE CTRL-STK)))
				      'NORMAL)))
	    (NOT
	     (RESOURCE-ERRORP
	      (MG-MEANING-R
	       (WHEN-HANDLER STMT)
	       PROC-LIST
	       (SET-CONDITION (MG-MEANING-R (BEGIN-BODY STMT)
					    PROC-LIST MG-STATE
					    (SUB1 N)
					    (LIST (LENGTH TEMP-STK)
						  (P-CTRL-STK-SIZE CTRL-STK)))
			      'NORMAL)
	       (SUB1 N)
	       (LIST (LENGTH TEMP-STK)
		     (P-CTRL-STK-SIZE CTRL-STK)))))))
 ((INSTRUCTIONS PROMOTE
                (DIVE 2 2 2 2 2 2 2 2 2)
                PUSH TOP
                (= (MG-MEANING-R (BEGIN-BODY STMT)
                                 PROC-LIST MG-STATE
                                 (SUB1 N)
                                 (LIST (LENGTH TEMP-STK)
                                       (P-CTRL-STK-SIZE CTRL-STK)))
                   (MG-MEANING (BEGIN-BODY STMT)
                               PROC-LIST MG-STATE
                               (SUB1 N))
                   0)
                SPLIT
                (REWRITE OK-BEGIN-STATEMENT)
                X
                (S LEMMAS)
                SPLIT
                (DEMOTE 6)
                (DIVE 1)
                X
                (DIVE 2 1 1 1)
                (REWRITE BEGIN-TRANSLATION-2)
                UP
                (S LEMMAS)
                TOP
                (ENABLE ADD-CODE)
                (S LEMMAS)
                S
                (PROVE (ENABLE OK-MG-STATEMENT))
                S X
                (REWRITE MG-MEANING-PRESERVES-MG-ALISTP
                         (($R-COND-LIST (APPEND (WHEN-LABELS STMT)
                                                R-COND-LIST))))
                (REWRITE BEGIN-BODY-HYPS)
                (REWRITE BEGIN-BODY-HYPS)
                (DIVE 1)
                =
                (DIVE 1 1)
                (REWRITE BEGIN-TRANSLATION-2)
                TOP PROVE S
                (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)
                S
                (REWRITE SIGNATURES-MATCH-PRESERVES-NO-P-ALIASING
                         (($ALIST1 (MG-ALIST MG-STATE))))
                (REWRITE MG-MEANING-PRESERVES-SIGNATURES-MATCH)
                (REWRITE OK-MG-STATEP-ALIST-PLISTP)
                S
                (REWRITE SIGNATURES-MATCH-REORDER
                         (($ALIST1 (MG-ALIST MG-STATE))))
                (REWRITE OK-MG-STATEP-ALIST-PLISTP)
                (REWRITE MG-MEANING-PRESERVES-SIGNATURES-MATCH)
                (REWRITE OK-MG-STATEP-ALIST-PLISTP)
                S S
                (REWRITE SIGNATURES-MATCH-PRESERVES-UNIQUENESS-OF-CARS
                         (($X (MG-ALIST MG-STATE))))
                (REWRITE MG-MEANING-PRESERVES-SIGNATURES-MATCH)
                (REWRITE OK-MG-STATEP-ALIST-PLISTP)
                (DIVE 1)
                (REWRITE MG-MEANING-EQUIVALENCE)
                TOP S S
                (DIVE 1)
                (REWRITE BEGIN-BODY-DOESNT-HALT)
                TOP S S
                (DIVE 1)
                (REWRITE BEGIN-WHEN-ARM-DOESNT-HALT)
                TOP S)))
\end{verbatim}


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

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

\begin{tabbing}{\sc Theorem}:  append-doesnt-affect-fetch-label \\ \index{append-doesnt-affect-fetch-labe!l}
\=\+({\it{x\/}} $\not\in$ {\it{lst\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{fetch-label}}\,({\it{x\/}}, {\rm{append}}\,({\rm{make-label-alist}}\,({\it{lst\/}}, {\it{label\/}})\index{make-label-alist}, {\it{label-alist\/}}))\index{fetch-label} \\ 
$=$$\;\;\;\;${\rm{fetch-label}}\,({\it{x\/}}, {\it{label-alist\/}})\index{fetch-label})\-\-
\end{tabbing}


\noindent{\sc Event}:   Enable nullify.

\addvspace{18pt}

%\item 
\begin{verbatim}


(prove-lemma begin-state2-normal-body-step1 (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) 'BEGIN-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 (begin-body stmt) proc-list mg-state (sub1 n)
				   (LIST (LENGTH TEMP-STK)
					 (P-CTRL-STK-SIZE CTRL-STK)))))
	(equal 
	 (p-step
	   (P-STATE                                                      ;; state2
	       (TAG 'PC
		    (CONS SUBR
			  (IF
			   (NORMAL (MG-MEANING-R (BEGIN-BODY STMT)
						 PROC-LIST MG-STATE
						 (SUB1 N)
						 (LIST (LENGTH TEMP-STK)
						       (P-CTRL-STK-SIZE CTRL-STK))))
			   (LENGTH
			    (CODE
			     (TRANSLATE (MAKE-CINFO (CODE CINFO)
						    (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
									      (LABEL-CNT CINFO))
							    (LABEL-ALIST CINFO))
						    (ADD1 (ADD1 (LABEL-CNT CINFO))))
					T-COND-LIST
					(BEGIN-BODY STMT)
					PROC-LIST)))
			   (FIND-LABEL
			    (FETCH-LABEL
			     (CC (MG-MEANING-R (BEGIN-BODY STMT)
					       PROC-LIST MG-STATE
					       (SUB1 N)
					       (LIST (LENGTH TEMP-STK)
						     (P-CTRL-STK-SIZE CTRL-STK))))
			     (LABEL-ALIST
			      (TRANSLATE (MAKE-CINFO (CODE CINFO)
						     (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
									       (LABEL-CNT CINFO))
							     (LABEL-ALIST CINFO))
						     (ADD1 (ADD1 (LABEL-CNT CINFO))))
					 T-COND-LIST
					 (BEGIN-BODY STMT)
					 PROC-LIST)))
			    (APPEND
			     (CODE
			      (TRANSLATE (MAKE-CINFO (CODE CINFO)
						     (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
									       (LABEL-CNT CINFO))
							     (LABEL-ALIST CINFO))
						     (ADD1 (ADD1 (LABEL-CNT CINFO))))
					 T-COND-LIST
					 (BEGIN-BODY STMT)
					 PROC-LIST))
			     (CONS
			      (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
			      (CONS
			       (CONS 'DL
				     (CONS (LABEL-CNT CINFO)
					   '(NIL (PUSH-CONSTANT (NAT 2)))))
			       (CONS
				'(POP-GLOBAL C-C)
				(APPEND
				 (CODE
				  (TRANSLATE
				   (NULLIFY
				    (SET-LABEL-ALIST
				     (TRANSLATE
				      (MAKE-CINFO (CODE CINFO)
						  (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
									    (LABEL-CNT CINFO))
							  (LABEL-ALIST CINFO))
						  (ADD1 (ADD1 (LABEL-CNT CINFO))))
				      T-COND-LIST
				      (BEGIN-BODY STMT)
				      PROC-LIST)
				     (LABEL-ALIST CINFO)))
				   T-COND-LIST
				   (WHEN-HANDLER STMT)
				   PROC-LIST))
				 (CONS (CONS 'DL
					     (CONS (ADD1 (LABEL-CNT CINFO))
						   '(NIL (NO-OP))))
				       CODE2))))))))))
	       CTRL-STK
	       (MAP-DOWN-VALUES
		(MG-ALIST (MG-MEANING-R (BEGIN-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 (BEGIN-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 (CODE CINFO)
						    (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
									      (LABEL-CNT CINFO))
							    (LABEL-ALIST CINFO))
						    (ADD1 (ADD1 (LABEL-CNT CINFO))))
					T-COND-LIST
					(BEGIN-BODY STMT)
					PROC-LIST)))
		      (ADD1
		       (ADD1
			(ADD1
			 (LENGTH
			  (CODE
			   (TRANSLATE
			    (MAKE-CINFO NIL
					(LABEL-ALIST CINFO)
					(LABEL-CNT
					 (TRANSLATE (MAKE-CINFO (CODE CINFO)
								(APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
											  (LABEL-CNT CINFO))
									(LABEL-ALIST CINFO))
								(ADD1 (ADD1 (LABEL-CNT CINFO))))
						    T-COND-LIST
						    (BEGIN-BODY STMT)
						    PROC-LIST)))
			    T-COND-LIST
			    (WHEN-HANDLER STMT)
			    PROC-LIST)))))))))
	  CTRL-STK
	  (MAP-DOWN-VALUES (MG-ALIST (MG-MEANING-R (BEGIN-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 (BEGIN-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)))
 ((INSTRUCTIONS 
   PROMOTE (DIVE 1) X (S LEMMAS) (DIVE 1 1 2) (REWRITE TRANSLATE-DEF-BODY-REWRITE)
   (REWRITE BEGIN-CODE-REWRITE1) UP (REWRITE GET-LENGTH-CAR) S UP X UP X (DIVE 1)
   X UP S X (S LEMMAS) (DIVE 1 2 1) (REWRITE DEFINEDP-CAR-ASSOC) NX (DIVE 2)
   (REWRITE TRANSLATE-DEF-BODY-REWRITE) (REWRITE BEGIN-CODE-REWRITE1) UP
   (REWRITE FIND-LABEL-APPEND) (DIVE 2) X (DIVE 1) X (DIVE 1) X (DIVE 1)
   (REWRITE FIND-LABEL-APPEND) (DIVE 2) X TOP (S LEMMAS) (DIVE 1)
   (REWRITE FIND-LABELP-MONOTONIC-LESSP) TOP S S (REWRITE LABEL-CNT-MONOTONIC3)
   PROVE S (DIVE 1) (REWRITE FIND-LABELP-MONOTONIC-LESSP) TOP S PROVE S (DIVE 1)
   (REWRITE BEGIN-FIND-LABELP-LEMMA1) TOP S (REWRITE CAR-DEFINEDP-DEFINED-PROCP))))
\end{verbatim}


\begin{tabbing}{\sc Theorem}:  begin-state2-normal-body-step2-equals-final \\ \index{begin-state2-normal-body-step2-eq!uals-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{begin-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{begin-body}}\,({\it{stmt\/}})\index{begin-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-step}}\,({\rm{p-state}}\,(\=\+{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,(\=\+{\it{subr\/}}, \\ 
\=\+{\rm{length}}\,({\rm{code}}\,({\rm{translate}}\,(\=\+{\rm{make-cinfo}}\,(\=\+{\rm{code}}\,({\it{cinfo\/}})\index{code}, \\ 
{\rm{append}}\,(\=\+{\rm{make-label-alist}}\,(\=\+{\rm{when-labels}}\,({\it{stmt\/}})\index{when-labels}, \\ 
{\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt})\-\index{make-label-alist}, \\ 
{\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{begin-body}}\,({\it{stmt\/}})\index{begin-body}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code})\index{length} \\ 
$+$$\;\;\;\;$($1\;+$ ($1\;+$ ($1\;+$ {\rm{length}}\,({\rm{code}}\,({\rm{translate}}\,(\=\+{\rm{make-cinfo}}\,(\=\+{\bf{nil}}, \\ 
{\rm{label-alist}}\,({\it{cinfo\/}})\index{label-alist}, \\ 
{\rm{label-cnt}}\,({\rm{translate}}\,(\=\+{\rm{make-cinfo}}\,(\=\+{\rm{code}}\,({\it{cinfo\/}})\index{code}, \\ 
{\rm{append}}\,(\=\+{\rm{make-label-alist}}\,(\=\+{\rm{when-labels}}\,({\it{stmt\/}})\index{when-labels}, \\ 
{\rm{label-cnt}}\,({\it{cinfo\/}})\index{label-cnt})\-\index{make-label-alist}, \\ 
{\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{begin-body}}\,({\it{stmt\/}})\index{begin-body}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{label-cnt})\-\index{make-cinfo}, \\ 
{\it{t-cond-list\/}}, \\ 
{\rm{when-handler}}\,({\it{stmt\/}})\index{when-handler}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code})\index{length})))\-)\-)\-\index{tag}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\rm{map-down-values}}\,(\=\+{\rm{mg-alist}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{begin-body}}\,({\it{stmt\/}})\index{begin-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{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{begin-body}}\,({\it{stmt\/}})\index{begin-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{cc}, \\ 
{\it{t-cond-list\/}})\-\index{mg-cond-to-p-nat})\-), \\ 
{\sc{mg-max-ctrl-stk-size}}\index{mg-max-ctrl-stk-size}, \\ 
{\sc{mg-max-temp-stk-size}}\index{mg-max-temp-stk-size}, \\ 
{\sc{mg-word-size}}\index{mg-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state})\index{p-step} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,(\=\+{\it{subr\/}}, \\ 
\=\+{\bf if }{\rm{normal}}\,({\rm{mg-meaning-r}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{normal} \\ 
{\bf then }{\rm{length}}\,({\rm{code}}\,({\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code})\index{length} \\ 
{\bf else }{\rm{find-label}}\,(\=\+{\rm{fetch-label}}\,(\=\+{\rm{cc}}\,({\rm{mg-meaning-r}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{cc}, \\ 
{\rm{label-alist}}\,({\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{label-alist})\-\index{fetch-label}, \\ 
{\rm{append}}\,(\=\+{\rm{code}}\,({\rm{translate}}\,(\=\+{\it{cinfo\/}}, \\ 
{\it{t-cond-list\/}}, \\ 
{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{translate})\index{code}, \\ 
{\it{code2\/}})\-)\-\index{find-label}$\;${\bf  endif}\-)\-)\-\index{tag}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\rm{map-down-values}}\,(\=\+{\rm{mg-alist}}\,({\rm{mg-meaning-r}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{mg-alist}, \\ 
{\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings}, \\ 
{\it{temp-stk\/}})\-\index{map-down-values}, \\ 
{\rm{translate-proc-list}}\,({\it{proc-list\/}})\index{translate-proc-list}, \\ 
{\rm{list}}\,({\rm{list}}\,(\=\+{\tt{'}}{\tt{c-c}}, \\ 
{\rm{mg-cond-to-p-nat}}\,(\=\+{\rm{cc}}\,({\rm{mg-meaning-r}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{cc}, \\ 
{\it{t-cond-list\/}})\-\index{mg-cond-to-p-nat})\-), \\ 
{\sc{mg-max-ctrl-stk-size}}\index{mg-max-ctrl-stk-size}, \\ 
{\sc{mg-max-temp-stk-size}}\index{mg-max-temp-stk-size}, \\ 
{\sc{mg-word-size}}\index{mg-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state})\-\-
\end{tabbing}

%\item 
\begin{verbatim}


(prove-lemma begin-nonnormal-nonwhen-body-state2-equals-final (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) 'BEGIN-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)))))
            (not (normal (mg-meaning-r (begin-body stmt) proc-list mg-state (sub1 n)
				       (LIST (LENGTH TEMP-STK)
					     (P-CTRL-STK-SIZE CTRL-STK)))))
	    (not (member (cc (mg-meaning-r (begin-body stmt) proc-list mg-state (sub1 n)
					   (LIST (LENGTH TEMP-STK)
						 (P-CTRL-STK-SIZE CTRL-STK))))
			 (when-labels stmt))))
     (equal (P-STATE                                                      ;; state2
	       (TAG 'PC
		    (CONS SUBR
			  (IF
			   (NORMAL (MG-MEANING-R (BEGIN-BODY STMT)
						 PROC-LIST MG-STATE
						 (SUB1 N)
						 (LIST (LENGTH TEMP-STK)
						       (P-CTRL-STK-SIZE CTRL-STK))))
			   (LENGTH
			    (CODE
			     (TRANSLATE (MAKE-CINFO (CODE CINFO)
						    (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
									      (LABEL-CNT CINFO))
							    (LABEL-ALIST CINFO))
						    (ADD1 (ADD1 (LABEL-CNT CINFO))))
					T-COND-LIST
					(BEGIN-BODY STMT)
					PROC-LIST)))
			   (FIND-LABEL
			    (FETCH-LABEL
			     (CC (MG-MEANING-R (BEGIN-BODY STMT)
					       PROC-LIST MG-STATE
					       (SUB1 N)
					       (LIST (LENGTH TEMP-STK)
						     (P-CTRL-STK-SIZE CTRL-STK))))
			     (LABEL-ALIST
			      (TRANSLATE (MAKE-CINFO (CODE CINFO)
						     (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
									       (LABEL-CNT CINFO))
							     (LABEL-ALIST CINFO))
						     (ADD1 (ADD1 (LABEL-CNT CINFO))))
					 T-COND-LIST
					 (BEGIN-BODY STMT)
					 PROC-LIST)))
			    (APPEND
			     (CODE
			      (TRANSLATE (MAKE-CINFO (CODE CINFO)
						     (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
									       (LABEL-CNT CINFO))
							     (LABEL-ALIST CINFO))
						     (ADD1 (ADD1 (LABEL-CNT CINFO))))
					 T-COND-LIST
					 (BEGIN-BODY STMT)
					 PROC-LIST))
			     (CONS
			      (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
			      (CONS
			       (CONS 'DL
				     (CONS (LABEL-CNT CINFO)
					   '(NIL (PUSH-CONSTANT (NAT 2)))))
			       (CONS
				'(POP-GLOBAL C-C)
				(APPEND
				 (CODE
				  (TRANSLATE
				   (NULLIFY
				    (SET-LABEL-ALIST
				     (TRANSLATE
				      (MAKE-CINFO (CODE CINFO)
						  (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
									    (LABEL-CNT CINFO))
							  (LABEL-ALIST CINFO))
						  (ADD1 (ADD1 (LABEL-CNT CINFO))))
				      T-COND-LIST
				      (BEGIN-BODY STMT)
				      PROC-LIST)
				     (LABEL-ALIST CINFO)))
				   T-COND-LIST
				   (WHEN-HANDLER STMT)
				   PROC-LIST))
				 (CONS (CONS 'DL
					     (CONS (ADD1 (LABEL-CNT CINFO))
						   '(NIL (NO-OP))))
				       CODE2))))))))))
	       CTRL-STK
	       (MAP-DOWN-VALUES
		(MG-ALIST (MG-MEANING-R (BEGIN-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 (BEGIN-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
		      (IF
		       (NORMAL (MG-MEANING-R STMT PROC-LIST MG-STATE N
					     (LIST (LENGTH TEMP-STK)
						   (P-CTRL-STK-SIZE CTRL-STK))))
		       (LENGTH (CODE (TRANSLATE CINFO T-COND-LIST STMT PROC-LIST)))
		       (FIND-LABEL
			(FETCH-LABEL (CC (MG-MEANING-R STMT PROC-LIST MG-STATE N
						       (LIST (LENGTH TEMP-STK)
							     (P-CTRL-STK-SIZE CTRL-STK))))
				     (LABEL-ALIST (TRANSLATE CINFO T-COND-LIST STMT
							     PROC-LIST)))
			(APPEND (CODE (TRANSLATE CINFO T-COND-LIST STMT PROC-LIST))
				CODE2)))))
	   CTRL-STK
	   (MAP-DOWN-VALUES (MG-ALIST (MG-MEANING-R STMT PROC-LIST MG-STATE N
						    (LIST (LENGTH TEMP-STK)
							  (P-CTRL-STK-SIZE CTRL-STK))))
			    (BINDINGS (TOP CTRL-STK))
			    TEMP-STK)
	   (TRANSLATE-PROC-LIST PROC-LIST)
	   (LIST
	    (LIST 'C-C
		  (MG-COND-TO-P-NAT (CC (MG-MEANING-R STMT PROC-LIST MG-STATE N
						      (LIST (LENGTH TEMP-STK)
							    (P-CTRL-STK-SIZE CTRL-STK))))
				    T-COND-LIST)))
           (MG-MAX-CTRL-STK-SIZE)
           (MG-MAX-TEMP-STK-SIZE)
           (MG-WORD-SIZE)
	   'RUN)))
 ((INSTRUCTIONS PROMOTE
                (S LEMMAS)
                S
                (= (MG-MEANING-R STMT PROC-LIST MG-STATE N
                                 (LIST (LENGTH TEMP-STK)
                                       (P-CTRL-STK-SIZE CTRL-STK)))
                   (MG-MEANING-R (BEGIN-BODY STMT)
                                 PROC-LIST MG-STATE
                                 (SUB1 N)
                                 (LIST (LENGTH TEMP-STK)
                                       (P-CTRL-STK-SIZE CTRL-STK)))
                   0)
                S
                (DIVE 2 2 2 1)
                (= F)
                TOP S
                (DIVE 2)
                (DIVE 2 2 2 1)
                (REWRITE NEW-CODE-APPENDED-TO-OLD1)
                TOP S
                (S LEMMAS)
                X
                (S LEMMAS)
                (DIVE 1)
                (REWRITE BEGIN-MEANING-R-2)
                TOP S)))
\end{verbatim}


\begin{tabbing}{\sc Theorem}:  append-make-label-alist-fetch-label \\ \index{append-make-label-alist-fetch-l!abel}
\=\+({\it{x\/}} $\in$ {\it{lst\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{cdr}}\,({\rm{assoc}}\,({\it{x\/}}, {\rm{append}}\,({\rm{make-label-alist}}\,({\it{lst\/}}, {\it{label\/}})\index{make-label-alist}, {\it{label-alist\/}}))) \\ 
$=$$\;\;\;\;${\it{label\/}})\-\-
\end{tabbing}

%\item 
\begin{verbatim}


(prove-lemma begin-when-signalled-state2-step1 (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) 'BEGIN-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)))))
            (not (normal (mg-meaning-r (begin-body stmt) proc-list mg-state (sub1 n)
				       (LIST (LENGTH TEMP-STK)
					     (P-CTRL-STK-SIZE CTRL-STK)))))
	    (member (cc (mg-meaning-r (begin-body stmt) proc-list mg-state (sub1 n)
				      (LIST (LENGTH TEMP-STK)
					    (P-CTRL-STK-SIZE CTRL-STK))))
		    (when-labels stmt)))
       (equal
	(p-step
          (P-STATE                                                      ;; state2
	       (TAG 'PC
		    (CONS SUBR
			  (IF
			   (NORMAL (MG-MEANING-R (BEGIN-BODY STMT)
						 PROC-LIST MG-STATE
						 (SUB1 N)
						 (LIST (LENGTH TEMP-STK)
						       (P-CTRL-STK-SIZE CTRL-STK))))
			   (LENGTH
			    (CODE
			     (TRANSLATE (MAKE-CINFO (CODE CINFO)
						    (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
									      (LABEL-CNT CINFO))
							    (LABEL-ALIST CINFO))
						    (ADD1 (ADD1 (LABEL-CNT CINFO))))
					T-COND-LIST
					(BEGIN-BODY STMT)
					PROC-LIST)))
			   (FIND-LABEL
			    (FETCH-LABEL
			     (CC (MG-MEANING-R (BEGIN-BODY STMT)
					       PROC-LIST MG-STATE
					       (SUB1 N)
					       (LIST (LENGTH TEMP-STK)
						     (P-CTRL-STK-SIZE CTRL-STK))))
			     (LABEL-ALIST
			      (TRANSLATE (MAKE-CINFO (CODE CINFO)
						     (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
									       (LABEL-CNT CINFO))
							     (LABEL-ALIST CINFO))
						     (ADD1 (ADD1 (LABEL-CNT CINFO))))
					 T-COND-LIST
					 (BEGIN-BODY STMT)
					 PROC-LIST)))
			    (APPEND
			     (CODE
			      (TRANSLATE (MAKE-CINFO (CODE CINFO)
						     (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
									       (LABEL-CNT CINFO))
							     (LABEL-ALIST CINFO))
						     (ADD1 (ADD1 (LABEL-CNT CINFO))))
					 T-COND-LIST
					 (BEGIN-BODY STMT)
					 PROC-LIST))
			     (CONS
			      (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
			      (CONS
			       (CONS 'DL
				     (CONS (LABEL-CNT CINFO)
					   '(NIL (PUSH-CONSTANT (NAT 2)))))
			       (CONS
				'(POP-GLOBAL C-C)
				(APPEND
				 (CODE
				  (TRANSLATE
				   (NULLIFY
				    (SET-LABEL-ALIST
				     (TRANSLATE
				      (MAKE-CINFO (CODE CINFO)
						  (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
									    (LABEL-CNT CINFO))
							  (LABEL-ALIST CINFO))
						  (ADD1 (ADD1 (LABEL-CNT CINFO))))
				      T-COND-LIST
				      (BEGIN-BODY STMT)
				      PROC-LIST)
				     (LABEL-ALIST CINFO)))
				   T-COND-LIST
				   (WHEN-HANDLER STMT)
				   PROC-LIST))
				 (CONS (CONS 'DL
					     (CONS (ADD1 (LABEL-CNT CINFO))
						   '(NIL (NO-OP))))
				       CODE2))))))))))
	       CTRL-STK
	       (MAP-DOWN-VALUES
		(MG-ALIST (MG-MEANING-R (BEGIN-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 (BEGIN-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 (CODE CINFO)
						 (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
									   (LABEL-CNT CINFO))
							 (LABEL-ALIST CINFO))
						 (ADD1 (ADD1 (LABEL-CNT CINFO))))
				     T-COND-LIST
				     (BEGIN-BODY STMT)
				     PROC-LIST)))
		       2)))
	   CTRL-STK
	   (PUSH
	    '(NAT 2)
	    (MAP-DOWN-VALUES (MG-ALIST (MG-MEANING-R (BEGIN-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 (BEGIN-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)))
    ((INSTRUCTIONS 
      PROMOTE (DIVE 1) X (S LEMMAS) UP (DIVE 1 1 1 1) (REWRITE FIND-LABEL-APPEND) (DIVE 2)
      X (DIVE 1) X UP UP NX (REWRITE TRANSLATE-DEF-BODY-REWRITE) (REWRITE BEGIN-CODE-REWRITE1)
      UP (REWRITE GET-LENGTH-PLUS) X UP X UP X (S LEMMAS) (DIVE 1) X (DIVE 1)
      (REWRITE MAP-DOWN-VALUES-PRESERVES-LENGTH) UP (REWRITE RESOURCES-ADEQUATE-TEMP-STK-NOT-MAX)
      UP S (S LEMMAS) (DIVE 1 2 2 1) (REWRITE FIND-LABEL-APPEND) (DIVE 2) 
      (= * 1 ((ENABLE FIND-LABELP))) TOP S PROVE (DIVE 1) (REWRITE FIND-LABELP-MONOTONIC-LESSP)
      UP S S PROVE S (DIVE 1) (REWRITE BEGIN-FIND-LABELP-LEMMA2) TOP S
      (REWRITE SIGNATURES-MATCH-PRESERVES-MG-VARS-LIST-OK (($X (MG-ALIST MG-STATE))))
      (DIVE 2 1) (REWRITE MG-MEANING-EQUIVALENCE) TOP
      (REWRITE MG-MEANING-PRESERVES-SIGNATURES-MATCH) (REWRITE OK-MG-STATEP-ALIST-PLISTP) S
      (DIVE 1) (REWRITE BEGIN-BODY-DOESNT-HALT) TOP S (DIVE 1 1) (REWRITE MG-MEANING-EQUIVALENCE)
      TOP 
      (REWRITE MG-MEANING-PRESERVES-MG-ALISTP (($R-COND-LIST (APPEND (WHEN-LABELS STMT) R-COND-LIST))))
      (REWRITE BEGIN-BODY-HYPS) (REWRITE BEGIN-BODY-HYPS) S (DIVE 1) (REWRITE BEGIN-BODY-DOESNT-HALT)
      TOP S (DIVE 1) (REWRITE FIND-LABELP-MONOTONIC-LESSP) TOP S S PROVE S (DIVE 1)
      (REWRITE BEGIN-FIND-LABELP-LEMMA2) TOP S)))
\end{verbatim}


\begin{verbatim};; The result of the (pop-global c-c) instruction should equal state3

\end{verbatim}%\item 
\begin{verbatim}


;; The result of the (pop-global c-c) instruction should equal state3

(prove-lemma begin-when-signalled-state2-step2 (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) 'BEGIN-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)))))
            (not (normal (mg-meaning-r (begin-body stmt) proc-list mg-state (sub1 n)
				       (LIST (LENGTH TEMP-STK)
					     (P-CTRL-STK-SIZE CTRL-STK)))))
	    (member (cc (mg-meaning-r (begin-body stmt) proc-list mg-state (sub1 n)
				      (LIST (LENGTH TEMP-STK)
					    (P-CTRL-STK-SIZE CTRL-STK))))
		    (when-labels stmt)))
       (equal
	(p-step
          (P-STATE
	   (TAG 'PC
		(CONS SUBR
		     (PLUS
			(LENGTH
			 (CODE
			  (TRANSLATE (MAKE-CINFO (CODE CINFO)
						 (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
									   (LABEL-CNT CINFO))
							 (LABEL-ALIST CINFO))
						 (ADD1 (ADD1 (LABEL-CNT CINFO))))
				     T-COND-LIST
				     (BEGIN-BODY STMT)
				     PROC-LIST)))
		       2)))
	   CTRL-STK
	   (PUSH
	    '(NAT 2)
	    (MAP-DOWN-VALUES (MG-ALIST (MG-MEANING-R (BEGIN-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 (BEGIN-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                                               ;; state3
		(SET-CONDITION (MG-MEANING-R (BEGIN-BODY STMT)
					     PROC-LIST MG-STATE
					     (SUB1 N)
					     (LIST (LENGTH TEMP-STK)
						   (P-CTRL-STK-SIZE CTRL-STK)))
			       'NORMAL)
		PROC-LIST CTRL-STK TEMP-STK
		(TAG 'PC
		     (CONS SUBR
			   (LENGTH
			    (CODE
			     (ADD-CODE
			      (SET-LABEL-ALIST
			       (TRANSLATE (MAKE-CINFO (CODE CINFO)
						      (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
										(LABEL-CNT CINFO))
							      (LABEL-ALIST CINFO))
						      (ADD1 (ADD1 (LABEL-CNT CINFO))))
					  T-COND-LIST
					  (BEGIN-BODY STMT)
					  PROC-LIST)
			       (LABEL-ALIST CINFO))
			      (CONS (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
				    (CONS (CONS 'DL
						(CONS (LABEL-CNT CINFO)
						      '(NIL (PUSH-CONSTANT (NAT 2)))))
					  '((POP-GLOBAL C-C)))))))))
		T-COND-LIST)))
     ((INSTRUCTIONS 
       PROMOTE (DIVE 1) X (S LEMMAS) (DIVE 1 1 2) (REWRITE TRANSLATE-DEF-BODY-REWRITE)
       (REWRITE BEGIN-CODE-REWRITE1) UP (REWRITE GET-LENGTH-PLUS) X X UP X UP X
       (S LEMMAS) (DIVE 1) X UP S (S LEMMAS) S UP (ENABLE MAP-DOWN) S
       (PROVE (ENABLE MG-COND-TO-P-NAT CONDITION-INDEX)))))
\end{verbatim}


%\item 
\begin{verbatim}


(prove-lemma begin-when-nonnormal-state4-equals-final (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) 'BEGIN-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)))))
            (not (normal (mg-meaning-r (begin-body stmt) proc-list mg-state (sub1 n)
				       (LIST (LENGTH TEMP-STK)
					     (P-CTRL-STK-SIZE CTRL-STK)))))
	    (member (cc (mg-meaning-r (begin-body stmt) proc-list mg-state (sub1 n)
				      (LIST (LENGTH TEMP-STK)
					    (P-CTRL-STK-SIZE CTRL-STK))))
		    (when-labels stmt))
            (not (normal 
		  (mg-meaning-r (when-handler stmt) proc-list
				(set-condition (mg-meaning-r (begin-body stmt) proc-list mg-state (sub1 n)
							     (LIST (LENGTH TEMP-STK)
								   (P-CTRL-STK-SIZE CTRL-STK)))
					       'normal)
				(sub1 n) (LIST (LENGTH TEMP-STK) (P-CTRL-STK-SIZE CTRL-STK))))))
     (equal 
	(P-STATE
	 (TAG 'PC
	      (CONS SUBR
		    (IF
		     (NORMAL
		      (MG-MEANING-R
		       (WHEN-HANDLER STMT)
		       PROC-LIST
		       (SET-CONDITION (MG-MEANING-R (BEGIN-BODY STMT)
						    PROC-LIST MG-STATE
						    (SUB1 N)
						    (LIST (LENGTH TEMP-STK)
							  (P-CTRL-STK-SIZE CTRL-STK)))
				      'NORMAL)
		       (SUB1 N)
		       (LIST (LENGTH TEMP-STK)
			     (P-CTRL-STK-SIZE CTRL-STK))))
		     (LENGTH
		      (CODE
		       (TRANSLATE
			(ADD-CODE
			 (SET-LABEL-ALIST
			  (TRANSLATE
			   (MAKE-CINFO (CODE CINFO)
				       (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
								 (LABEL-CNT CINFO))
					       (LABEL-ALIST CINFO))
				       (ADD1 (ADD1 (LABEL-CNT CINFO))))
			   T-COND-LIST
			   (BEGIN-BODY STMT)
			   PROC-LIST)
			  (LABEL-ALIST CINFO))
			 (CONS (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
			       (CONS (CONS 'DL
					   (CONS (LABEL-CNT CINFO)
						 '(NIL (PUSH-CONSTANT (NAT 2)))))
				     '((POP-GLOBAL C-C)))))
			T-COND-LIST
			(WHEN-HANDLER STMT)
			PROC-LIST)))
		     (FIND-LABEL
		      (FETCH-LABEL
		       (CC
			(MG-MEANING-R
			 (WHEN-HANDLER STMT)
			 PROC-LIST
			 (SET-CONDITION (MG-MEANING-R (BEGIN-BODY STMT)
						      PROC-LIST MG-STATE
						      (SUB1 N)
						      (LIST (LENGTH TEMP-STK)
							    (P-CTRL-STK-SIZE CTRL-STK)))
					'NORMAL)
			 (SUB1 N)
			 (LIST (LENGTH TEMP-STK)
			       (P-CTRL-STK-SIZE CTRL-STK))))
		       (LABEL-ALIST
			(TRANSLATE
			 (ADD-CODE
			  (SET-LABEL-ALIST
			   (TRANSLATE
			    (MAKE-CINFO (CODE CINFO)
					(APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
								  (LABEL-CNT CINFO))
						(LABEL-ALIST CINFO))
					(ADD1 (ADD1 (LABEL-CNT CINFO))))
			    T-COND-LIST
			    (BEGIN-BODY STMT)
			    PROC-LIST)
			   (LABEL-ALIST CINFO))
			  (CONS (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
				(CONS (CONS 'DL
					    (CONS (LABEL-CNT CINFO)
						  '(NIL (PUSH-CONSTANT (NAT 2)))))
				      '((POP-GLOBAL C-C)))))
			 T-COND-LIST
			 (WHEN-HANDLER STMT)
			 PROC-LIST)))
		      (APPEND
		       (CODE
			(TRANSLATE
			 (ADD-CODE
			  (SET-LABEL-ALIST
			   (TRANSLATE
			    (MAKE-CINFO (CODE CINFO)
					(APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
								  (LABEL-CNT CINFO))
						(LABEL-ALIST CINFO))
					(ADD1 (ADD1 (LABEL-CNT CINFO))))
			    T-COND-LIST
			    (BEGIN-BODY STMT)
			    PROC-LIST)
			   (LABEL-ALIST CINFO))
			  (CONS (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
				(CONS (CONS 'DL
					    (CONS (LABEL-CNT CINFO)
						  '(NIL (PUSH-CONSTANT (NAT 2)))))
				      '((POP-GLOBAL C-C)))))
			 T-COND-LIST
			 (WHEN-HANDLER STMT)
			 PROC-LIST))
		       (CONS (CONS 'DL
				   (CONS (ADD1 (LABEL-CNT CINFO))
					 '(NIL (NO-OP))))
			     CODE2))))))
	 CTRL-STK
	 (MAP-DOWN-VALUES
	  (MG-ALIST
	   (MG-MEANING-R
	    (WHEN-HANDLER STMT)
	    PROC-LIST
	    (SET-CONDITION (MG-MEANING-R (BEGIN-BODY STMT)
					 PROC-LIST MG-STATE
					 (SUB1 N)
					 (LIST (LENGTH TEMP-STK)
					       (P-CTRL-STK-SIZE CTRL-STK)))
			   'NORMAL)
	    (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
		   (WHEN-HANDLER STMT)
		   PROC-LIST
		   (SET-CONDITION (MG-MEANING-R (BEGIN-BODY STMT)
						PROC-LIST MG-STATE
						(SUB1 N)
						(LIST (LENGTH TEMP-STK)
						      (P-CTRL-STK-SIZE CTRL-STK)))
				  'NORMAL)
		   (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 S
   (= (MG-MEANING-R STMT PROC-LIST MG-STATE N
		    (LIST (LENGTH TEMP-STK) (P-CTRL-STK-SIZE CTRL-STK)))
      (MG-MEANING-R
          (WHEN-HANDLER STMT) PROC-LIST
          (MG-STATE 'NORMAL
                    (MG-ALIST (MG-MEANING-R (BEGIN-BODY STMT) PROC-LIST MG-STATE (SUB1 N)
                                            (LIST (LENGTH TEMP-STK) (P-CTRL-STK-SIZE CTRL-STK))))
                    (MG-PSW (MG-MEANING-R (BEGIN-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))) 0)
   S (S LEMMAS) (DIVE 1 2 2 1) (= * F 0) UP S TOP (DIVE 2 2 2 1) (= * F 0) UP S TOP (S LEMMAS)
   (DEMOTE 21) S (S LEMMAS) (DEMOTE 21) S (S LEMMAS) (DIVE 1) (REWRITE BEGIN-MEANING-R-2) TOP S)))
\end{verbatim}


%\item 
\begin{verbatim}


(prove-lemma begin-when-normal-step-state4-equals-final (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) 'BEGIN-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)))))
            (not (normal (mg-meaning-r (begin-body stmt) proc-list mg-state (sub1 n)
				       (LIST (LENGTH TEMP-STK)
					     (P-CTRL-STK-SIZE CTRL-STK)))))
	    (member (cc (mg-meaning-r (begin-body stmt) proc-list mg-state (sub1 n)
				      (LIST (LENGTH TEMP-STK)
					    (P-CTRL-STK-SIZE CTRL-STK))))
		    (when-labels stmt))
            (normal 
	     (mg-meaning-r (when-handler stmt) proc-list
			   (set-condition (mg-meaning-r (begin-body stmt) proc-list mg-state (sub1 n)
							(LIST (LENGTH TEMP-STK)
							      (P-CTRL-STK-SIZE CTRL-STK)))
					  'normal)
			   (sub1 n) (LIST (LENGTH TEMP-STK) (P-CTRL-STK-SIZE CTRL-STK)))))
       (equal 
	(p-step
	  (P-STATE                                                    ;; state4
	       (TAG 'PC
		    (CONS SUBR
			  (IF
			   (NORMAL
			    (MG-MEANING-R
			     (WHEN-HANDLER STMT)
			     PROC-LIST
			     (SET-CONDITION (MG-MEANING-R (BEGIN-BODY STMT)
							  PROC-LIST MG-STATE
							  (SUB1 N)
							  (LIST (LENGTH TEMP-STK)
								(P-CTRL-STK-SIZE CTRL-STK)))
					    'NORMAL)
			     (SUB1 N)
			     (LIST (LENGTH TEMP-STK)
				   (P-CTRL-STK-SIZE CTRL-STK))))
			   (LENGTH
			    (CODE
			     (TRANSLATE
			      (ADD-CODE
			       (SET-LABEL-ALIST
				(TRANSLATE
				 (MAKE-CINFO (CODE CINFO)
					     (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
								       (LABEL-CNT CINFO))
						     (LABEL-ALIST CINFO))
					     (ADD1 (ADD1 (LABEL-CNT CINFO))))
				 T-COND-LIST
				 (BEGIN-BODY STMT)
				 PROC-LIST)
				(LABEL-ALIST CINFO))
			       (CONS (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
				     (CONS (CONS 'DL
						 (CONS (LABEL-CNT CINFO)
						       '(NIL (PUSH-CONSTANT (NAT 2)))))
					   '((POP-GLOBAL C-C)))))
			      T-COND-LIST
			      (WHEN-HANDLER STMT)
			      PROC-LIST)))
			   (FIND-LABEL
			    (FETCH-LABEL
			     (CC
			      (MG-MEANING-R
			       (WHEN-HANDLER STMT)
			       PROC-LIST
			       (SET-CONDITION (MG-MEANING-R (BEGIN-BODY STMT)
							    PROC-LIST MG-STATE
							    (SUB1 N)
							    (LIST (LENGTH TEMP-STK)
								  (P-CTRL-STK-SIZE CTRL-STK)))
					      'NORMAL)
			       (SUB1 N)
			       (LIST (LENGTH TEMP-STK)
				     (P-CTRL-STK-SIZE CTRL-STK))))
			     (LABEL-ALIST
			      (TRANSLATE
			       (ADD-CODE
				(SET-LABEL-ALIST
				 (TRANSLATE
				  (MAKE-CINFO (CODE CINFO)
					      (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
									(LABEL-CNT CINFO))
						      (LABEL-ALIST CINFO))
					      (ADD1 (ADD1 (LABEL-CNT CINFO))))
				  T-COND-LIST
				  (BEGIN-BODY STMT)
				  PROC-LIST)
				 (LABEL-ALIST CINFO))
				(CONS (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
				      (CONS (CONS 'DL
						  (CONS (LABEL-CNT CINFO)
							'(NIL (PUSH-CONSTANT (NAT 2)))))
					    '((POP-GLOBAL C-C)))))
			       T-COND-LIST
			       (WHEN-HANDLER STMT)
			       PROC-LIST)))
			    (APPEND
			     (CODE
			      (TRANSLATE
			       (ADD-CODE
				(SET-LABEL-ALIST
				 (TRANSLATE
				  (MAKE-CINFO (CODE CINFO)
					      (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
									(LABEL-CNT CINFO))
						      (LABEL-ALIST CINFO))
					      (ADD1 (ADD1 (LABEL-CNT CINFO))))
				  T-COND-LIST
				  (BEGIN-BODY STMT)
				  PROC-LIST)
				 (LABEL-ALIST CINFO))
				(CONS (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
				      (CONS (CONS 'DL
						  (CONS (LABEL-CNT CINFO)
							'(NIL (PUSH-CONSTANT (NAT 2)))))
					    '((POP-GLOBAL C-C)))))
			       T-COND-LIST
			       (WHEN-HANDLER STMT)
			       PROC-LIST))
			     (CONS (CONS 'DL
					 (CONS (ADD1 (LABEL-CNT CINFO))
					       '(NIL (NO-OP))))
				   CODE2))))))
	       CTRL-STK
	       (MAP-DOWN-VALUES
		(MG-ALIST
		 (MG-MEANING-R
		  (WHEN-HANDLER STMT)
		  PROC-LIST
		  (SET-CONDITION (MG-MEANING-R (BEGIN-BODY STMT)
					       PROC-LIST MG-STATE
					       (SUB1 N)
					       (LIST (LENGTH TEMP-STK)
						     (P-CTRL-STK-SIZE CTRL-STK)))
				 'NORMAL)
		  (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
			 (WHEN-HANDLER STMT)
			 PROC-LIST
			 (SET-CONDITION (MG-MEANING-R (BEGIN-BODY STMT)
						      PROC-LIST MG-STATE
						      (SUB1 N)
						      (LIST (LENGTH TEMP-STK)
							    (P-CTRL-STK-SIZE CTRL-STK)))
					'NORMAL)
			 (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 (DIVE 1) X (S LEMMAS) (DIVE 2 1 2 2 1) (= * T 0) UP S UP UP UP UP (DIVE 1 1 1 1)
      (= * T 0) UP S UP (DIVE 2) (REWRITE TRANSLATE-DEF-BODY-REWRITE) 
      (REWRITE BEGIN-CODE-REWRITE1) UP (DIVE 1 1) (REWRITE NEW-CODE-APPENDED-TO-OLD1) UP UP
      (ENABLE LENGTH-CONS) (S LEMMAS) (REWRITE GET-LENGTH-PLUS) X X X (REWRITE GET-LENGTH-CAR)
      S UP X UP X (DIVE 1) X UP S X (S LEMMAS) TOP S
      (= (MG-MEANING-R STMT PROC-LIST MG-STATE N 
		       (LIST (LENGTH TEMP-STK) (P-CTRL-STK-SIZE CTRL-STK)))
         (MG-MEANING-R
	  (WHEN-HANDLER STMT) PROC-LIST
	  (MG-STATE 'NORMAL
		    (MG-ALIST (MG-MEANING-R (BEGIN-BODY STMT) PROC-LIST MG-STATE (SUB1 N)
					    (LIST (LENGTH TEMP-STK) (P-CTRL-STK-SIZE CTRL-STK))))
		    'RUN)
	  (SUB1 N)
	  (LIST (LENGTH TEMP-STK) (P-CTRL-STK-SIZE CTRL-STK))) 0)
      S (DIVE 2 2 2 1) (= * T 0) TOP S (DIVE 2 2 2 1 1) (REWRITE BEGIN-TRANSLATION-2)
      TOP (PROVE (ENABLE ADD-CODE SET-LABEL-ALIST)) (DEMOTE 21) S (S LEMMAS) (DIVE 1)
      (REWRITE BEGIN-MEANING-R-2) TOP S (S LEMMAS) X (S LEMMAS) (DEMOTE 21) S (S LEMMAS)
      (DEMOTE 21) S (S LEMMAS))))
\end{verbatim}


\begin{tabbing}{\sc Theorem}:  begin-body-normal-exact-time-schema \\ \index{begin-body-normal-exact-time-sc!hema}
\=\+(\=\+({\it{stmt-time\/}} $=$ ({\tt{2}} $+$ {\it{body-time\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{p}}\,({\it{initial\/}}, {\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}:  begin-body-normal-clock \\ \index{begin-body-normal-clock}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{begin-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{r-cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\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{begin-body}}\,({\it{stmt\/}})\index{begin-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} \\ 
$=$$\;\;\;\;$({\tt{2}} $+$ {\rm{clock}}\,({\rm{begin-body}}\,({\it{stmt\/}})\index{begin-body}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}} $-\;1$)\index{clock}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  begin-body-nonnormal-nonwhen-exact-time-schema \\ \index{begin-body-nonnormal-nonwhen-ex!act-time-schema}
\=\+(\=\+({\it{stmt-time\/}} $=$ {\it{body-time\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{p}}\,({\it{initial\/}}, {\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}:  begin-body-nonnormal-nonwhen-clock \\ \index{begin-body-nonnormal-nonwhen-cl!ock}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{begin-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{r-cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\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{begin-body}}\,({\it{stmt\/}})\index{begin-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{begin-body}}\,({\it{stmt\/}})\index{begin-body}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}} $-\;1$, {\it{sizes\/}})\index{mg-meaning-r})\index{cc} \\ 
$\not\in$$\;\;\;\;${\rm{when-labels}}\,({\it{stmt\/}})\index{when-labels})\-)\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{clock}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}})\index{clock} \\ 
$=$$\;\;\;\;${\rm{clock}}\,({\rm{begin-body}}\,({\it{stmt\/}})\index{begin-body}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}} $-\;1$)\index{clock})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  begin-when-normal-exact-time-schema \\ \index{begin-when-normal-exact-time-sc!hema}
\=\+(\=\+({\it{stmt-time\/}} $=$ ({\it{body-time\/}} $+$ ({\tt{3}} $+$ {\it{when-arm-time\/}}))) \\ 
$\wedge$$\;\;\;\;$({\rm{p}}\,({\it{initial\/}}, {\it{body-time\/}})\index{p} $=$ {\it{state2\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{p}}\,({\it{state2\/}}, {\tt{2}})\index{p} $=$ {\it{state3\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{p}}\,({\it{state3\/}}, {\it{when-arm-time\/}})\index{p} $=$ {\it{state4\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{p-step}}\,({\it{state4\/}})\index{p-step} $=$ {\it{final\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{p}}\,({\it{initial\/}}, {\it{stmt-time\/}})\index{p} $=$ {\it{final\/}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  begin-when-normal-clock \\ \index{begin-when-normal-clock}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{begin-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{r-cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\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{begin-body}}\,({\it{stmt\/}})\index{begin-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{begin-body}}\,({\it{stmt\/}})\index{begin-body}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}} $-\;1$, {\it{sizes\/}})\index{mg-meaning-r})\index{cc} \\ 
$\in$$\;\;\;\;${\rm{when-labels}}\,({\it{stmt\/}})\index{when-labels})\- \\ 
$\wedge$$\;\;\;\;${\rm{normal}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{when-handler}}\,({\it{stmt\/}})\index{when-handler}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{set-condition}}\,(\=\+{\rm{mg-meaning-r}}\,(\=\+{\rm{begin-body}}\,({\it{stmt\/}})\index{begin-body}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{sizes\/}})\-\index{mg-meaning-r}, \\ 
{\tt{'}}{\tt{normal}})\-\index{set-condition}, \\ 
{\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{begin-body}}\,({\it{stmt\/}})\index{begin-body}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}} $-\;1$)\index{clock} \\ 
$+$$\;\;\;\;${\tt{3}} \\ 
$+$$\;\;\;\;${\rm{clock}}\,(\=\+{\rm{when-handler}}\,({\it{stmt\/}})\index{when-handler}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{set-condition}}\,(\=\+{\rm{mg-meaning-r}}\,(\=\+{\rm{begin-body}}\,({\it{stmt\/}})\index{begin-body}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{sizes\/}})\-\index{mg-meaning-r}, \\ 
{\tt{'}}{\tt{normal}})\-\index{set-condition}, \\ 
{\it{n\/}} $-\;1$)\-\index{clock})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  begin-when-nonnormal-exact-time-schema \\ \index{begin-when-nonnormal-exact-time!-schema}
\=\+(\=\+({\it{stmt-time\/}} $=$ ({\it{body-time\/}} $+$ ({\tt{2}} $+$ {\it{when-arm-time\/}}))) \\ 
$\wedge$$\;\;\;\;$({\rm{p}}\,({\it{initial\/}}, {\it{body-time\/}})\index{p} $=$ {\it{state2\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{p}}\,({\it{state2\/}}, {\tt{2}})\index{p} $=$ {\it{state3\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{p}}\,({\it{state3\/}}, {\it{when-arm-time\/}})\index{p} $=$ {\it{state4\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{state4\/}} $=$ {\it{final\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{p}}\,({\it{initial\/}}, {\it{stmt-time\/}})\index{p} $=$ {\it{final\/}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  begin-when-nonnormal-clock \\ \index{begin-when-nonnormal-clock}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{begin-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{r-cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\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{begin-body}}\,({\it{stmt\/}})\index{begin-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{begin-body}}\,({\it{stmt\/}})\index{begin-body}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}} $-\;1$, {\it{sizes\/}})\index{mg-meaning-r})\index{cc} \\ 
$\in$$\;\;\;\;${\rm{when-labels}}\,({\it{stmt\/}})\index{when-labels})\- \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{normal}}\,({\rm{mg-meaning-r}}\,(\=\+{\rm{when-handler}}\,({\it{stmt\/}})\index{when-handler}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{set-condition}}\,(\=\+{\rm{mg-meaning-r}}\,(\=\+{\rm{begin-body}}\,({\it{stmt\/}})\index{begin-body}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{sizes\/}})\-\index{mg-meaning-r}, \\ 
{\tt{'}}{\tt{normal}})\-\index{set-condition}, \\ 
{\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{begin-body}}\,({\it{stmt\/}})\index{begin-body}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}} $-\;1$)\index{clock} \\ 
$+$$\;\;\;\;${\tt{2}} \\ 
$+$$\;\;\;\;${\rm{clock}}\,(\=\+{\rm{when-handler}}\,({\it{stmt\/}})\index{when-handler}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{set-condition}}\,(\=\+{\rm{mg-meaning-r}}\,(\=\+{\rm{begin-body}}\,({\it{stmt\/}})\index{begin-body}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{sizes\/}})\-\index{mg-meaning-r}, \\ 
{\tt{'}}{\tt{normal}})\-\index{set-condition}, \\ 
{\it{n\/}} $-\;1$)\-\index{clock})\-)\-\-
\end{tabbing}

%\item 
\begin{verbatim}


(prove-lemma begin-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) 'BEGIN-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 (BEGIN-BODY STMT)
			       (APPEND (WHEN-LABELS STMT)
				       R-COND-LIST)
			       NAME-ALIST PROC-LIST)
	      (OK-MG-DEF-PLISTP PROC-LIST)
	      (OK-TRANSLATION-PARAMETERS
	       (MAKE-CINFO (CODE CINFO)
			   (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
						     (LABEL-CNT CINFO))
				   (LABEL-ALIST CINFO))
			   (ADD1 (ADD1 (LABEL-CNT CINFO))))
	       T-COND-LIST
	       (BEGIN-BODY STMT)
	       PROC-LIST
	       (CONS
		(LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
		(CONS
		 (CONS 'DL
		       (CONS (LABEL-CNT CINFO)
			     '(NIL (PUSH-CONSTANT (NAT 2)))))
		 (CONS
		  '(POP-GLOBAL C-C)
		  (APPEND
		   (CODE
		    (TRANSLATE
		     (NULLIFY
		      (SET-LABEL-ALIST
		       (TRANSLATE
			(MAKE-CINFO (CODE CINFO)
				    (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
							      (LABEL-CNT CINFO))
					    (LABEL-ALIST CINFO))
				    (ADD1 (ADD1 (LABEL-CNT CINFO))))
			T-COND-LIST
			(BEGIN-BODY STMT)
			PROC-LIST)
		       (LABEL-ALIST CINFO)))
		     T-COND-LIST
		     (WHEN-HANDLER STMT)
		     PROC-LIST))
		   (CONS (CONS 'DL
			       (CONS (ADD1 (LABEL-CNT CINFO))
				     '(NIL (NO-OP))))
			 CODE2))))))
	      (OK-MG-STATEP MG-STATE
			    (APPEND (WHEN-LABELS STMT)
				    R-COND-LIST))
	      (COND-SUBSETP (APPEND (WHEN-LABELS STMT)
				    R-COND-LIST)
			    T-COND-LIST)
	      (EQUAL
	       (CODE (TRANSLATE-DEF-BODY (ASSOC SUBR PROC-LIST)
					 PROC-LIST))
	       (APPEND
		(CODE (TRANSLATE (MAKE-CINFO (CODE CINFO)
					     (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
								       (LABEL-CNT CINFO))
						     (LABEL-ALIST CINFO))
					     (ADD1 (ADD1 (LABEL-CNT CINFO))))
				 T-COND-LIST
				 (BEGIN-BODY STMT)
				 PROC-LIST))
		(CONS
		 (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
		 (CONS
		  (CONS 'DL
			(CONS (LABEL-CNT CINFO)
			      '(NIL (PUSH-CONSTANT (NAT 2)))))
		  (CONS
		   '(POP-GLOBAL C-C)
		   (APPEND
		    (CODE
		     (TRANSLATE
		      (NULLIFY
		       (SET-LABEL-ALIST
			(TRANSLATE
			 (MAKE-CINFO (CODE CINFO)
				     (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
							       (LABEL-CNT CINFO))
					     (LABEL-ALIST CINFO))
				     (ADD1 (ADD1 (LABEL-CNT CINFO))))
			 T-COND-LIST
			 (BEGIN-BODY STMT)
			 PROC-LIST)
			(LABEL-ALIST CINFO)))
		      T-COND-LIST
		      (WHEN-HANDLER STMT)
		      PROC-LIST))
		    (CONS (CONS 'DL
				(CONS (ADD1 (LABEL-CNT CINFO))
				      '(NIL (NO-OP))))
			  CODE2)))))))
	      (USER-DEFINED-PROCP SUBR PROC-LIST)
	      (PLISTP TEMP-STK)
	      (LISTP CTRL-STK)
	      (MG-VARS-LIST-OK-IN-P-STATE (MG-ALIST MG-STATE)
					  (BINDINGS (TOP CTRL-STK))
					  TEMP-STK)
	      (NO-P-ALIASING (BINDINGS (TOP CTRL-STK))
			     (MG-ALIST MG-STATE))
	      (SIGNATURES-MATCH (MG-ALIST MG-STATE)
				NAME-ALIST)
	      (NORMAL MG-STATE)
	      (ALL-CARS-UNIQUE (MG-ALIST MG-STATE))
	      (NOT (RESOURCE-ERRORP (MG-MEANING-R (BEGIN-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 (CODE CINFO)
							      (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
											(LABEL-CNT CINFO))
								      (LABEL-ALIST CINFO))
							      (ADD1 (ADD1 (LABEL-CNT CINFO))))))))
			 T-COND-LIST)
	       (CLOCK (BEGIN-BODY STMT) PROC-LIST MG-STATE (SUB1 N)))       ;; body-time
	      (P-STATE                                                      ;; state2
	       (TAG 'PC
		    (CONS SUBR
			  (IF
			   (NORMAL (MG-MEANING-R (BEGIN-BODY STMT)
						 PROC-LIST MG-STATE
						 (SUB1 N)
						 (LIST (LENGTH TEMP-STK)
						       (P-CTRL-STK-SIZE CTRL-STK))))
			   (LENGTH
			    (CODE
			     (TRANSLATE (MAKE-CINFO (CODE CINFO)
						    (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
									      (LABEL-CNT CINFO))
							    (LABEL-ALIST CINFO))
						    (ADD1 (ADD1 (LABEL-CNT CINFO))))
					T-COND-LIST
					(BEGIN-BODY STMT)
					PROC-LIST)))
			   (FIND-LABEL
			    (FETCH-LABEL
			     (CC (MG-MEANING-R (BEGIN-BODY STMT)
					       PROC-LIST MG-STATE
					       (SUB1 N)
					       (LIST (LENGTH TEMP-STK)
						     (P-CTRL-STK-SIZE CTRL-STK))))
			     (LABEL-ALIST
			      (TRANSLATE (MAKE-CINFO (CODE CINFO)
						     (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
									       (LABEL-CNT CINFO))
							     (LABEL-ALIST CINFO))
						     (ADD1 (ADD1 (LABEL-CNT CINFO))))
					 T-COND-LIST
					 (BEGIN-BODY STMT)
					 PROC-LIST)))
			    (APPEND
			     (CODE
			      (TRANSLATE (MAKE-CINFO (CODE CINFO)
						     (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
									       (LABEL-CNT CINFO))
							     (LABEL-ALIST CINFO))
						     (ADD1 (ADD1 (LABEL-CNT CINFO))))
					 T-COND-LIST
					 (BEGIN-BODY STMT)
					 PROC-LIST))
			     (CONS
			      (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
			      (CONS
			       (CONS 'DL
				     (CONS (LABEL-CNT CINFO)
					   '(NIL (PUSH-CONSTANT (NAT 2)))))
			       (CONS
				'(POP-GLOBAL C-C)
				(APPEND
				 (CODE
				  (TRANSLATE
				   (NULLIFY
				    (SET-LABEL-ALIST
				     (TRANSLATE
				      (MAKE-CINFO (CODE CINFO)
						  (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
									    (LABEL-CNT CINFO))
							  (LABEL-ALIST CINFO))
						  (ADD1 (ADD1 (LABEL-CNT CINFO))))
				      T-COND-LIST
				      (BEGIN-BODY STMT)
				      PROC-LIST)
				     (LABEL-ALIST CINFO)))
				   T-COND-LIST
				   (WHEN-HANDLER STMT)
				   PROC-LIST))
				 (CONS (CONS 'DL
					     (CONS (ADD1 (LABEL-CNT CINFO))
						   '(NIL (NO-OP))))
				       CODE2))))))))))
	       CTRL-STK
	       (MAP-DOWN-VALUES
		(MG-ALIST (MG-MEANING-R (BEGIN-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 (BEGIN-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 (WHEN-HANDLER STMT)
			       R-COND-LIST NAME-ALIST PROC-LIST)
	      (OK-MG-DEF-PLISTP PROC-LIST)
	      (OK-TRANSLATION-PARAMETERS
	       (ADD-CODE
		(SET-LABEL-ALIST
		 (TRANSLATE (MAKE-CINFO (CODE CINFO)
					(APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
								  (LABEL-CNT CINFO))
						(LABEL-ALIST CINFO))
					(ADD1 (ADD1 (LABEL-CNT CINFO))))
			    T-COND-LIST
			    (BEGIN-BODY STMT)
			    PROC-LIST)
		 (LABEL-ALIST CINFO))
		(CONS (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
		      (CONS (CONS 'DL
				  (CONS (LABEL-CNT CINFO)
					'(NIL (PUSH-CONSTANT (NAT 2)))))
			    '((POP-GLOBAL C-C)))))
	       T-COND-LIST
	       (WHEN-HANDLER STMT)
	       PROC-LIST
	       (CONS (CONS 'DL
			   (CONS (ADD1 (LABEL-CNT CINFO))
				 '(NIL (NO-OP))))
		     CODE2))
	      (OK-MG-STATEP
	       (SET-CONDITION (MG-MEANING-R (BEGIN-BODY STMT)
					    PROC-LIST MG-STATE
					    (SUB1 N)
					    (LIST (LENGTH TEMP-STK)
						  (P-CTRL-STK-SIZE CTRL-STK)))
			      'NORMAL)
	       R-COND-LIST)
	      (COND-SUBSETP R-COND-LIST T-COND-LIST)
	      (EQUAL
	       (CODE (TRANSLATE-DEF-BODY (ASSOC SUBR PROC-LIST)
					 PROC-LIST))
	       (APPEND
		(CODE
		 (TRANSLATE
		  (ADD-CODE
		   (SET-LABEL-ALIST
		    (TRANSLATE (MAKE-CINFO (CODE CINFO)
					   (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
								     (LABEL-CNT CINFO))
						   (LABEL-ALIST CINFO))
					   (ADD1 (ADD1 (LABEL-CNT CINFO))))
			       T-COND-LIST
			       (BEGIN-BODY STMT)
			       PROC-LIST)
		    (LABEL-ALIST CINFO))
		   (CONS (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
			 (CONS (CONS 'DL
				     (CONS (LABEL-CNT CINFO)
					   '(NIL (PUSH-CONSTANT (NAT 2)))))
			       '((POP-GLOBAL C-C)))))
		  T-COND-LIST
		  (WHEN-HANDLER STMT)
		  PROC-LIST))
		(CONS (CONS 'DL
			    (CONS (ADD1 (LABEL-CNT CINFO))
				  '(NIL (NO-OP))))
		      CODE2)))
	      (USER-DEFINED-PROCP SUBR PROC-LIST)
	      (PLISTP TEMP-STK)
	      (LISTP CTRL-STK)
	      (MG-VARS-LIST-OK-IN-P-STATE
	       (MG-ALIST (SET-CONDITION (MG-MEANING-R (BEGIN-BODY STMT)
						      PROC-LIST MG-STATE
						      (SUB1 N)
						      (LIST (LENGTH TEMP-STK)
							    (P-CTRL-STK-SIZE CTRL-STK)))
					'NORMAL))
	       (BINDINGS (TOP CTRL-STK))
	       TEMP-STK)
	      (NO-P-ALIASING
	       (BINDINGS (TOP CTRL-STK))
	       (MG-ALIST (SET-CONDITION (MG-MEANING-R (BEGIN-BODY STMT)
						      PROC-LIST MG-STATE
						      (SUB1 N)
						      (LIST (LENGTH TEMP-STK)
							    (P-CTRL-STK-SIZE CTRL-STK)))
					'NORMAL)))
	      (SIGNATURES-MATCH
	       (MG-ALIST (SET-CONDITION (MG-MEANING-R (BEGIN-BODY STMT)
						      PROC-LIST MG-STATE
						      (SUB1 N)
						      (LIST (LENGTH TEMP-STK)
							    (P-CTRL-STK-SIZE CTRL-STK)))
					'NORMAL))
	       NAME-ALIST)
	      (NORMAL (SET-CONDITION (MG-MEANING-R (BEGIN-BODY STMT)
						   PROC-LIST MG-STATE
						   (SUB1 N)
						   (LIST (LENGTH TEMP-STK)
							 (P-CTRL-STK-SIZE CTRL-STK)))
				     'NORMAL))
	      (ALL-CARS-UNIQUE
	       (MG-ALIST (SET-CONDITION (MG-MEANING-R (BEGIN-BODY STMT)
						      PROC-LIST MG-STATE
						      (SUB1 N)
						      (LIST (LENGTH TEMP-STK)
							    (P-CTRL-STK-SIZE CTRL-STK)))
					'NORMAL)))
	      (NOT
	       (RESOURCE-ERRORP
		(MG-MEANING-R
		 (WHEN-HANDLER STMT)
		 PROC-LIST
		 (SET-CONDITION (MG-MEANING-R (BEGIN-BODY STMT)
					      PROC-LIST MG-STATE
					      (SUB1 N)
					      (LIST (LENGTH TEMP-STK)
						    (P-CTRL-STK-SIZE CTRL-STK)))
				'NORMAL)
		 (SUB1 N)
		 (LIST (LENGTH TEMP-STK)
		       (P-CTRL-STK-SIZE CTRL-STK))))))
	     (EQUAL
	      (P
	       (MAP-DOWN                                               ;; state3
		(SET-CONDITION (MG-MEANING-R (BEGIN-BODY STMT)
					     PROC-LIST MG-STATE
					     (SUB1 N)
					     (LIST (LENGTH TEMP-STK)
						   (P-CTRL-STK-SIZE CTRL-STK)))
			       'NORMAL)
		PROC-LIST CTRL-STK TEMP-STK
		(TAG 'PC
		     (CONS SUBR
			   (LENGTH
			    (CODE
			     (ADD-CODE
			      (SET-LABEL-ALIST
			       (TRANSLATE (MAKE-CINFO (CODE CINFO)
						      (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
										(LABEL-CNT CINFO))
							      (LABEL-ALIST CINFO))
						      (ADD1 (ADD1 (LABEL-CNT CINFO))))
					  T-COND-LIST
					  (BEGIN-BODY STMT)
					  PROC-LIST)
			       (LABEL-ALIST CINFO))
			      (CONS (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
				    (CONS (CONS 'DL
						(CONS (LABEL-CNT CINFO)
						      '(NIL (PUSH-CONSTANT (NAT 2)))))
					  '((POP-GLOBAL C-C)))))))))
		T-COND-LIST)
	       (CLOCK (WHEN-HANDLER STMT)                                 ;; when-arm-time
		      PROC-LIST
		      (SET-CONDITION (MG-MEANING-R (BEGIN-BODY STMT)
						   PROC-LIST MG-STATE
						   (SUB1 N)
						   (LIST (LENGTH TEMP-STK)
							 (P-CTRL-STK-SIZE CTRL-STK)))
				     'NORMAL)
		      (SUB1 N)))
	      (P-STATE                                                    ;; state4
	       (TAG 'PC
		    (CONS SUBR
			  (IF
			   (NORMAL
			    (MG-MEANING-R
			     (WHEN-HANDLER STMT)
			     PROC-LIST
			     (SET-CONDITION (MG-MEANING-R (BEGIN-BODY STMT)
							  PROC-LIST MG-STATE
							  (SUB1 N)
							  (LIST (LENGTH TEMP-STK)
								(P-CTRL-STK-SIZE CTRL-STK)))
					    'NORMAL)
			     (SUB1 N)
			     (LIST (LENGTH TEMP-STK)
				   (P-CTRL-STK-SIZE CTRL-STK))))
			   (LENGTH
			    (CODE
			     (TRANSLATE
			      (ADD-CODE
			       (SET-LABEL-ALIST
				(TRANSLATE
				 (MAKE-CINFO (CODE CINFO)
					     (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
								       (LABEL-CNT CINFO))
						     (LABEL-ALIST CINFO))
					     (ADD1 (ADD1 (LABEL-CNT CINFO))))
				 T-COND-LIST
				 (BEGIN-BODY STMT)
				 PROC-LIST)
				(LABEL-ALIST CINFO))
			       (CONS (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
				     (CONS (CONS 'DL
						 (CONS (LABEL-CNT CINFO)
						       '(NIL (PUSH-CONSTANT (NAT 2)))))
					   '((POP-GLOBAL C-C)))))
			      T-COND-LIST
			      (WHEN-HANDLER STMT)
			      PROC-LIST)))
			   (FIND-LABEL
			    (FETCH-LABEL
			     (CC
			      (MG-MEANING-R
			       (WHEN-HANDLER STMT)
			       PROC-LIST
			       (SET-CONDITION (MG-MEANING-R (BEGIN-BODY STMT)
							    PROC-LIST MG-STATE
							    (SUB1 N)
							    (LIST (LENGTH TEMP-STK)
								  (P-CTRL-STK-SIZE CTRL-STK)))
					      'NORMAL)
			       (SUB1 N)
			       (LIST (LENGTH TEMP-STK)
				     (P-CTRL-STK-SIZE CTRL-STK))))
			     (LABEL-ALIST
			      (TRANSLATE
			       (ADD-CODE
				(SET-LABEL-ALIST
				 (TRANSLATE
				  (MAKE-CINFO (CODE CINFO)
					      (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
									(LABEL-CNT CINFO))
						      (LABEL-ALIST CINFO))
					      (ADD1 (ADD1 (LABEL-CNT CINFO))))
				  T-COND-LIST
				  (BEGIN-BODY STMT)
				  PROC-LIST)
				 (LABEL-ALIST CINFO))
				(CONS (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
				      (CONS (CONS 'DL
						  (CONS (LABEL-CNT CINFO)
							'(NIL (PUSH-CONSTANT (NAT 2)))))
					    '((POP-GLOBAL C-C)))))
			       T-COND-LIST
			       (WHEN-HANDLER STMT)
			       PROC-LIST)))
			    (APPEND
			     (CODE
			      (TRANSLATE
			       (ADD-CODE
				(SET-LABEL-ALIST
				 (TRANSLATE
				  (MAKE-CINFO (CODE CINFO)
					      (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
									(LABEL-CNT CINFO))
						      (LABEL-ALIST CINFO))
					      (ADD1 (ADD1 (LABEL-CNT CINFO))))
				  T-COND-LIST
				  (BEGIN-BODY STMT)
				  PROC-LIST)
				 (LABEL-ALIST CINFO))
				(CONS (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
				      (CONS (CONS 'DL
						  (CONS (LABEL-CNT CINFO)
							'(NIL (PUSH-CONSTANT (NAT 2)))))
					    '((POP-GLOBAL C-C)))))
			       T-COND-LIST
			       (WHEN-HANDLER STMT)
			       PROC-LIST))
			     (CONS (CONS 'DL
					 (CONS (ADD1 (LABEL-CNT CINFO))
					       '(NIL (NO-OP))))
				   CODE2))))))
	       CTRL-STK
	       (MAP-DOWN-VALUES
		(MG-ALIST
		 (MG-MEANING-R
		  (WHEN-HANDLER STMT)
		  PROC-LIST
		  (SET-CONDITION (MG-MEANING-R (BEGIN-BODY STMT)
					       PROC-LIST MG-STATE
					       (SUB1 N)
					       (LIST (LENGTH TEMP-STK)
						     (P-CTRL-STK-SIZE CTRL-STK)))
				 'NORMAL)
		  (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
			 (WHEN-HANDLER STMT)
			 PROC-LIST
			 (SET-CONDITION (MG-MEANING-R (BEGIN-BODY STMT)
						      PROC-LIST MG-STATE
						      (SUB1 N)
						      (LIST (LENGTH TEMP-STK)
							    (P-CTRL-STK-SIZE CTRL-STK)))
					'NORMAL)
			 (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 PROMOTE
   (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 @BODY-TIME
                     (CLOCK (BEGIN-BODY STMT)
                            PROC-LIST MG-STATE
                            (SUB1 N)))
   (ADD-ABBREVIATION @STATE2
    (P-STATE
     (TAG 'PC
      (CONS SUBR
       (IF
        (NORMAL (MG-MEANING-R (BEGIN-BODY STMT)
                              PROC-LIST MG-STATE
                              (SUB1 N)
                              (LIST (LENGTH TEMP-STK)
                                    (P-CTRL-STK-SIZE CTRL-STK))))
        (LENGTH
         (CODE
            (TRANSLATE (MAKE-CINFO (CODE CINFO)
                                   (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
                                                             (LABEL-CNT CINFO))
                                           (LABEL-ALIST CINFO))
                                   (ADD1 (ADD1 (LABEL-CNT CINFO))))
                       T-COND-LIST
                       (BEGIN-BODY STMT)
                       PROC-LIST)))
        (FIND-LABEL
         (FETCH-LABEL
          (CC (MG-MEANING-R (BEGIN-BODY STMT)
                            PROC-LIST MG-STATE
                            (SUB1 N)
                            (LIST (LENGTH TEMP-STK)
                                  (P-CTRL-STK-SIZE CTRL-STK))))
          (LABEL-ALIST
            (TRANSLATE (MAKE-CINFO (CODE CINFO)
                                   (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
                                                             (LABEL-CNT CINFO))
                                           (LABEL-ALIST CINFO))
                                   (ADD1 (ADD1 (LABEL-CNT CINFO))))
                       T-COND-LIST
                       (BEGIN-BODY STMT)
                       PROC-LIST)))
         (APPEND
          (CODE
            (TRANSLATE (MAKE-CINFO (CODE CINFO)
                                   (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
                                                             (LABEL-CNT CINFO))
                                           (LABEL-ALIST CINFO))
                                   (ADD1 (ADD1 (LABEL-CNT CINFO))))
                       T-COND-LIST
                       (BEGIN-BODY STMT)
                       PROC-LIST))
          (CONS
           (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
           (CONS
            (CONS 'DL
                  (CONS (LABEL-CNT CINFO)
                        '(NIL (PUSH-CONSTANT (NAT 2)))))
            (CONS
             '(POP-GLOBAL C-C)
             (APPEND
              (CODE
               (TRANSLATE
                (NULLIFY
                 (SET-LABEL-ALIST
                  (TRANSLATE
                       (MAKE-CINFO (CODE CINFO)
                                   (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
                                                             (LABEL-CNT CINFO))
                                           (LABEL-ALIST CINFO))
                                   (ADD1 (ADD1 (LABEL-CNT CINFO))))
                       T-COND-LIST
                       (BEGIN-BODY STMT)
                       PROC-LIST)
                  (LABEL-ALIST CINFO)))
                T-COND-LIST
                (WHEN-HANDLER STMT)
                PROC-LIST))
              (CONS (CONS 'DL
                          (CONS (ADD1 (LABEL-CNT CINFO))
                                '(NIL (NO-OP))))
                    CODE2))))))))))
     CTRL-STK
     (MAP-DOWN-VALUES
                    (MG-ALIST (MG-MEANING-R (BEGIN-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 (BEGIN-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
     (SET-CONDITION (MG-MEANING-R (BEGIN-BODY STMT)
                                  PROC-LIST MG-STATE
                                  (SUB1 N)
                                  (LIST (LENGTH TEMP-STK)
                                        (P-CTRL-STK-SIZE CTRL-STK)))
                    'NORMAL)
     PROC-LIST CTRL-STK TEMP-STK
     (TAG 'PC
      (CONS SUBR
       (LENGTH
        (CODE
         (ADD-CODE
          (SET-LABEL-ALIST
            (TRANSLATE (MAKE-CINFO (CODE CINFO)
                                   (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
                                                             (LABEL-CNT CINFO))
                                           (LABEL-ALIST CINFO))
                                   (ADD1 (ADD1 (LABEL-CNT CINFO))))
                       T-COND-LIST
                       (BEGIN-BODY STMT)
                       PROC-LIST)
            (LABEL-ALIST CINFO))
          (CONS (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
                (CONS (CONS 'DL
                            (CONS (LABEL-CNT CINFO)
                                  '(NIL (PUSH-CONSTANT (NAT 2)))))
                      '((POP-GLOBAL C-C)))))))))
     T-COND-LIST))
   (ADD-ABBREVIATION @WHEN-ARM-TIME
         (CLOCK (WHEN-HANDLER STMT)
                PROC-LIST
                (SET-CONDITION (MG-MEANING-R (BEGIN-BODY STMT)
                                             PROC-LIST MG-STATE
                                             (SUB1 N)
                                             (LIST (LENGTH TEMP-STK)
                                                   (P-CTRL-STK-SIZE CTRL-STK)))
                               'NORMAL)
                (SUB1 N)))
   (ADD-ABBREVIATION @STATE4
    (P-STATE
     (TAG 'PC
      (CONS SUBR
       (IF
        (NORMAL
         (MG-MEANING-R
                (WHEN-HANDLER STMT)
                PROC-LIST
                (SET-CONDITION (MG-MEANING-R (BEGIN-BODY STMT)
                                             PROC-LIST MG-STATE
                                             (SUB1 N)
                                             (LIST (LENGTH TEMP-STK)
                                                   (P-CTRL-STK-SIZE CTRL-STK)))
                               'NORMAL)
                (SUB1 N)
                (LIST (LENGTH TEMP-STK)
                      (P-CTRL-STK-SIZE CTRL-STK))))
        (LENGTH
         (CODE
          (TRANSLATE
           (ADD-CODE
            (SET-LABEL-ALIST
             (TRANSLATE
                       (MAKE-CINFO (CODE CINFO)
                                   (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
                                                             (LABEL-CNT CINFO))
                                           (LABEL-ALIST CINFO))
                                   (ADD1 (ADD1 (LABEL-CNT CINFO))))
                       T-COND-LIST
                       (BEGIN-BODY STMT)
                       PROC-LIST)
             (LABEL-ALIST CINFO))
            (CONS (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
                  (CONS (CONS 'DL
                              (CONS (LABEL-CNT CINFO)
                                    '(NIL (PUSH-CONSTANT (NAT 2)))))
                        '((POP-GLOBAL C-C)))))
           T-COND-LIST
           (WHEN-HANDLER STMT)
           PROC-LIST)))
        (FIND-LABEL
         (FETCH-LABEL
          (CC
           (MG-MEANING-R
                (WHEN-HANDLER STMT)
                PROC-LIST
                (SET-CONDITION (MG-MEANING-R (BEGIN-BODY STMT)
                                             PROC-LIST MG-STATE
                                             (SUB1 N)
                                             (LIST (LENGTH TEMP-STK)
                                                   (P-CTRL-STK-SIZE CTRL-STK)))
                               'NORMAL)
                (SUB1 N)
                (LIST (LENGTH TEMP-STK)
                      (P-CTRL-STK-SIZE CTRL-STK))))
          (LABEL-ALIST
           (TRANSLATE
            (ADD-CODE
             (SET-LABEL-ALIST
              (TRANSLATE
                       (MAKE-CINFO (CODE CINFO)
                                   (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
                                                             (LABEL-CNT CINFO))
                                           (LABEL-ALIST CINFO))
                                   (ADD1 (ADD1 (LABEL-CNT CINFO))))
                       T-COND-LIST
                       (BEGIN-BODY STMT)
                       PROC-LIST)
              (LABEL-ALIST CINFO))
             (CONS (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
                   (CONS (CONS 'DL
                               (CONS (LABEL-CNT CINFO)
                                     '(NIL (PUSH-CONSTANT (NAT 2)))))
                         '((POP-GLOBAL C-C)))))
            T-COND-LIST
            (WHEN-HANDLER STMT)
            PROC-LIST)))
         (APPEND
          (CODE
           (TRANSLATE
            (ADD-CODE
             (SET-LABEL-ALIST
              (TRANSLATE
                       (MAKE-CINFO (CODE CINFO)
                                   (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
                                                             (LABEL-CNT CINFO))
                                           (LABEL-ALIST CINFO))
                                   (ADD1 (ADD1 (LABEL-CNT CINFO))))
                       T-COND-LIST
                       (BEGIN-BODY STMT)
                       PROC-LIST)
              (LABEL-ALIST CINFO))
             (CONS (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
                   (CONS (CONS 'DL
                               (CONS (LABEL-CNT CINFO)
                                     '(NIL (PUSH-CONSTANT (NAT 2)))))
                         '((POP-GLOBAL C-C)))))
            T-COND-LIST
            (WHEN-HANDLER STMT)
            PROC-LIST))
          (CONS (CONS 'DL
                      (CONS (ADD1 (LABEL-CNT CINFO))
                            '(NIL (NO-OP))))
                CODE2))))))
     CTRL-STK
     (MAP-DOWN-VALUES
      (MG-ALIST
       (MG-MEANING-R
                (WHEN-HANDLER STMT)
                PROC-LIST
                (SET-CONDITION (MG-MEANING-R (BEGIN-BODY STMT)
                                             PROC-LIST MG-STATE
                                             (SUB1 N)
                                             (LIST (LENGTH TEMP-STK)
                                                   (P-CTRL-STK-SIZE CTRL-STK)))
                               'NORMAL)
                (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
                (WHEN-HANDLER STMT)
                PROC-LIST
                (SET-CONDITION (MG-MEANING-R (BEGIN-BODY STMT)
                                             PROC-LIST MG-STATE
                                             (SUB1 N)
                                             (LIST (LENGTH TEMP-STK)
                                                   (P-CTRL-STK-SIZE CTRL-STK)))
                               'NORMAL)
                (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))
   (DEMOTE 19)
   (DIVE 1 1)
   PUSH UP
   (DIVE 2 1)
   (DIVE 1 5 2 2 1)
   S TOP PROMOTE
   (CLAIM (NORMAL (MG-MEANING-R (BEGIN-BODY STMT)
                                PROC-LIST MG-STATE
                                (SUB1 N)
                                (LIST (LENGTH TEMP-STK)
                                      (P-CTRL-STK-SIZE CTRL-STK))))
          0)
   (DROP 19)
   (CLAIM (EQUAL @STMT-TIME (PLUS 2 @BODY-TIME))
          0)
   (CLAIM (EQUAL (P @STATE2 2) @FINAL) 0)
   (DEMOTE 19 21 22)
   (GENERALIZE ((@STATE4 STATE4)
                (@WHEN-ARM-TIME WHEN-ARM-TIME)
                (@STATE3 STATE3)
                (@STATE2 STATE2)
                (@BODY-TIME BODY-TIME)
                (@FINAL FINAL)
                (@STMT-TIME STMT-TIME)
                (@INITIAL INITIAL)))
   DROP
   (USE-LEMMA BEGIN-BODY-NORMAL-EXACT-TIME-SCHEMA)
   PROVE
   (CONTRADICT 22)
   (DROP 19 21 22)
   (DIVE 1)
   (REWRITE P-ADD1-3)
   (REWRITE P-ADD1-3)
   (DIVE 1)
   (DIVE 1)
   (REWRITE BEGIN-STATE2-NORMAL-BODY-STEP1)
   UP
   (REWRITE BEGIN-STATE2-NORMAL-BODY-STEP2-EQUALS-FINAL)
   UP
   (REWRITE P-0-UNWINDING-LEMMA)
   TOP S-PROP
   (CONTRADICT 21)
   (DIVE 1)
   (REWRITE BEGIN-BODY-NORMAL-CLOCK)
   TOP S
   (CLAIM (NOT (MEMBER (CC (MG-MEANING-R (BEGIN-BODY STMT)
                                         PROC-LIST MG-STATE
                                         (SUB1 N)
                                         (LIST (LENGTH TEMP-STK)
                                               (P-CTRL-STK-SIZE CTRL-STK))))
                       (WHEN-LABELS STMT)))
          0)
   (DROP 19)
   (CLAIM (EQUAL @STMT-TIME @BODY-TIME)
          0)
   (CLAIM (EQUAL @STATE2 @FINAL) 0)
   (DEMOTE 19 22 23)
   (GENERALIZE ((@STATE4 STATE4)
                (@WHEN-ARM-TIME WHEN-ARM-TIME)
                (@STATE3 STATE3)
                (@STATE2 STATE2)
                (@BODY-TIME BODY-TIME)
                (@FINAL FINAL)
                (@STMT-TIME STMT-TIME)
                (@INITIAL INITIAL)))
   DROP
   (USE-LEMMA BEGIN-BODY-NONNORMAL-NONWHEN-EXACT-TIME-SCHEMA)
   PROVE
   (CONTRADICT 23)
   (DROP 19 22 23)
   (DIVE 1)
   (REWRITE BEGIN-NONNORMAL-NONWHEN-BODY-STATE2-EQUALS-FINAL)
   TOP S-PROP
   (CONTRADICT 22)
   (DIVE 1)
   (REWRITE BEGIN-BODY-NONNORMAL-NONWHEN-CLOCK)
   TOP S
   (DEMOTE 19)
   (DIVE 1 1)
   PUSH TOP PROMOTE
   (CLAIM (EQUAL (P @STATE2 2) @STATE3)
          0)
   (CLAIM
    (NORMAL
     (MG-MEANING-R
                (WHEN-HANDLER STMT)
                PROC-LIST
                (SET-CONDITION (MG-MEANING-R (BEGIN-BODY STMT)
                                             PROC-LIST MG-STATE
                                             (SUB1 N)
                                             (LIST (LENGTH TEMP-STK)
                                                   (P-CTRL-STK-SIZE CTRL-STK)))
                               'NORMAL)
                (SUB1 N)
                (LIST (LENGTH TEMP-STK)
                      (P-CTRL-STK-SIZE CTRL-STK))))
    0)
   (CLAIM (EQUAL @STMT-TIME
                 (PLUS @BODY-TIME 3 @WHEN-ARM-TIME))
          0)
   (CLAIM (EQUAL (P-STEP @STATE4) @FINAL)
          0)
   (DEMOTE 19 22 23 25 26)
   (GENERALIZE ((@STATE4 STATE4)
                (@WHEN-ARM-TIME WHEN-ARM-TIME)
                (@STATE3 STATE3)
                (@STATE2 STATE2)
                (@BODY-TIME BODY-TIME)
                (@FINAL FINAL)
                (@STMT-TIME STMT-TIME)
                (@INITIAL INITIAL)))
   DROP
   (USE-LEMMA BEGIN-WHEN-NORMAL-EXACT-TIME-SCHEMA)
   PROVE
   (CONTRADICT 26)
   (DIVE 1)
   (REWRITE BEGIN-WHEN-NORMAL-STEP-STATE4-EQUALS-FINAL)
   TOP S-PROP
   (CONTRADICT 25)
   (DIVE 1)
   (REWRITE BEGIN-WHEN-NORMAL-CLOCK
            (($SIZES (LIST (LENGTH TEMP-STK)
                           (P-CTRL-STK-SIZE CTRL-STK)))))
   TOP S
   (CLAIM (EQUAL @STMT-TIME
                 (PLUS @BODY-TIME 2 @WHEN-ARM-TIME))
          0)
   (CLAIM (EQUAL @STATE4 @FINAL) 0)
   (DEMOTE 19 22 23 25 26)
   (GENERALIZE ((@STATE4 STATE4)
                (@WHEN-ARM-TIME WHEN-ARM-TIME)
                (@STATE3 STATE3)
                (@STATE2 STATE2)
                (@BODY-TIME BODY-TIME)
                (@FINAL FINAL)
                (@STMT-TIME STMT-TIME)
                (@INITIAL INITIAL)))
   DROP
   (USE-LEMMA BEGIN-WHEN-NONNORMAL-EXACT-TIME-SCHEMA)
   PROVE
   (CONTRADICT 26)
   (DIVE 1)
   (REWRITE BEGIN-WHEN-NONNORMAL-STATE4-EQUALS-FINAL)
   TOP S-PROP
   (CONTRADICT 25)
   (DIVE 1)
   (REWRITE BEGIN-WHEN-NONNORMAL-CLOCK
            (($SIZES (LIST (LENGTH TEMP-STK)
                           (P-CTRL-STK-SIZE CTRL-STK)))))
   TOP S
   (CONTRADICT 23)
   (DIVE 1)
   (REWRITE P-ADD1-3)
   (REWRITE P-ADD1-3)
   (REWRITE P-0-UNWINDING-LEMMA)
   (DIVE 1)
   (REWRITE BEGIN-WHEN-SIGNALLED-STATE2-STEP1)
   UP
   (REWRITE BEGIN-WHEN-SIGNALLED-STATE2-STEP2)
   TOP S-PROP SPLIT
   (REWRITE BEGIN-WHEN-HANDLER-HYPS)
   (REWRITE BEGIN-WHEN-HANDLER-HYPS)
   (REWRITE BEGIN-WHEN-HANDLER-HYPS)
   (DIVE 1)
   (REWRITE BEGIN-WHEN-HANDLER-HYPS)
   TOP S
   (REWRITE BEGIN-WHEN-HANDLER-HYPS)
   (REWRITE BEGIN-WHEN-HANDLER-HYPS)
   (REWRITE BEGIN-WHEN-HANDLER-HYPS)
   (REWRITE BEGIN-WHEN-HANDLER-HYPS)
   (REWRITE BEGIN-WHEN-HANDLER-HYPS)
   (DIVE 1)
   (REWRITE BEGIN-WHEN-HANDLER-HYPS)
   UP S
   (DROP 19)
   SPLIT
   (REWRITE BEGIN-BODY-HYPS)
   (REWRITE BEGIN-BODY-HYPS)
   (REWRITE BEGIN-BODY-HYPS)
   (REWRITE BEGIN-BODY-HYPS)
   (DIVE 1)
   (REWRITE BEGIN-BODY-HYPS)
   TOP S
   (DIVE 1)
   (REWRITE BEGIN-BODY-HYPS)
   TOP S)))
\end{verbatim}




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

\addvspace{18pt}

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