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

\addvspace{18pt}

\begin{verbatim};; I know that in the absence of resource-errors the two MG interpreters
;; and the two clocks are the same.  Therefore, after I have proved everything
;; with the resource-error versions, I automatically gain the non-resource-error
;; versions.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                           ;;
;;                              EXACT TIME LEMMA                             ;;
;;                                                                           ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

\end{verbatim}\begin{tabbing}{\sc Theorem}:  not-resource-errorp-not-zerop-n \\ \index{not-resource-errorp-not-zerop-n}
\=\+(\=\+{\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{r-cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resource-errorp}}\,({\rm{mg-meaning-r}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\it{temp-stk\/}})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{resource-errorp}))\- \\ 
$\rightarrow$$\;\;\;\;$({\it{n\/}} $\not\simeq {\tt{0}}$)\-
\end{tabbing}
      

%\item 
\begin{verbatim}

      

(defn exact-time-induction-hint (cinfo r-cond-list t-cond-list stmt 
					     proc-list mg-state n code2 subr
   	 			             ctrl-stk temp-stk name-alist)
       (if (zerop n)
           t
       (if (resources-inadequatep stmt proc-list 
				  (list (length temp-stk) (p-ctrl-stk-size ctrl-stk)))
	   t
       (if (equal (car stmt) 'no-op-mg)
           t
       (if (equal (car stmt) 'signal-mg)
           t
       (if (equal (car stmt) 'prog2-mg)
           (and (exact-time-induction-hint 
		  cinfo
		  r-cond-list
		  t-cond-list
		  (prog2-left-branch stmt)
		  proc-list
		  mg-state
		  (sub1 n)
		  (append (code (translate (nullify (translate (nullify cinfo)
							       t-cond-list
							       (prog2-left-branch stmt)
							       proc-list))
					   t-cond-list
					   (prog2-right-branch stmt)
					   proc-list))
			  code2)
		  subr ctrl-stk temp-stk name-alist)
                (exact-time-induction-hint 
		  (translate cinfo t-cond-list (prog2-left-branch stmt) proc-list)
                  r-cond-list
		  t-cond-list
		  (prog2-right-branch stmt)
		  proc-list
		  (mg-meaning-r (prog2-left-branch stmt) proc-list mg-state (sub1 n)
				(list (length temp-stk) (p-ctrl-stk-size ctrl-stk)))
		  (sub1 n)
		  code2
		  subr ctrl-stk temp-stk name-alist))
       (if (equal (car stmt) 'loop-mg)
           (and (exact-time-induction-hint 
                   (make-cinfo (append (code cinfo)
				       (list (list 'dl (label-cnt cinfo) nil '(no-op))))
			       (cons (cons 'leave (add1 (label-cnt cinfo)))
				     (label-alist cinfo))
			       (add1 (add1 (label-cnt cinfo))))
                  (cons 'leave r-cond-list) t-cond-list
		  (loop-body stmt)
		  proc-list
		  mg-state
		  (sub1 n)
		  (cons (list 'jump (label-cnt cinfo))
			(cons (list 'dl (add1 (label-cnt cinfo)) nil '(push-constant (nat 2)))
			      (cons '(pop-global c-c)
				    code2)))
		  subr ctrl-stk temp-stk name-alist)
                (exact-time-induction-hint
		  cinfo 
                  (cons 'leave r-cond-list) t-cond-list
		  stmt
		  proc-list
		  (mg-meaning-r (loop-body stmt) proc-list mg-state (sub1 n)
				(list (length temp-stk) (p-ctrl-stk-size ctrl-stk)))
		  (sub1 n)
		  code2
		  subr ctrl-stk temp-stk name-alist))
       (if (equal (car stmt) 'if-mg)
            (and (exact-time-induction-hint
		   (make-cinfo 
		     (append (code cinfo)
			    (list (list 'push-local (if-condition stmt))
				  '(fetch-temp-stk)
                                  (list 'test-bool-and-jump 'false (label-cnt cinfo))))
		     (label-alist cinfo)
		     (add1 (add1 (label-cnt cinfo))))
                   r-cond-list t-cond-list
		   (if-true-branch stmt)
                   proc-list
		   mg-state
		   (sub1 n)
		   (cons (list 'jump (add1 (label-cnt cinfo)))
			 (cons (list 'dl (label-cnt cinfo) nil '(no-op))
			       (append (code (translate 
					       (nullify
						 (translate 
						   (make-cinfo 
						     nil
						     (label-alist cinfo)
						     (add1 (add1 (label-cnt cinfo))))
                                                   t-cond-list
						   (if-true-branch stmt)
						   proc-list))
					       t-cond-list
					       (if-false-branch stmt)
					       proc-list))
				       (cons (list 'dl (add1 (label-cnt cinfo)) nil '(no-op))
					     code2))))
		   subr ctrl-stk temp-stk name-alist)
                (exact-time-induction-hint 
		  (add-code 
		    (translate 
		      (make-cinfo 
			(append (code cinfo)
			    (list (list 'push-local (if-condition stmt))
				  '(fetch-temp-stk)
                                  (list 'test-bool-and-jump 'false (label-cnt cinfo))))
			(label-alist cinfo)
			(add1 (add1 (label-cnt cinfo))))
		      t-cond-list
		      (if-true-branch stmt)
		      proc-list)
		    (list (list 'jump (add1 (label-cnt cinfo)))
			  (list 'dl (label-cnt cinfo) nil '(no-op))))
                  r-cond-list t-cond-list
                  (if-false-branch stmt)
		  proc-list
                  mg-state
                  (sub1 n)
                  (cons (list 'dl (add1 (label-cnt cinfo)) nil '(no-op))
                        code2)
		  subr ctrl-stk temp-stk name-alist))
        (if (equal (car stmt) 'begin-mg)
            (and 
              (exact-time-induction-hint
		(make-cinfo (code cinfo)
			    (append (make-label-alist (when-labels stmt)
						      (label-cnt cinfo))
				    (label-alist cinfo))
			    (add1 (add1 (label-cnt cinfo))))
                (append (when-labels stmt) r-cond-list)
                t-cond-list
		(begin-body stmt)
		proc-list
		mg-state
		(sub1 n)
		(cons (list 'jump (add1 (label-cnt cinfo)))
		      (cons (list 'dl (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 (list 'dl (add1 (label-cnt cinfo)) nil '(no-op))
					  code2)))))
		subr ctrl-stk temp-stk name-alist)
              (exact-time-induction-hint
                 (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))
		  (list (list 'jump (add1 (label-cnt cinfo)))
			(list 'dl (label-cnt cinfo) nil '(push-constant (nat 2)))
			'(pop-global c-c)))
                r-cond-list
		t-cond-list
		(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)
		(cons (list 'dl (add1 (label-cnt cinfo)) nil '(no-op))
					  code2)
                subr ctrl-stk temp-stk name-alist))
       (if (equal (car stmt) 'proc-call-mg)
           (exact-time-induction-hint
   	         (make-cinfo nil
			     (cons (cons 'routineerror 0)
				   (make-label-alist (make-cond-list (fetch-called-def stmt proc-list)) 0))
			     1)
		 (make-cond-list (fetch-called-def stmt proc-list))
		 (make-cond-list (fetch-called-def stmt proc-list))
                 (def-body (fetch-called-def stmt proc-list))
		 proc-list
		 (make-call-environment mg-state stmt (fetch-called-def stmt proc-list))
		 (sub1 n)
		 (cons '(dl 0 nil (no-op))
		       (cons (list 'pop* (data-length (def-locals (fetch-called-def stmt proc-list))))
		             '((ret))))
		 (call-name stmt)
                 (cons (p-frame 
			(make-frame-alist (fetch-called-def stmt proc-list) stmt ctrl-stk temp-stk)
			(tag 'pc (cons subr	
			       (add1 (PLUS (LENGTH (CODE CINFO))
						   (data-length (DEF-LOCALS (FETCH-CALLED-DEF 
									       STMT PROC-LIST)))
						   (length (DEF-LOCALS (FETCH-CALLED-DEF 
									STMT PROC-LIST)))
						   (LENGTH (CALL-ACTUALS STMT)))))))
		       ctrl-stk)
                 (append (reverse (mg-to-p-local-values (def-locals (fetch-called-def stmt proc-list))))
			 (map-down-values (mg-alist mg-state)
					  (bindings (top ctrl-stk))
					  temp-stk))
		 (make-name-alist (fetch-called-def stmt proc-list)))
        (if (equal (car stmt) 'predefined-proc-call-mg)
	    t
 	    f))))))))))
    ((lessp (COUNT n)))
    (INSTRUCTIONS (BASH (ENABLE WHEN-HANDLER BEGIN-BODY IF-TRUE-BRANCH
				IF-FALSE-BRANCH LOOP-BODY PROG2-RIGHT-BRANCH
				PROG2-LEFT-BRANCH))))
\end{verbatim}


\begin{verbatim};;  The cond-list is required in the translation so that 
;;  I can convert between MG and Piton conditions;  in the recognizer it is only 
;;  required that I have some set of conditions which could be signalled.  It had better
;;  be that any signalled are on the translator cond-list or I won't be able to do the
;;  mapping.  However, I can sometimes signal 'leave and 'routineerror even though 
;;  these are not on the translator cond-list.  This is because their map functions are
;;  computed independently of the list.  Therefore the appropriate relation between the 
;;  recognizer-cond-alist and translator-cond-alist is that (cond-subsetp rec-list trans-list).

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


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

\addvspace{18pt}

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


\noindent{\sc Event}:   Disable exact-time-lemma2.

\addvspace{18pt}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                           ;;
;;                         TRANSLATION CORRECTNESS                           ;;
;;                                                                           ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Notice that exact-time-hyps refers to two cond-lists (which are related by
;; the function cond-subsetp) while translation-is-correct only refers to a 
;; single list.  The two lists are necessary in exact-time-hyps to make the 
;; induction work.  The user supplies only a single list with his input statement.
;; That list must be an identifier-plistp and hence may not contain 'leave.
;;

;; The hypotheses of this theorem guarantee the following:
;;    1. mg-state is of the form <alist current-condition>
;;       a. the alist is of the form < <name type value> ... >
;;       b. the condition is 'normal, 'routineerror, 'timed-out, or
;;             is in cond-list
;;    2. proc-list is a syntactically legal list of micro-gypsy procedures (which may
;;             be mutually recursive)
;;    3. stmt is a syntactically legal micro-Gypsy statement with respect to proc-list
;;             with conditions from cond-list and variables from (mg-alist mg-state)
;;    4. the translation environment described by cinfo is legitimate
;;       a.  cinfo is of the form <code label-alist label-cnt cond-list>, where 
;;               cond-list and code are proper lists
;;       b.  cond-list is a proper list containing only legal identifiers, 'leave, or 
;;               'routineerror
;;       c.  translation stmt with cinfo does not generate any labels which would 
;;               duplicate labels in (code cinfo) or code2
;;    5. subr is the name of some procedure in proc-list
;;    6. the body of procedure subr is the context in which stmt "lives"; that is 
;;           the translation of the body of subr is equal to the append of the 
;;           the translation of stmt with code2
;;    7. execution of stmt does not yield the condition timed-out.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  cons-preserves-cond-subsetp \\ \index{cons-preserves-cond-subsetp}
{\rm{cond-subsetp}}\,({\it{y\/}}, {\it{z\/}})\index{cond-subsetp} $\rightarrow$ {\rm{cond-subsetp}}\,({\it{y\/}}, {\rm{cons}}\,({\it{x\/}}, {\it{z\/}}))\index{cond-subsetp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  cond-subsetp-reflexive \\ \index{cond-subsetp-reflexive}
{\rm{ok-cond-list}}\,({\it{cond-list\/}})\index{ok-cond-list} $\rightarrow$ {\rm{cond-subsetp}}\,({\it{cond-list\/}}, {\it{cond-list\/}})\index{cond-subsetp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mg-meaning-preserves-signatures-match3 \\ \index{mg-meaning-preserves-signatures!-match3}
\=\+(\=\+{\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{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-mg-statep}}\,({\it{mg-state\/}}, {\it{cond-list\/}})\index{ok-mg-statep} \\ 
$\wedge$$\;\;\;\;${\rm{signatures-match}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{name-alist\/}})\index{signatures-match})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{signatures-match}}\,(\=\+{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, \\ 
{\rm{mg-alist}}\,({\rm{mg-meaning}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}})\index{mg-meaning})\index{mg-alist})\-\index{signatures-match}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mg-state-decomposition \\ \index{mg-state-decomposition}
\=\+($\neg$ {\rm{resource-errorp}}\,({\it{state\/}})\index{resource-errorp}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{mg-state}}\,({\rm{cc}}\,({\it{state\/}})\index{cc}, {\rm{mg-alist}}\,({\it{state\/}})\index{mg-alist}, {\tt{'}}{\tt{run}})\index{mg-state} $=$ {\it{state\/}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  signatures-match-implies-signatures-equal \\ \index{signatures-match-implies-signat!ures-equal}
\=\+{\rm{signatures-match}}\,({\it{alist1\/}}, {\it{alist2\/}})\index{signatures-match} \\ 
$\rightarrow$$\;\;\;\;$({\rm{signature}}\,({\it{alist1\/}})\index{signature} $=$ {\rm{signature}}\,({\it{alist2\/}})\index{signature})\-
\end{tabbing}


\noindent{\sc Event}:   Disable signatures-match-implies-signatures-equal.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  translation-is-correct2 \\ \index{translation-is-correct2}
\=\+(\=\+{\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{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{cond-list\/}}, {\it{stmt\/}}, {\it{proc-list\/}}, {\it{code2\/}})\index{ok-translation-parameters} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statep}}\,({\it{mg-state\/}}, {\it{cond-list\/}})\index{ok-mg-statep} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{code}}\,({\rm{translate-def-body}}\,({\rm{assoc}}\,({\it{subr\/}}, {\it{proc-list\/}}), {\it{proc-list\/}})\index{translate-def-body})\index{code} \\ 
$=$$\;\;\;\;${\rm{append}}\,({\rm{code}}\,({\rm{translate}}\,({\it{cinfo\/}}, {\it{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{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$$\;\;\;\;$({\it{pc-offset\/}} $=$ {\rm{length}}\,({\rm{code}}\,({\it{cinfo\/}})\index{code})\index{length}) \\ 
$\wedge$$\;\;\;\;$({\rm{cc}}\,({\it{mg-state\/}})\index{cc} $\not=$ {\tt{'}}{\tt{leave}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{map-up}}\,(\=\+{\rm{p}}\,(\=\+{\rm{map-down}}\,(\=\+{\it{mg-state\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{ctrl-stk\/}}, \\ 
{\it{temp-stk\/}}, \\ 
{\rm{tag}}\,({\tt{'}}{\tt{pc}}, {\rm{cons}}\,({\it{subr\/}}, {\it{pc-offset\/}}))\index{tag}, \\ 
{\it{cond-list\/}})\-\index{map-down}, \\ 
{\rm{clock}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}})\index{clock})\-\index{p}, \\ 
{\rm{signature}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{signature}, \\ 
{\it{cond-list\/}})\-\index{map-up} \\ 
$=$$\;\;\;\;${\rm{mg-meaning}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}})\index{mg-meaning})\-\-
\end{tabbing}

\begin{verbatim};; The following few functions are for making the "initial story" about how you invoke the 
;; MG compiler at the highest level.  That is, we want to be able to compute the meaning of
;; an MG statement.  To do so, I build a procedure around it and show by the lemma
;; translation-is-correct2 that the meaning of the statement is the execution of that 
;; procedure.
;; 
;; This takes an alist from the mg-state and turns it into
;; a list of local-var-decls as might appear in a Micro-Gypsy
;; procedure.

;; Does this do anything;  the alist is already in the right form.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{make-mg-locals-list} \\  
\=\+{\rm{make-mg-locals-list}}\,({\it{mg-alist\/}})\index{make-mg-locals-list} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{mg-alist\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{cons}}\,(\=\+{\rm{list}}\,(\=\+{\rm{name}}\,({\rm{car}}\,({\it{mg-alist\/}}))\index{name}, \\ 
{\rm{m-type}}\,({\rm{car}}\,({\it{mg-alist\/}}))\index{m-type}, \\ 
{\rm{m-value}}\,({\rm{car}}\,({\it{mg-alist\/}}))\index{m-value})\-, \\ 
{\rm{make-mg-locals-list}}\,({\rm{cdr}}\,({\it{mg-alist\/}}))\index{make-mg-locals-list})\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  make-mg-local-list-preserves-listcars \\ \index{make-mg-local-list-preserves-li!stcars}
{\rm{listcars}}\,({\rm{make-mg-locals-list}}\,({\it{lst\/}})\index{make-mg-locals-list})\index{listcars} $=$ {\rm{listcars}}\,({\it{lst\/}})\index{listcars}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  make-mg-locals-list-ok-mg-local-data-plistp \\ \index{make-mg-locals-list-ok-mg-local!-data-plistp}
\=\+{\rm{mg-alistp}}\,({\it{mg-alist\/}})\index{mg-alistp} \\ 
$\rightarrow$$\;\;\;\;${\rm{ok-mg-local-data-plistp}}\,({\rm{make-mg-locals-list}}\,({\it{mg-alist\/}})\index{make-mg-locals-list})\index{ok-mg-local-data-plistp}\-
\end{tabbing}

\begin{verbatim};; The point of this is to cons up a new user-defined-procedure
;; definition from the following components:
;;    alist: the Micro-Gypsy variable alist in which the statement is
;;        to be interpreted.
;;    subr: a user-supplied name;
;;    stmt: the statement which we are interpreting
;;    cond-list: a list of conditions which we will allow
;;        to be raised.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{make-mg-proc} \\  
\=\+{\rm{make-mg-proc}}\,({\it{alist\/}}, {\it{subr\/}}, {\it{stmt\/}}, {\it{cond-list\/}})\index{make-mg-proc} \\ 
$=$$\;\;\;\;${\rm{list}}\,({\it{subr\/}}, {\bf{nil}}, {\it{cond-list\/}}, {\rm{make-mg-locals-list}}\,({\it{alist\/}})\index{make-mg-locals-list}, {\bf{nil}}, {\it{stmt\/}})\-
\end{tabbing}

\begin{verbatim};; Initial-temp-stk places the values of the mg-alist variables onto the temp-stk;
;; initial-bindings creates the Piton bindings corresponding to that initial
;; temp-stk.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{initial-temp-stk-reversed} \\  
\=\+{\rm{initial-temp-stk-reversed}}\,({\it{mg-alist\/}})\index{initial-temp-stk-reversed} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{mg-alist\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf elseif }{\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\rm{car}}\,({\it{mg-alist\/}})))\index{simple-mg-type-refp} \\ 
{\bf then }{\rm{cons}}\,(\=\+{\rm{mg-to-p-simple-literal}}\,({\rm{caddr}}\,({\rm{car}}\,({\it{mg-alist\/}})))\index{mg-to-p-simple-literal}, \\ 
{\rm{initial-temp-stk-reversed}}\,({\rm{cdr}}\,({\it{mg-alist\/}}))\index{initial-temp-stk-reversed})\- \\ 
{\bf else }{\rm{append}}\,(\=\+{\rm{mg-to-p-simple-literal-list}}\,({\rm{caddr}}\,({\rm{car}}\,({\it{mg-alist\/}})))\index{mg-to-p-simple-literal-list}, \\ 
{\rm{initial-temp-stk-reversed}}\,({\rm{cdr}}\,({\it{mg-alist\/}}))\index{initial-temp-stk-reversed})\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  initial-temp-stk-reversed-plistp \\ \index{initial-temp-stk-reversed-plistp}
{\rm{plistp}}\,({\rm{initial-temp-stk-reversed}}\,({\it{x\/}})\index{initial-temp-stk-reversed})\index{plistp}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{initial-temp-stk} \\  
{\rm{initial-temp-stk}}\,({\it{mg-alist\/}})\index{initial-temp-stk} $=$ {\rm{reverse}}\,({\rm{initial-temp-stk-reversed}}\,({\it{mg-alist\/}})\index{initial-temp-stk-reversed})\index{reverse}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{initial-bindings} \\  
\=\+{\rm{initial-bindings}}\,({\it{mg-alist\/}}, {\it{n\/}})\index{initial-bindings} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{mg-alist\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf elseif }{\rm{simple-mg-type-refp}}\,({\rm{cadr}}\,({\rm{car}}\,({\it{mg-alist\/}})))\index{simple-mg-type-refp} \\ 
{\bf then }{\rm{cons}}\,(\=\+{\rm{cons}}\,({\rm{caar}}\,({\it{mg-alist\/}}), {\rm{tag}}\,({\tt{'}}{\tt{nat}}, {\it{n\/}})\index{tag}), \\ 
{\rm{initial-bindings}}\,({\rm{cdr}}\,({\it{mg-alist\/}}), $1\;+$ {\it{n\/}})\index{initial-bindings})\- \\ 
{\bf else }{\rm{cons}}\,(\=\+{\rm{cons}}\,({\rm{caar}}\,({\it{mg-alist\/}}), {\rm{tag}}\,({\tt{'}}{\tt{nat}}, {\it{n\/}})\index{tag}), \\ 
{\rm{initial-bindings}}\,(\=\+{\rm{cdr}}\,({\it{mg-alist\/}}), \\ 
{\it{n\/}} $+$ {\rm{array-length}}\,({\rm{cadr}}\,({\rm{car}}\,({\it{mg-alist\/}})))\index{array-length})\-\index{initial-bindings})\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  length-initial-bindings \\ \index{length-initial-bindings}
{\rm{length}}\,({\rm{initial-bindings}}\,({\it{alist\/}}, {\it{n\/}})\index{initial-bindings})\index{length} $=$ {\rm{length}}\,({\it{alist\/}})\index{length}
\end{tabbing}

\begin{verbatim};; 10/4/88 changing the final return pc from nil to (pc (subr . 0))
;;         It is ignored but must be a legal pc value.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{map-down1} \\  
\=\+{\rm{map-down1}}\,({\it{mg-state\/}}, {\it{proc-list\/}}, {\it{cond-list\/}}, {\it{subr\/}}, {\it{stmt\/}})\index{map-down1} \\ 
$=$$\;\;\;\;${\rm{map-down}}\,(\=\+{\it{mg-state\/}}, \\ 
{\rm{cons}}\,(\=\+{\rm{make-mg-proc}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\it{subr\/}}, {\it{stmt\/}}, {\it{cond-list\/}})\index{make-mg-proc}, \\ 
{\it{proc-list\/}})\-, \\ 
{\rm{list}}\,({\rm{cons}}\,(\=\+{\rm{initial-bindings}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\tt{0}})\index{initial-bindings}, \\ 
{\rm{list}}\,({\rm{tag}}\,({\tt{'}}{\tt{pc}}, {\rm{cons}}\,({\it{subr\/}}, {\tt{0}}))\index{tag}))\-), \\ 
{\rm{initial-temp-stk}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{initial-temp-stk}, \\ 
{\rm{tag}}\,({\tt{'}}{\tt{pc}}, {\rm{cons}}\,({\it{subr\/}}, {\tt{0}}))\index{tag}, \\ 
{\it{cond-list\/}})\-\index{map-down}\-
\end{tabbing}

\begin{verbatim};; This theorem shows that I can compute the meaning of a statement if you will give me 
;; the following and guarantee the following:
;;    proc-list:   must be a legitimate MG procedure list;
;;    cond-list:   a list of conditions you will allow to be raised;
;;    mg-state:    a legitimate MG state with current condition constrained by cond-list,
;;                    names on the alist must all be unique;
;;    stmt:        must be a legal statement with respect to proc-list and cond-list;
;;    n:           the clock parameter saying how long to let the thing run;
;;    :   an integer telling me the size of the implementation ;
;;    subr:   a litatom which is not the name of any procedure on proc-list;
;;
;; Supplied with these things, I can show you the meaning of a statement (provided that
;; the computation does not run out of time or space.

;;(defn ok-cond-list1 (cond-list)
;;       (and (ok-cond-list cond-list)
;;	    (not (member 'leave cond-list))))

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{new-proc-name} \\  
\=\+{\rm{new-proc-name}}\,({\it{x\/}}, {\it{proc-list\/}})\index{new-proc-name} \\ 
$=$$\;\;\;\;$({\rm{ok-mg-namep}}\,({\it{x\/}})\index{ok-mg-namep} $\wedge$ ($\neg$ {\rm{defined-procp}}\,({\it{x\/}}, {\it{proc-list\/}})\index{defined-procp}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  new-proc-doesnt-affect-fetch-called-def \\ \index{new-proc-doesnt-affect-fetch-ca!lled-def}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{new-proc-name}}\,({\rm{car}}\,({\it{new-proc\/}}), {\it{proc-list\/}})\index{new-proc-name} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{fetch-called-def}}\,({\it{stmt\/}}, {\rm{cons}}\,({\it{new-proc\/}}, {\it{proc-list\/}}))\index{fetch-called-def} \\ 
$=$$\;\;\;\;${\rm{fetch-called-def}}\,({\it{stmt\/}}, {\it{proc-list\/}})\index{fetch-called-def})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  new-proc-doesnt-affect-mg-meaning-proc-call-case \\ \index{new-proc-doesnt-affect-mg-meani!ng-proc-call-case}
\=\+(\=\+({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;${\rm{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+{\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,(\=\+{\rm{def-body}}\,({\rm{fetch-called-def}}\,({\it{stmt\/}}, {\it{proc-list\/}})\index{fetch-called-def})\index{def-body}, \\ 
{\rm{make-cond-list}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{make-cond-list}, \\ 
{\rm{make-name-alist}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{make-name-alist}, \\ 
{\it{proc-list\/}})\-\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{new-proc-name}}\,({\rm{car}}\,({\it{new-proc\/}}), {\it{proc-list\/}})\index{new-proc-name})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{mg-meaning}}\,(\=\+{\rm{def-body}}\,({\rm{fetch-called-def}}\,({\it{stmt\/}}, {\it{proc-list\/}})\index{fetch-called-def})\index{def-body}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{make-call-environment}}\,(\=\+{\it{mg-state\/}}, \\ 
{\it{stmt\/}}, \\ 
{\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\-\index{make-call-environment}, \\ 
{\it{n\/}} $-\;1$)\-\index{mg-meaning} \\ 
$=$$\;\;\;\;${\rm{mg-meaning}}\,(\=\+{\rm{def-body}}\,({\rm{fetch-called-def}}\,({\it{stmt\/}}, {\it{proc-list\/}})\index{fetch-called-def})\index{def-body}, \\ 
{\rm{cons}}\,({\it{new-proc\/}}, {\it{proc-list\/}}), \\ 
{\rm{make-call-environment}}\,(\=\+{\it{mg-state\/}}, \\ 
{\it{stmt\/}}, \\ 
{\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\-\index{make-call-environment}, \\ 
{\it{n\/}} $-\;1$)\-\index{mg-meaning})\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{new-proc-name}}\,({\rm{car}}\,({\it{new-proc\/}}), {\it{proc-list\/}})\index{new-proc-name})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{mg-meaning}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}})\index{mg-meaning} \\ 
$=$$\;\;\;\;${\rm{mg-meaning}}\,({\it{stmt\/}}, {\rm{cons}}\,({\it{new-proc\/}}, {\it{proc-list\/}}), {\it{mg-state\/}}, {\it{n\/}})\index{mg-meaning})\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{meaning-induction-hint3} \\  
\=\+{\rm{meaning-induction-hint3}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}}, \\ 
{\it{name-alist\/}}, \\ 
{\it{cond-list\/}}, \\ 
{\it{new-proc\/}})\-\index{meaning-induction-hint3} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }$\neg$ {\rm{normal}}\,({\it{mg-state\/}})\index{normal}$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{no-op-mg}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{signal-mg}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{prog2-mg}} \\ 
{\bf then }\=\+{\rm{meaning-induction-hint3}}\,(\=\+{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{name-alist\/}}, \\ 
{\it{cond-list\/}}, \\ 
{\it{new-proc\/}})\-\index{meaning-induction-hint3} \\ 
$\wedge$$\;\;\;\;${\rm{meaning-induction-hint3}}\,(\=\+{\rm{prog2-right-branch}}\,({\it{stmt\/}})\index{prog2-right-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{mg-meaning}}\,(\=\+{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\rm{cons}}\,(\=\+{\it{new-proc\/}}, \\ 
{\it{proc-list\/}})\-, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$)\-\index{mg-meaning}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{name-alist\/}}, \\ 
{\it{cond-list\/}}, \\ 
{\it{new-proc\/}})\-\index{meaning-induction-hint3}\- \\ 
{\bf elseif }{\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{loop-mg}} \\ 
{\bf then }\=\+{\rm{meaning-induction-hint3}}\,(\=\+{\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{name-alist\/}}, \\ 
{\rm{cons}}\,({\tt{'}}{\tt{leave}}, {\it{cond-list\/}}), \\ 
{\it{new-proc\/}})\-\index{meaning-induction-hint3} \\ 
$\wedge$$\;\;\;\;${\rm{meaning-induction-hint3}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{mg-meaning}}\,(\=\+{\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, \\ 
{\rm{cons}}\,(\=\+{\it{new-proc\/}}, \\ 
{\it{proc-list\/}})\-, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$)\-\index{mg-meaning}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{name-alist\/}}, \\ 
{\it{cond-list\/}}, \\ 
{\it{new-proc\/}})\-\index{meaning-induction-hint3}\- \\ 
{\bf elseif }{\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{if-mg}} \\ 
{\bf then }\=\+{\rm{meaning-induction-hint3}}\,(\=\+{\rm{if-false-branch}}\,({\it{stmt\/}})\index{if-false-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{name-alist\/}}, \\ 
{\it{cond-list\/}}, \\ 
{\it{new-proc\/}})\-\index{meaning-induction-hint3} \\ 
$\wedge$$\;\;\;\;${\rm{meaning-induction-hint3}}\,(\=\+{\rm{if-true-branch}}\,({\it{stmt\/}})\index{if-true-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{name-alist\/}}, \\ 
{\it{cond-list\/}}, \\ 
{\it{new-proc\/}})\-\index{meaning-induction-hint3}\- \\ 
{\bf elseif }{\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{begin-mg}} \\ 
{\bf then }\=\+{\rm{meaning-induction-hint3}}\,(\=\+{\rm{begin-body}}\,({\it{stmt\/}})\index{begin-body}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{name-alist\/}}, \\ 
{\rm{append}}\,({\rm{when-labels}}\,({\it{stmt\/}})\index{when-labels}, {\it{cond-list\/}}), \\ 
{\it{new-proc\/}})\-\index{meaning-induction-hint3} \\ 
$\wedge$$\;\;\;\;${\rm{meaning-induction-hint3}}\,(\=\+{\rm{when-handler}}\,({\it{stmt\/}})\index{when-handler}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{set-condition}}\,(\=\+{\rm{mg-meaning}}\,(\=\+{\rm{begin-body}}\,({\it{stmt\/}})\index{begin-body}, \\ 
{\rm{cons}}\,(\=\+{\it{new-proc\/}}, \\ 
{\it{proc-list\/}})\-, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$)\-\index{mg-meaning}, \\ 
{\tt{'}}{\tt{normal}})\-\index{set-condition}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{name-alist\/}}, \\ 
{\it{cond-list\/}}, \\ 
{\it{new-proc\/}})\-\index{meaning-induction-hint3}\- \\ 
{\bf elseif }{\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{proc-call-mg}} \\ 
{\bf then }{\rm{meaning-induction-hint3}}\,(\=\+{\rm{def-body}}\,({\rm{fetch-called-def}}\,({\it{stmt\/}}, {\it{proc-list\/}})\index{fetch-called-def})\index{def-body}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{make-call-environment}}\,(\=\+{\it{mg-state\/}}, \\ 
{\it{stmt\/}}, \\ 
{\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\-\index{make-call-environment}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\rm{make-name-alist}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{make-name-alist}, \\ 
{\rm{make-cond-list}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{make-cond-list}, \\ 
{\it{new-proc\/}})\-\index{meaning-induction-hint3} \\ 
{\bf elseif }{\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{predefined-proc-call-mg}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};; >>> For an automatic proof, these rules should be oriented in the other direction.  Otherwise,
;;     they could cause looping.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  new-proc-doesnt-affect-mg-meaning \\ \index{new-proc-doesnt-affect-mg-meani!ng}
\=\+(\=\+{\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{new-proc-name}}\,({\rm{car}}\,({\it{new-proc\/}}), {\it{proc-list\/}})\index{new-proc-name})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{mg-meaning}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}})\index{mg-meaning} \\ 
$=$$\;\;\;\;${\rm{mg-meaning}}\,({\it{stmt\/}}, {\rm{cons}}\,({\it{new-proc\/}}, {\it{proc-list\/}}), {\it{mg-state\/}}, {\it{n\/}})\index{mg-meaning})\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{meaning-induction-hint4} \\  
\=\+{\rm{meaning-induction-hint4}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}}, \\ 
{\it{name-alist\/}}, \\ 
{\it{cond-list\/}}, \\ 
{\it{new-proc\/}}, \\ 
{\it{sizes\/}})\-\index{meaning-induction-hint4} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }$\neg$ {\rm{normal}}\,({\it{mg-state\/}})\index{normal}$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\rm{resources-inadequatep}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{sizes\/}})\index{resources-inadequatep}$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{no-op-mg}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{signal-mg}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{prog2-mg}} \\ 
{\bf then }\=\+{\rm{meaning-induction-hint4}}\,(\=\+{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{name-alist\/}}, \\ 
{\it{cond-list\/}}, \\ 
{\it{new-proc\/}}, \\ 
{\it{sizes\/}})\-\index{meaning-induction-hint4} \\ 
$\wedge$$\;\;\;\;${\rm{meaning-induction-hint4}}\,(\=\+{\rm{prog2-right-branch}}\,({\it{stmt\/}})\index{prog2-right-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{mg-meaning-r}}\,(\=\+{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\rm{cons}}\,(\=\+{\it{new-proc\/}}, \\ 
{\it{proc-list\/}})\-, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{sizes\/}})\-\index{mg-meaning-r}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{name-alist\/}}, \\ 
{\it{cond-list\/}}, \\ 
{\it{new-proc\/}}, \\ 
{\it{sizes\/}})\-\index{meaning-induction-hint4}\- \\ 
{\bf elseif }{\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{loop-mg}} \\ 
{\bf then }\=\+{\rm{meaning-induction-hint4}}\,(\=\+{\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{name-alist\/}}, \\ 
{\rm{cons}}\,({\tt{'}}{\tt{leave}}, {\it{cond-list\/}}), \\ 
{\it{new-proc\/}}, \\ 
{\it{sizes\/}})\-\index{meaning-induction-hint4} \\ 
$\wedge$$\;\;\;\;${\rm{meaning-induction-hint4}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{mg-meaning-r}}\,(\=\+{\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, \\ 
{\rm{cons}}\,(\=\+{\it{new-proc\/}}, \\ 
{\it{proc-list\/}})\-, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{sizes\/}})\-\index{mg-meaning-r}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{name-alist\/}}, \\ 
{\it{cond-list\/}}, \\ 
{\it{new-proc\/}}, \\ 
{\it{sizes\/}})\-\index{meaning-induction-hint4}\- \\ 
{\bf elseif }{\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{if-mg}} \\ 
{\bf then }\=\+{\rm{meaning-induction-hint4}}\,(\=\+{\rm{if-false-branch}}\,({\it{stmt\/}})\index{if-false-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{name-alist\/}}, \\ 
{\it{cond-list\/}}, \\ 
{\it{new-proc\/}}, \\ 
{\it{sizes\/}})\-\index{meaning-induction-hint4} \\ 
$\wedge$$\;\;\;\;${\rm{meaning-induction-hint4}}\,(\=\+{\rm{if-true-branch}}\,({\it{stmt\/}})\index{if-true-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{name-alist\/}}, \\ 
{\it{cond-list\/}}, \\ 
{\it{new-proc\/}}, \\ 
{\it{sizes\/}})\-\index{meaning-induction-hint4}\- \\ 
{\bf elseif }{\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{begin-mg}} \\ 
{\bf then }\=\+{\rm{meaning-induction-hint4}}\,(\=\+{\rm{begin-body}}\,({\it{stmt\/}})\index{begin-body}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\it{name-alist\/}}, \\ 
{\rm{append}}\,({\rm{when-labels}}\,({\it{stmt\/}})\index{when-labels}, {\it{cond-list\/}}), \\ 
{\it{new-proc\/}}, \\ 
{\it{sizes\/}})\-\index{meaning-induction-hint4} \\ 
$\wedge$$\;\;\;\;${\rm{meaning-induction-hint4}}\,(\=\+{\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}, \\ 
{\rm{cons}}\,(\=\+{\it{new-proc\/}}, \\ 
{\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{name-alist\/}}, \\ 
{\it{cond-list\/}}, \\ 
{\it{new-proc\/}}, \\ 
{\it{sizes\/}})\-\index{meaning-induction-hint4}\- \\ 
{\bf elseif }{\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{proc-call-mg}} \\ 
{\bf then }{\rm{meaning-induction-hint4}}\,(\=\+{\rm{def-body}}\,({\rm{fetch-called-def}}\,({\it{stmt\/}}, {\it{proc-list\/}})\index{fetch-called-def})\index{def-body}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{make-call-environment}}\,(\=\+{\it{mg-state\/}}, \\ 
{\it{stmt\/}}, \\ 
{\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\-\index{make-call-environment}, \\ 
{\it{n\/}} $-\;1$, \\ 
{\rm{make-name-alist}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{make-name-alist}, \\ 
{\rm{make-cond-list}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{make-cond-list}, \\ 
{\it{new-proc\/}}, \\ 
{\rm{list}}\,(\=\+\=\+{\rm{t-size}}\,({\it{sizes\/}})\index{t-size} \\ 
$+$$\;\;\;\;${\rm{data-length}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{data-length}\-, \\ 
\=\+{\rm{c-size}}\,({\it{sizes\/}})\index{c-size} \\ 
$+$$\;\;\;\;$(\=\+{\tt{2}} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\rm{def-locals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-locals})\index{length} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\rm{def-formals}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{def-formals})\index{length})\-\-)\-)\-\index{meaning-induction-hint4} \\ 
{\bf elseif }{\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{predefined-proc-call-mg}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  new-proc-doesnt-affect-resources-inadequatep \\ \index{new-proc-doesnt-affect-resource!s-inadequatep}
\=\+(\=\+{\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{new-proc-name}}\,({\rm{car}}\,({\it{new-proc\/}}), {\it{proc-list\/}})\index{new-proc-name})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{resources-inadequatep}}\,({\it{stmt\/}}, {\rm{cons}}\,({\it{new-proc\/}}, {\it{proc-list\/}}), {\it{sizes\/}})\index{resources-inadequatep} \\ 
$=$$\;\;\;\;${\rm{resources-inadequatep}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{sizes\/}})\index{resources-inadequatep})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  new-proc-doesnt-affect-mg-meaning-r \\ \index{new-proc-doesnt-affect-mg-meani!ng-r}
\=\+(\=\+{\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{new-proc-name}}\,({\rm{car}}\,({\it{new-proc\/}}), {\it{proc-list\/}})\index{new-proc-name})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{mg-meaning-r}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}}, {\it{sizes\/}})\index{mg-meaning-r} \\ 
$=$$\;\;\;\;${\rm{mg-meaning-r}}\,({\it{stmt\/}}, {\rm{cons}}\,({\it{new-proc\/}}, {\it{proc-list\/}}), {\it{mg-state\/}}, {\it{n\/}}, {\it{sizes\/}})\index{mg-meaning-r})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  new-proc-doesnt-affect-mg-meaning-r-2 \\ \index{new-proc-doesnt-affect-mg-meani!ng-r-2}
\=\+(\=\+{\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{new-proc-name}}\,({\rm{car}}\,({\it{new-proc\/}}), {\it{proc-list\/}})\index{new-proc-name})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{mg-meaning-r}}\,({\it{stmt\/}}, {\rm{cons}}\,({\it{new-proc\/}}, {\it{proc-list\/}}), {\it{mg-state\/}}, {\it{n\/}}, {\it{sizes\/}})\index{mg-meaning-r} \\ 
$=$$\;\;\;\;${\rm{mg-meaning-r}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}}, {\it{sizes\/}})\index{mg-meaning-r})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  new-proc-doesnt-affect-clock-prog2-case \\ \index{new-proc-doesnt-affect-clock-pr!og2-case}
\=\+(\=\+({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;${\rm{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{prog2-mg}}) \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+{\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,(\=\+{\rm{prog2-right-branch}}\,({\it{stmt\/}})\index{prog2-right-branch}, \\ 
{\it{cond-list\/}}, \\ 
{\it{name-alist\/}}, \\ 
{\it{proc-list\/}})\-\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{new-proc-name}}\,({\rm{car}}\,({\it{new-proc\/}}), {\it{proc-list\/}})\index{new-proc-name})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{clock}}\,(\=\+{\rm{prog2-right-branch}}\,({\it{stmt\/}})\index{prog2-right-branch}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{mg-meaning}}\,(\=\+{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\rm{cons}}\,({\it{new-proc\/}}, {\it{proc-list\/}}), \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$)\-\index{mg-meaning}, \\ 
{\it{n\/}} $-\;1$)\-\index{clock} \\ 
$=$$\;\;\;\;${\rm{clock}}\,(\=\+{\rm{prog2-right-branch}}\,({\it{stmt\/}})\index{prog2-right-branch}, \\ 
{\rm{cons}}\,({\it{new-proc\/}}, {\it{proc-list\/}}), \\ 
{\rm{mg-meaning}}\,(\=\+{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\rm{cons}}\,({\it{new-proc\/}}, {\it{proc-list\/}}), \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$)\-\index{mg-meaning}, \\ 
{\it{n\/}} $-\;1$)\-\index{clock})\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+{\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,(\=\+{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\it{cond-list\/}}, \\ 
{\it{name-alist\/}}, \\ 
{\it{proc-list\/}})\-\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{new-proc-name}}\,({\rm{car}}\,({\it{new-proc\/}}), {\it{proc-list\/}})\index{new-proc-name})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{clock}}\,({\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}} $-\;1$)\index{clock} \\ 
$=$$\;\;\;\;${\rm{clock}}\,(\=\+{\rm{prog2-left-branch}}\,({\it{stmt\/}})\index{prog2-left-branch}, \\ 
{\rm{cons}}\,({\it{new-proc\/}}, {\it{proc-list\/}}), \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$)\-\index{clock})\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{new-proc-name}}\,({\rm{car}}\,({\it{new-proc\/}}), {\it{proc-list\/}})\index{new-proc-name})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{clock}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}})\index{clock} \\ 
$=$$\;\;\;\;${\rm{clock}}\,({\it{stmt\/}}, {\rm{cons}}\,({\it{new-proc\/}}, {\it{proc-list\/}}), {\it{mg-state\/}}, {\it{n\/}})\index{clock})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  new-proc-doesnt-affect-clock-loop-case \\ \index{new-proc-doesnt-affect-clock-lo!op-case}
\=\+(\=\+({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;${\rm{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{loop-mg}}) \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+{\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{new-proc-name}}\,({\rm{car}}\,({\it{new-proc\/}}), {\it{proc-list\/}})\index{new-proc-name})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{clock}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{mg-meaning}}\,(\=\+{\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, \\ 
{\rm{cons}}\,({\it{new-proc\/}}, {\it{proc-list\/}}), \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$)\-\index{mg-meaning}, \\ 
{\it{n\/}} $-\;1$)\-\index{clock} \\ 
$=$$\;\;\;\;${\rm{clock}}\,(\=\+{\it{stmt\/}}, \\ 
{\rm{cons}}\,({\it{new-proc\/}}, {\it{proc-list\/}}), \\ 
{\rm{mg-meaning}}\,(\=\+{\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, \\ 
{\rm{cons}}\,({\it{new-proc\/}}, {\it{proc-list\/}}), \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$)\-\index{mg-meaning}, \\ 
{\it{n\/}} $-\;1$)\-\index{clock})\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+{\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,(\=\+{\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, \\ 
{\rm{cons}}\,({\tt{'}}{\tt{leave}}, {\it{cond-list\/}}), \\ 
{\it{name-alist\/}}, \\ 
{\it{proc-list\/}})\-\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{new-proc-name}}\,({\rm{car}}\,({\it{new-proc\/}}), {\it{proc-list\/}})\index{new-proc-name})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{clock}}\,({\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}} $-\;1$)\index{clock} \\ 
$=$$\;\;\;\;${\rm{clock}}\,(\=\+{\rm{loop-body}}\,({\it{stmt\/}})\index{loop-body}, \\ 
{\rm{cons}}\,({\it{new-proc\/}}, {\it{proc-list\/}}), \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$)\-\index{clock})\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{new-proc-name}}\,({\rm{car}}\,({\it{new-proc\/}}), {\it{proc-list\/}})\index{new-proc-name})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{clock}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}})\index{clock} \\ 
$=$$\;\;\;\;${\rm{clock}}\,({\it{stmt\/}}, {\rm{cons}}\,({\it{new-proc\/}}, {\it{proc-list\/}}), {\it{mg-state\/}}, {\it{n\/}})\index{clock})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  new-proc-doesnt-affect-clock-if-case \\ \index{new-proc-doesnt-affect-clock-if!-case}
\=\+(\=\+({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;${\rm{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{if-mg}}) \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+{\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,(\=\+{\rm{if-true-branch}}\,({\it{stmt\/}})\index{if-true-branch}, \\ 
{\it{cond-list\/}}, \\ 
{\it{name-alist\/}}, \\ 
{\it{proc-list\/}})\-\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{new-proc-name}}\,({\rm{car}}\,({\it{new-proc\/}}), {\it{proc-list\/}})\index{new-proc-name})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{clock}}\,({\rm{if-true-branch}}\,({\it{stmt\/}})\index{if-true-branch}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}} $-\;1$)\index{clock} \\ 
$=$$\;\;\;\;${\rm{clock}}\,(\=\+{\rm{if-true-branch}}\,({\it{stmt\/}})\index{if-true-branch}, \\ 
{\rm{cons}}\,({\it{new-proc\/}}, {\it{proc-list\/}}), \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$)\-\index{clock})\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+{\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,(\=\+{\rm{if-false-branch}}\,({\it{stmt\/}})\index{if-false-branch}, \\ 
{\it{cond-list\/}}, \\ 
{\it{name-alist\/}}, \\ 
{\it{proc-list\/}})\-\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{new-proc-name}}\,({\rm{car}}\,({\it{new-proc\/}}), {\it{proc-list\/}})\index{new-proc-name})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{clock}}\,({\rm{if-false-branch}}\,({\it{stmt\/}})\index{if-false-branch}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}} $-\;1$)\index{clock} \\ 
$=$$\;\;\;\;${\rm{clock}}\,(\=\+{\rm{if-false-branch}}\,({\it{stmt\/}})\index{if-false-branch}, \\ 
{\rm{cons}}\,({\it{new-proc\/}}, {\it{proc-list\/}}), \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$)\-\index{clock})\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{new-proc-name}}\,({\rm{car}}\,({\it{new-proc\/}}), {\it{proc-list\/}})\index{new-proc-name})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{clock}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}})\index{clock} \\ 
$=$$\;\;\;\;${\rm{clock}}\,({\it{stmt\/}}, {\rm{cons}}\,({\it{new-proc\/}}, {\it{proc-list\/}}), {\it{mg-state\/}}, {\it{n\/}})\index{clock})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  new-proc-doesnt-affect-clock-begin-case \\ \index{new-proc-doesnt-affect-clock-be!gin-case}
\=\+(\=\+({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;${\rm{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{begin-mg}}) \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+{\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,(\=\+{\rm{when-handler}}\,({\it{stmt\/}})\index{when-handler}, \\ 
{\it{cond-list\/}}, \\ 
{\it{name-alist\/}}, \\ 
{\it{proc-list\/}})\-\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{new-proc-name}}\,({\rm{car}}\,({\it{new-proc\/}}), {\it{proc-list\/}})\index{new-proc-name})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{clock}}\,(\=\+{\rm{when-handler}}\,({\it{stmt\/}})\index{when-handler}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{set-condition}}\,(\=\+{\rm{mg-meaning}}\,(\=\+{\rm{begin-body}}\,({\it{stmt\/}})\index{begin-body}, \\ 
{\rm{cons}}\,({\it{new-proc\/}}, {\it{proc-list\/}}), \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$)\-\index{mg-meaning}, \\ 
{\tt{'}}{\tt{normal}})\-\index{set-condition}, \\ 
{\it{n\/}} $-\;1$)\-\index{clock} \\ 
$=$$\;\;\;\;${\rm{clock}}\,(\=\+{\rm{when-handler}}\,({\it{stmt\/}})\index{when-handler}, \\ 
{\rm{cons}}\,({\it{new-proc\/}}, {\it{proc-list\/}}), \\ 
{\rm{set-condition}}\,(\=\+{\rm{mg-meaning}}\,(\=\+{\rm{begin-body}}\,({\it{stmt\/}})\index{begin-body}, \\ 
{\rm{cons}}\,(\=\+{\it{new-proc\/}}, \\ 
{\it{proc-list\/}})\-, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$)\-\index{mg-meaning}, \\ 
{\tt{'}}{\tt{normal}})\-\index{set-condition}, \\ 
{\it{n\/}} $-\;1$)\-\index{clock})\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+{\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,(\=\+{\rm{begin-body}}\,({\it{stmt\/}})\index{begin-body}, \\ 
{\rm{append}}\,({\rm{when-labels}}\,({\it{stmt\/}})\index{when-labels}, {\it{cond-list\/}}), \\ 
{\it{name-alist\/}}, \\ 
{\it{proc-list\/}})\-\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{new-proc-name}}\,({\rm{car}}\,({\it{new-proc\/}}), {\it{proc-list\/}})\index{new-proc-name})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{clock}}\,({\rm{begin-body}}\,({\it{stmt\/}})\index{begin-body}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}} $-\;1$)\index{clock} \\ 
$=$$\;\;\;\;${\rm{clock}}\,(\=\+{\rm{begin-body}}\,({\it{stmt\/}})\index{begin-body}, \\ 
{\rm{cons}}\,({\it{new-proc\/}}, {\it{proc-list\/}}), \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}} $-\;1$)\-\index{clock})\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{new-proc-name}}\,({\rm{car}}\,({\it{new-proc\/}}), {\it{proc-list\/}})\index{new-proc-name})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{clock}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}})\index{clock} \\ 
$=$$\;\;\;\;${\rm{clock}}\,({\it{stmt\/}}, {\rm{cons}}\,({\it{new-proc\/}}, {\it{proc-list\/}}), {\it{mg-state\/}}, {\it{n\/}})\index{clock})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  new-proc-doesnt-affect-clock-proc-call-case \\ \index{new-proc-doesnt-affect-clock-pr!oc-call-case}
\=\+(\=\+({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;${\rm{normal}}\,({\it{mg-state\/}})\index{normal} \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+{\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,(\=\+{\rm{def-body}}\,({\rm{fetch-called-def}}\,({\it{stmt\/}}, {\it{proc-list\/}})\index{fetch-called-def})\index{def-body}, \\ 
{\rm{make-cond-list}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{make-cond-list}, \\ 
{\rm{make-name-alist}}\,({\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\index{make-name-alist}, \\ 
{\it{proc-list\/}})\-\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{new-proc-name}}\,({\rm{car}}\,({\it{new-proc\/}}), {\it{proc-list\/}})\index{new-proc-name})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{clock}}\,(\=\+{\rm{def-body}}\,({\rm{fetch-called-def}}\,({\it{stmt\/}}, {\it{proc-list\/}})\index{fetch-called-def})\index{def-body}, \\ 
{\it{proc-list\/}}, \\ 
{\rm{make-call-environment}}\,(\=\+{\it{mg-state\/}}, \\ 
{\it{stmt\/}}, \\ 
{\rm{fetch-called-def}}\,({\it{stmt\/}}, {\it{proc-list\/}})\index{fetch-called-def})\-\index{make-call-environment}, \\ 
{\it{n\/}} $-\;1$)\-\index{clock} \\ 
$=$$\;\;\;\;${\rm{clock}}\,(\=\+{\rm{def-body}}\,({\rm{fetch-called-def}}\,({\it{stmt\/}}, {\it{proc-list\/}})\index{fetch-called-def})\index{def-body}, \\ 
{\rm{cons}}\,({\it{new-proc\/}}, {\it{proc-list\/}}), \\ 
{\rm{make-call-environment}}\,(\=\+{\it{mg-state\/}}, \\ 
{\it{stmt\/}}, \\ 
{\rm{fetch-called-def}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}})\-\index{fetch-called-def})\-\index{make-call-environment}, \\ 
{\it{n\/}} $-\;1$)\-\index{clock})\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{new-proc-name}}\,({\rm{car}}\,({\it{new-proc\/}}), {\it{proc-list\/}})\index{new-proc-name})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{clock}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}})\index{clock} \\ 
$=$$\;\;\;\;${\rm{clock}}\,({\it{stmt\/}}, {\rm{cons}}\,({\it{new-proc\/}}, {\it{proc-list\/}}), {\it{mg-state\/}}, {\it{n\/}})\index{clock})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  new-proc-doesnt-affect-clock \\ \index{new-proc-doesnt-affect-clock}
\=\+(\=\+{\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{new-proc-name}}\,({\rm{car}}\,({\it{new-proc\/}}), {\it{proc-list\/}})\index{new-proc-name})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{clock}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}})\index{clock} \\ 
$=$$\;\;\;\;${\rm{clock}}\,({\it{stmt\/}}, {\rm{cons}}\,({\it{new-proc\/}}, {\it{proc-list\/}}), {\it{mg-state\/}}, {\it{n\/}})\index{clock})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  new-proc-doesnt-affect-ok-mg-statement-proc-call-case \\ \index{new-proc-doesnt-affect-ok-mg-st!atement-proc-call-case}
\=\+(\=\+({\rm{car}}\,({\it{stmt\/}}) $=$ {\tt{'}}{\tt{proc-call-mg}}) \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{new-proc-name}}\,({\rm{car}}\,({\it{new-proc\/}}), {\it{proc-list\/}})\index{new-proc-name})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{cond-list\/}}, {\it{name-alist\/}}, {\rm{cons}}\,({\it{new-proc\/}}, {\it{proc-list\/}}))\index{ok-mg-statement}\-
\end{tabbing}


\noindent{\sc Event}:   Enable ok-mg-statement.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  new-proc-doesnt-affect-ok-mg-statement \\ \index{new-proc-doesnt-affect-ok-mg-st!atement}
\=\+(\=\+{\rm{ok-mg-def-plistp}}\,({\it{proc-list\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{cond-list\/}}, {\it{name-alist\/}}, {\it{proc-list\/}})\index{ok-mg-statement} \\ 
$\wedge$$\;\;\;\;${\rm{new-proc-name}}\,({\rm{car}}\,({\it{new-proc\/}}), {\it{proc-list\/}})\index{new-proc-name})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{cond-list\/}}, {\it{name-alist\/}}, {\rm{cons}}\,({\it{new-proc\/}}, {\it{proc-list\/}}))\index{ok-mg-statement}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  new-proc-preserves-ok-mg-def \\ \index{new-proc-preserves-ok-mg-def}
\=\+(\=\+{\rm{new-proc-name}}\,({\rm{car}}\,({\it{new-proc\/}}), {\it{pl\/}})\index{new-proc-name} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-def-plistp}}\,({\it{pl\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-def}}\,({\it{def\/}}, {\it{pl\/}})\index{ok-mg-def})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{ok-mg-def}}\,({\it{def\/}}, {\rm{cons}}\,({\it{new-proc\/}}, {\it{pl\/}}))\index{ok-mg-def}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  new-proc-preserves-ok-mg-def-plistp1 \\ \index{new-proc-preserves-ok-mg-def-pli!stp1}
\=\+(\=\+{\rm{new-proc-name}}\,({\rm{car}}\,({\it{new-proc\/}}), {\it{pl2\/}})\index{new-proc-name} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-def-plistp}}\,({\it{pl2\/}})\index{ok-mg-def-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{ok-mg-def-plistp1}}\,({\it{pl1\/}}, {\it{pl2\/}})\index{ok-mg-def-plistp1})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{ok-mg-def-plistp1}}\,({\it{pl1\/}}, {\rm{cons}}\,({\it{new-proc\/}}, {\it{pl2\/}}))\index{ok-mg-def-plistp1}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  make-alist-make-locals-list-preserves-signatures-match \\ \index{make-alist-make-locals-list-pre!serves-signatures-match}
\=\+{\rm{mg-alistp}}\,({\it{mg-alist\/}})\index{mg-alistp} \\ 
$\rightarrow$$\;\;\;\;${\rm{signatures-match}}\,(\=\+{\it{mg-alist\/}}, \\ 
{\rm{make-alist-from-formals}}\,({\rm{make-mg-locals-list}}\,({\it{mg-alist\/}})\index{make-mg-locals-list})\index{make-alist-from-formals})\-\index{signatures-match}\-
\end{tabbing}

\begin{verbatim};; To do this one I needed to change the hyp the cond-list is a cond-identifierp-plistp
;; to an identifier plistp.  

\end{verbatim}\begin{tabbing}{\sc Theorem}:  new-proc-preserves-ok-mg-def-plistp \\ \index{new-proc-preserves-ok-mg-def-pli!stp}
\=\+(\=\+{\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{cond-list\/}}, {\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-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-mg-statep}}\,({\it{mg-state\/}}, {\it{cond-list\/}})\index{ok-mg-statep} \\ 
$\wedge$$\;\;\;\;${\rm{identifier-plistp}}\,({\it{cond-list\/}})\index{identifier-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{new-proc-name}}\,({\it{subr\/}}, {\it{proc-list\/}})\index{new-proc-name} \\ 
$\wedge$$\;\;\;\;$({\rm{length}}\,({\it{cond-list\/}})\index{length} $<$ ((({\rm{exp}}\,({\tt{2}}, {\sc{mg-word-size}}\index{mg-word-size})\index{exp} $-\;1$) $-\;1$) $-\;1$)))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{ok-mg-def-plistp}}\,({\rm{cons}}\,(\=\+{\rm{make-mg-proc}}\,(\=\+{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, \\ 
{\it{subr\/}}, \\ 
{\it{stmt\/}}, \\ 
{\it{cond-list\/}})\-\index{make-mg-proc}, \\ 
{\it{proc-list\/}})\-)\index{ok-mg-def-plistp}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mg-to-p-simple-literal-list-listp \\ \index{mg-to-p-simple-literal-list-listp}
{\rm{listp}}\,({\rm{mg-to-p-simple-literal-list}}\,({\it{x\/}})\index{mg-to-p-simple-literal-list}) $=$ {\rm{listp}}\,({\it{x\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  initial-temp-stk-reversed-listp \\ \index{initial-temp-stk-reversed-listp}
({\rm{mg-alistp}}\,({\it{x\/}})\index{mg-alistp} $\wedge$ {\rm{listp}}\,({\it{x\/}})) $\rightarrow$ {\rm{listp}}\,({\rm{initial-temp-stk-reversed}}\,({\it{x\/}})\index{initial-temp-stk-reversed})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  length-initial-temp-stk-reversed \\ \index{length-initial-temp-stk-reverse!d}
\=\+{\rm{mg-alistp}}\,({\it{alist\/}})\index{mg-alistp} \\ 
$\rightarrow$$\;\;\;\;$({\rm{length}}\,({\rm{initial-temp-stk-reversed}}\,({\it{alist\/}})\index{initial-temp-stk-reversed})\index{length} $=$ {\rm{data-length}}\,({\it{alist\/}})\index{data-length})\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{initial-bindings-induction-hint} \\  
\=\+{\rm{initial-bindings-induction-hint}}\,({\it{mg-alist\/}}, {\it{n\/}}, {\it{lst\/}})\index{initial-bindings-induction-hint} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{mg-alist\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\rm{simple-mg-type-refp}}\,({\rm{cadar}}\,({\it{mg-alist\/}}))\index{simple-mg-type-refp} \\ 
{\bf then }{\rm{initial-bindings-induction-hint}}\,(\=\+{\rm{cdr}}\,({\it{mg-alist\/}}), \\ 
$1\;+$ {\it{n\/}}, \\ 
{\rm{cons}}\,(\=\+{\rm{mg-to-p-simple-literal}}\,({\rm{caddar}}\,({\it{mg-alist\/}}))\index{mg-to-p-simple-literal}, \\ 
{\it{lst\/}})\-)\-\index{initial-bindings-induction-hint} \\ 
{\bf else }{\rm{initial-bindings-induction-hint}}\,(\=\+{\rm{cdr}}\,({\it{mg-alist\/}}), \\ 
{\it{n\/}} $+$ {\rm{array-length}}\,({\rm{cadar}}\,({\it{mg-alist\/}}))\index{array-length}, \\ 
{\rm{append}}\,(\=\+{\rm{reverse}}\,({\rm{mg-to-p-simple-literal-list}}\,({\rm{caddar}}\,({\it{mg-alist\/}}))\index{mg-to-p-simple-literal-list})\index{reverse}, \\ 
{\it{lst\/}})\-)\-\index{initial-bindings-induction-hint}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  initial-bindings-ok-in-initial-temp-stk1 \\ \index{initial-bindings-ok-in-initial-te!mp-stk1}
\=\+({\rm{mg-alistp}}\,({\it{mg-alist\/}})\index{mg-alistp} $\wedge$ ({\it{n\/}} $=$ {\rm{length}}\,({\it{lst\/}})\index{length}) $\wedge$ {\rm{all-cars-unique}}\,({\it{mg-alist\/}})\index{all-cars-unique}) \\ 
$\rightarrow$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,(\=\+{\it{mg-alist\/}}, \\ 
{\rm{initial-bindings}}\,({\it{mg-alist\/}}, {\it{n\/}})\index{initial-bindings}, \\ 
{\rm{append}}\,({\rm{initial-temp-stk}}\,({\it{mg-alist\/}})\index{initial-temp-stk}, {\it{lst\/}}))\-\index{mg-vars-list-ok-in-p-state}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  initial-bindings-ok-in-initial-temp-stk \\ \index{initial-bindings-ok-in-initial-te!mp-stk}
\=\+({\rm{ok-mg-statep}}\,({\it{mg-state\/}}, {\it{cond-list\/}})\index{ok-mg-statep} $\wedge$ {\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique}) \\ 
$\rightarrow$$\;\;\;\;${\rm{mg-vars-list-ok-in-p-state}}\,(\=\+{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, \\ 
{\rm{initial-bindings}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, {\tt{0}})\index{initial-bindings}, \\ 
{\rm{initial-temp-stk}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{initial-temp-stk})\-\index{mg-vars-list-ok-in-p-state}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  initial-bindings-all-pointers-bigger \\ \index{initial-bindings-all-pointers-bi!gger}
\=\+{\rm{all-cars-unique}}\,({\it{alist\/}})\index{all-cars-unique} \\ 
$\rightarrow$$\;\;\;\;${\rm{all-pointers-bigger}}\,(\=\+{\rm{collect-pointers}}\,({\rm{initial-bindings}}\,({\it{alist\/}}, {\it{n\/}})\index{initial-bindings}, {\it{alist\/}})\index{collect-pointers}, \\ 
{\it{n\/}})\-\index{all-pointers-bigger}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  no-p-aliasing-in-initial-bindings \\ \index{no-p-aliasing-in-initial-bindin!gs}
\=\+({\rm{all-cars-unique}}\,({\it{mg-alist\/}})\index{all-cars-unique} $\wedge$ {\rm{mg-alistp}}\,({\it{mg-alist\/}})\index{mg-alistp} $\wedge$ ({\it{n\/}} $\in\;${\bf{N}}${}$)) \\ 
$\rightarrow$$\;\;\;\;${\rm{no-p-aliasing}}\,({\rm{initial-bindings}}\,({\it{mg-alist\/}}, {\it{n\/}})\index{initial-bindings}, {\it{mg-alist\/}})\index{no-p-aliasing}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  leave-not-state-cc \\ \index{leave-not-state-cc}
\=\+({\rm{ok-mg-statep}}\,({\it{mg-state\/}}, {\it{cond-list\/}})\index{ok-mg-statep} $\wedge$ {\rm{identifier-plistp}}\,({\it{cond-list\/}})\index{identifier-plistp}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{cc}}\,({\it{mg-state\/}})\index{cc} $\not=$ {\tt{'}}{\tt{leave}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  translation-is-correct3 \\ \index{translation-is-correct3}
\=\+(\=\+{\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{cond-list\/}}, {\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-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-mg-statep}}\,({\it{mg-state\/}}, {\it{cond-list\/}})\index{ok-mg-statep} \\ 
$\wedge$$\;\;\;\;${\rm{identifier-plistp}}\,({\it{cond-list\/}})\index{identifier-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{new-proc-name}}\,({\it{subr\/}}, {\it{proc-list\/}})\index{new-proc-name} \\ 
$\wedge$$\;\;\;\;$({\rm{length}}\,({\it{cond-list\/}})\index{length} $<$ ((({\rm{exp}}\,({\tt{2}}, {\sc{mg-word-size}}\index{mg-word-size})\index{exp} $-\;1$) $-\;1$) $-\;1$)) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resource-errorp}}\,({\rm{mg-meaning-r}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{length}}\,({\rm{initial-temp-stk}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{initial-temp-stk})\index{length}, \\ 
{\rm{p-ctrl-stk-size}}\,({\rm{list}}\,({\rm{cons}}\,(\=\+{\rm{initial-bindings}}\,(\=\+{\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist}, \\ 
{\tt{0}})\-\index{initial-bindings}, \\ 
{\rm{list}}\,({\rm{tag}}\,(\=\+{\tt{'}}{\tt{pc}}, \\ 
{\rm{cons}}\,(\=\+{\it{subr\/}}, \\ 
{\tt{0}})\-)\-\index{tag}))\-))\index{p-ctrl-stk-size})\-)\-\index{mg-meaning-r})\index{resource-errorp}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{map-up}}\,(\=\+{\rm{p}}\,(\=\+{\rm{map-down1}}\,({\it{mg-state\/}}, {\it{proc-list\/}}, {\it{cond-list\/}}, {\it{subr\/}}, {\it{stmt\/}})\index{map-down1}, \\ 
{\rm{clock}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}})\index{clock})\-\index{p}, \\ 
{\rm{signature}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{signature}, \\ 
{\it{cond-list\/}})\-\index{map-up} \\ 
$=$$\;\;\;\;${\rm{mg-meaning}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}})\index{mg-meaning})\-\-
\end{tabbing}

\begin{verbatim};; This is just a slightly cleaned up version of the previous lemma.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  translation-is-correct4 \\ \index{translation-is-correct4}
\=\+(\=\+{\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{cond-list\/}}, {\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-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-mg-statep}}\,({\it{mg-state\/}}, {\it{cond-list\/}})\index{ok-mg-statep} \\ 
$\wedge$$\;\;\;\;${\rm{identifier-plistp}}\,({\it{cond-list\/}})\index{identifier-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{new-proc-name}}\,({\it{subr\/}}, {\it{proc-list\/}})\index{new-proc-name} \\ 
$\wedge$$\;\;\;\;$({\rm{length}}\,({\it{cond-list\/}})\index{length} $<$ ((({\rm{exp}}\,({\tt{2}}, {\sc{mg-word-size}}\index{mg-word-size})\index{exp} $-\;1$) $-\;1$) $-\;1$)) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resource-errorp}}\,({\rm{mg-meaning-r}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{data-length}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{data-length}, \\ 
{\tt{2}} $+$ {\rm{length}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{length})\-)\-\index{mg-meaning-r})\index{resource-errorp}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{map-up}}\,(\=\+{\rm{p}}\,(\=\+{\rm{map-down1}}\,({\it{mg-state\/}}, {\it{proc-list\/}}, {\it{cond-list\/}}, {\it{subr\/}}, {\it{stmt\/}})\index{map-down1}, \\ 
{\rm{clock}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}})\index{clock})\-\index{p}, \\ 
{\rm{signature}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{signature}, \\ 
{\it{cond-list\/}})\-\index{map-up} \\ 
$=$$\;\;\;\;${\rm{mg-meaning}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}})\index{mg-meaning})\-\-
\end{tabbing}


\begin{tabbing}{\sc Definition}:\index{ok-execution-environment} \\  
\=\+{\rm{ok-execution-environment}}\,({\it{stmt\/}}, {\it{cond-list\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{subr\/}}, {\it{n\/}})\index{ok-execution-environment} \\ 
$=$$\;\;\;\;$(\=\+{\rm{ok-mg-statement}}\,({\it{stmt\/}}, {\it{cond-list\/}}, {\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-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-mg-statep}}\,({\it{mg-state\/}}, {\it{cond-list\/}})\index{ok-mg-statep} \\ 
$\wedge$$\;\;\;\;${\rm{identifier-plistp}}\,({\it{cond-list\/}})\index{identifier-plistp} \\ 
$\wedge$$\;\;\;\;${\rm{all-cars-unique}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{all-cars-unique} \\ 
$\wedge$$\;\;\;\;${\rm{new-proc-name}}\,({\it{subr\/}}, {\it{proc-list\/}})\index{new-proc-name} \\ 
$\wedge$$\;\;\;\;$({\rm{length}}\,({\it{cond-list\/}})\index{length} $<$ ((({\rm{exp}}\,({\tt{2}}, {\sc{mg-word-size}}\index{mg-word-size})\index{exp} $-\;1$) $-\;1$) $-\;1$)))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  translation-is-correct5 \\ \index{translation-is-correct5}
\=\+(\=\+{\rm{ok-execution-environment}}\,({\it{stmt\/}}, {\it{cond-list\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{subr\/}}, {\it{n\/}})\index{ok-execution-environment} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{resource-errorp}}\,({\rm{mg-meaning-r}}\,(\=\+{\it{stmt\/}}, \\ 
{\it{proc-list\/}}, \\ 
{\it{mg-state\/}}, \\ 
{\it{n\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{data-length}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{data-length}, \\ 
{\tt{2}} $+$ {\rm{length}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{length})\-)\-\index{mg-meaning-r})\index{resource-errorp}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{map-up}}\,(\=\+{\rm{p}}\,(\=\+{\rm{map-down1}}\,({\it{mg-state\/}}, {\it{proc-list\/}}, {\it{cond-list\/}}, {\it{subr\/}}, {\it{stmt\/}})\index{map-down1}, \\ 
{\rm{clock}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}})\index{clock})\-\index{p}, \\ 
{\rm{signature}}\,({\rm{mg-alist}}\,({\it{mg-state\/}})\index{mg-alist})\index{signature}, \\ 
{\it{cond-list\/}})\-\index{map-up} \\ 
$=$$\;\;\;\;${\rm{mg-meaning}}\,({\it{stmt\/}}, {\it{proc-list\/}}, {\it{mg-state\/}}, {\it{n\/}})\index{mg-meaning})\-\-
\end{tabbing}





\noindent{\sc Event}:   Make the library {\tt{"ca10"}}.

\addvspace{18pt}

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