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

\addvspace{18pt}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                             ;;
;;                   THE ASSEMBLY LANGUAGE                     ;;
;;                                                             ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; The fields of the p-state are to be interpreted as follows:
;;    pc is the 0-based program counter;
;;    temp-stk is a stack for moving variables and computing values
;;    ctrl-stk is a list of frames with the local variables;
;;    data-segment is a var alist of global variables 
;;    psw is 'run, 'halt, or some indication of error

\end{verbatim}
\noindent{\sc Event}:   Add the shell {\it{p-state\/}}\index{p-state}, with recognizer function symbol {\it{p-statep\/}} and 9 accessors: {\it{p-pc\/}}, with type restriction (none-of) and default value zero; {\it{p-ctrl-stk\/}}, with type restriction (none-of) and default value zero; {\it{p-temp-stk\/}}, with type restriction (none-of) and default value zero; {\it{p-prog-segment\/}}, with type restriction (none-of) and default value zero; {\it{p-data-segment\/}}, with type restriction (none-of) and default value zero; {\it{p-max-ctrl-stk-size\/}}, with type restriction (none-of) and default value zero; {\it{p-max-temp-stk-size\/}}, with type restriction (none-of) and default value zero; {\it{p-word-size\/}}, with type restriction (none-of) and default value zero; {\it{p-psw\/}}, with type restriction (none-of) and default value zero.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{p-halt} \\  
\=\+{\rm{p-halt}}\,({\it{p\/}}, {\it{psw\/}})\index{p-halt} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{p-pc}}\,({\it{p\/}})\index{p-pc}, \\ 
{\rm{p-ctrl-stk}}\,({\it{p\/}})\index{p-ctrl-stk}, \\ 
{\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk}, \\ 
{\rm{p-prog-segment}}\,({\it{p\/}})\index{p-prog-segment}, \\ 
{\rm{p-data-segment}}\,({\it{p\/}})\index{p-data-segment}, \\ 
{\rm{p-max-ctrl-stk-size}}\,({\it{p\/}})\index{p-max-ctrl-stk-size}, \\ 
{\rm{p-max-temp-stk-size}}\,({\it{p\/}})\index{p-max-temp-stk-size}, \\ 
{\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size}, \\ 
{\it{psw\/}})\-\index{p-state}\-
\end{tabbing}

\begin{verbatim};;(defn errorp (psw)
;;  (and (not (equal psw 'run))
;;       (not (equal psw 'halt))))

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{definition}$\;\;$
{\rm{definition}}\,({\it{name\/}}, {\it{alist\/}})\index{definition} $=$ {\rm{assoc}}\,({\it{name\/}}, {\it{alist\/}})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{put-value} \\  
{\rm{put-value}}\,({\it{val\/}}, {\it{name\/}}, {\it{alist\/}})\index{put-value} $=$ {\rm{put-assoc}}\,({\it{val\/}}, {\it{name\/}}, {\it{alist\/}})\index{put-assoc}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{formal-vars}$\;\;$
{\rm{formal-vars}}\,({\it{d\/}})\index{formal-vars} $=$ {\rm{cadr}}\,({\it{d\/}})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{temp-var-dcls}$\;\;$
{\rm{temp-var-dcls}}\,({\it{d\/}})\index{temp-var-dcls} $=$ {\rm{caddr}}\,({\it{d\/}})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{program-body}$\;\;$
{\rm{program-body}}\,({\it{d\/}})\index{program-body} $=$ {\rm{cdddr}}\,({\it{d\/}})
\end{tabbing}

\begin{verbatim};;(defn local-vars (d) (append (formal-vars d) (listcars (temp-var-dcls d))))

;; Addresses are tagged "address pairs".  This differs from the earlier formulation
;; in having to worry about the tags.  Thus the pc is now (pc (subr . foo)).

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{adp-name}$\;\;$
{\rm{adp-name}}\,({\it{adp\/}})\index{adp-name} $=$ {\rm{car}}\,({\it{adp\/}})
\end{tabbing}


\noindent{\sc Event}:   Disable adp-name.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{adp-offset}$\;\;$
{\rm{adp-offset}}\,({\it{adp\/}})\index{adp-offset} $=$ {\rm{cdr}}\,({\it{adp\/}})
\end{tabbing}


\noindent{\sc Event}:   Disable adp-offset.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  adp-name-cons \\ \index{adp-name-cons}
{\rm{adp-name}}\,({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}))\index{adp-name} $=$ {\it{x\/}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  adp-offset-cons \\ \index{adp-offset-cons}
{\rm{adp-offset}}\,({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}))\index{adp-offset} $=$ {\it{y\/}}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{adpp} \\  
\=\+{\rm{adpp}}\,({\it{x\/}}, {\it{segment\/}})\index{adpp} \\ 
$=$$\;\;\;\;$(\=\+{\rm{listp}}\,({\it{x\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{adp-offset}}\,({\it{x\/}})\index{adp-offset} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{definedp}}\,({\rm{adp-name}}\,({\it{x\/}})\index{adp-name}, {\it{segment\/}})\index{definedp} \\ 
$\wedge$$\;\;\;\;$({\rm{adp-offset}}\,({\it{x\/}})\index{adp-offset} $<$ {\rm{length}}\,({\rm{value}}\,({\rm{adp-name}}\,({\it{x\/}})\index{adp-name}, {\it{segment\/}})\index{value})\index{length}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{pcpp} \\  
\=\+{\rm{pcpp}}\,({\it{x\/}}, {\it{segment\/}})\index{pcpp} \\ 
$=$$\;\;\;\;$(\=\+{\rm{listp}}\,({\it{x\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{adp-offset}}\,({\it{x\/}})\index{adp-offset} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{definedp}}\,({\rm{adp-name}}\,({\it{x\/}})\index{adp-name}, {\it{segment\/}})\index{definedp} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{adp-offset}}\,({\it{x\/}})\index{adp-offset} \\ 
$<$$\;\;\;\;${\rm{length}}\,({\rm{program-body}}\,({\rm{definition}}\,({\rm{adp-name}}\,({\it{x\/}})\index{adp-name}, {\it{segment\/}})\index{definition})\index{program-body})\index{length})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{add-adp} \\  
{\rm{add-adp}}\,({\it{adp\/}}, {\it{n\/}})\index{add-adp} $=$ {\rm{cons}}\,({\rm{adp-name}}\,({\it{adp\/}})\index{adp-name}, {\rm{adp-offset}}\,({\it{adp\/}})\index{adp-offset} $+$ {\it{n\/}})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{add1-adp}$\;\;$
{\rm{add1-adp}}\,({\it{adp\/}})\index{add1-adp} $=$ {\rm{add-adp}}\,({\it{adp\/}}, {\tt{1}})\index{add-adp}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{sub-adp} \\  
{\rm{sub-adp}}\,({\it{adp\/}}, {\it{n\/}})\index{sub-adp} $=$ {\rm{cons}}\,({\rm{adp-name}}\,({\it{adp\/}})\index{adp-name}, {\rm{adp-offset}}\,({\it{adp\/}})\index{adp-offset} $-$ {\it{n\/}})
\end{tabbing}

\begin{verbatim};;(defn sub1-adp (adp) (sub-adp adp 1))
;;
;;(defn add1-adp-adpp (x segment)
;;      (adpp (add1-adp x) segment))
;;
;;(defn add-adp-adpp (x n segment)
;;      (adpp (add-adp x n) segment))

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{fetch-adp} \\  
\=\+{\rm{fetch-adp}}\,({\it{adp\/}}, {\it{segment\/}})\index{fetch-adp} \\ 
$=$$\;\;\;\;${\rm{get}}\,({\rm{adp-offset}}\,({\it{adp\/}})\index{adp-offset}, {\rm{value}}\,({\rm{adp-name}}\,({\it{adp\/}})\index{adp-name}, {\it{segment\/}})\index{value})\index{get}\-
\end{tabbing}

\begin{verbatim};; Puts val in the named segment at addr.  

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{deposit-adp} \\  
\=\+{\rm{deposit-adp}}\,({\it{val\/}}, {\it{adp\/}}, {\it{segment\/}})\index{deposit-adp} \\ 
$=$$\;\;\;\;${\rm{put-value}}\,(\=\+{\rm{put}}\,({\it{val\/}}, {\rm{adp-offset}}\,({\it{adp\/}})\index{adp-offset}, {\rm{value}}\,({\rm{adp-name}}\,({\it{adp\/}})\index{adp-name}, {\it{segment\/}})\index{value})\index{put}, \\ 
{\rm{adp-name}}\,({\it{adp\/}})\index{adp-name}, \\ 
{\it{segment\/}})\-\index{put-value}\-
\end{tabbing}

\begin{verbatim};; These two functions are the analogues of get and put counting from
;; the right.  They are used in the definition of fetch and deposit on the
;; temp-stk.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{rget}$\;\;$
{\rm{rget}}\,({\it{n\/}}, {\it{lst\/}})\index{rget} $=$ {\rm{get}}\,(({\rm{length}}\,({\it{lst\/}})\index{length} $-$ {\it{n\/}}) $-\;1$, {\it{lst\/}})\index{get}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{rput} \\  
{\rm{rput}}\,({\it{val\/}}, {\it{n\/}}, {\it{lst\/}})\index{rput} $=$ {\rm{put}}\,({\it{val\/}}, ({\rm{length}}\,({\it{lst\/}})\index{length} $-$ {\it{n\/}}) $-\;1$, {\it{lst\/}})\index{put}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  rput-preserves-length \\ \index{rput-preserves-length}
({\it{y\/}} $<$ {\rm{length}}\,({\it{z\/}})\index{length}) $\rightarrow$ ({\rm{length}}\,({\rm{rput}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{rput})\index{length} $=$ {\rm{length}}\,({\it{z\/}})\index{length})
\end{tabbing}


\noindent{\sc Event}:   Disable rget.

\addvspace{18pt}

\noindent{\sc Event}:   Disable rput.

\addvspace{18pt}

\begin{verbatim};; Tagged objects
;; All Piton objects are tagged with their "type".  The form is (tag obj)

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{tag}$\;\;$
{\rm{tag}}\,({\it{type\/}}, {\it{obj\/}})\index{tag} $=$ {\rm{list}}\,({\it{type\/}}, {\it{obj\/}})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{type}$\;\;$
{\rm{type}}\,({\it{const\/}})\index{type} $=$ {\rm{car}}\,({\it{const\/}})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{untag}$\;\;$
{\rm{untag}}\,({\it{const\/}})\index{untag} $=$ {\rm{cadr}}\,({\it{const\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  type-expansion \\ \index{type-expansion}
{\rm{type}}\,({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}))\index{type} $=$ {\it{x\/}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  type-tag \\ \index{type-tag}
{\rm{type}}\,({\rm{tag}}\,({\it{x\/}}, {\it{y\/}})\index{tag})\index{type} $=$ {\it{x\/}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  untag-tag \\ \index{untag-tag}
{\rm{untag}}\,({\rm{tag}}\,({\it{x\/}}, {\it{y\/}})\index{tag})\index{untag} $=$ {\it{y\/}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  untag-cons \\ \index{untag-cons}
{\rm{untag}}\,({\rm{list}}\,({\it{x\/}}, {\it{y\/}}))\index{untag} $=$ {\it{y\/}}
\end{tabbing}

\begin{verbatim};;(prove-lemma tag-length-2 (rewrite)
;;      (equal (cddr (tag x y)) nil)
;;     ((enable tag)))

\end{verbatim}
\noindent{\sc Event}:   Disable type.

\addvspace{18pt}

\noindent{\sc Event}:   Disable tag.

\addvspace{18pt}

\noindent{\sc Event}:   Disable untag.

\addvspace{18pt}

\begin{verbatim};; Tagged addresses

;;(defn addressp (x segment) (adpp (untag x) segment))

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{area-name}$\;\;$
{\rm{area-name}}\,({\it{x\/}})\index{area-name} $=$ {\rm{adp-name}}\,({\rm{untag}}\,({\it{x\/}})\index{untag})\index{adp-name}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{offset}$\;\;$
{\rm{offset}}\,({\it{x\/}})\index{offset} $=$ {\rm{adp-offset}}\,({\rm{untag}}\,({\it{x\/}})\index{untag})\index{adp-offset}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{add-addr} \\  
{\rm{add-addr}}\,({\it{addr\/}}, {\it{n\/}})\index{add-addr} $=$ {\rm{tag}}\,({\rm{type}}\,({\it{addr\/}})\index{type}, {\rm{add-adp}}\,({\rm{untag}}\,({\it{addr\/}})\index{untag}, {\it{n\/}})\index{add-adp})\index{tag}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{add1-addr}$\;\;$
{\rm{add1-addr}}\,({\it{addr\/}})\index{add1-addr} $=$ {\rm{add-addr}}\,({\it{addr\/}}, {\tt{1}})\index{add-addr}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{sub-addr} \\  
{\rm{sub-addr}}\,({\it{addr\/}}, {\it{n\/}})\index{sub-addr} $=$ {\rm{tag}}\,({\rm{type}}\,({\it{addr\/}})\index{type}, {\rm{sub-adp}}\,({\rm{untag}}\,({\it{addr\/}})\index{untag}, {\it{n\/}})\index{sub-adp})\index{tag}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{sub1-addr}$\;\;$
{\rm{sub1-addr}}\,({\it{addr\/}})\index{sub1-addr} $=$ {\rm{sub-addr}}\,({\it{addr\/}}, {\tt{1}})\index{sub-addr}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{fetch} \\  
{\rm{fetch}}\,({\it{addr\/}}, {\it{segment\/}})\index{fetch} $=$ {\rm{fetch-adp}}\,({\rm{untag}}\,({\it{addr\/}})\index{untag}, {\it{segment\/}})\index{fetch-adp}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{deposit} \\  
{\rm{deposit}}\,({\it{val\/}}, {\it{addr\/}}, {\it{segment\/}})\index{deposit} $=$ {\rm{deposit-adp}}\,({\it{val\/}}, {\rm{untag}}\,({\it{addr\/}})\index{untag}, {\it{segment\/}})\index{deposit-adp}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{add1-nat}$\;\;$
{\rm{add1-nat}}\,({\it{nat\/}})\index{add1-nat} $=$ {\rm{tag}}\,({\tt{'}}{\tt{nat}}, $1\;+$ {\rm{untag}}\,({\it{nat\/}})\index{untag})\index{tag}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  untag-add1-nat \\ \index{untag-add1-nat}
{\rm{untag}}\,({\rm{add1-nat}}\,({\it{nat\/}})\index{add1-nat})\index{untag} $=$ ($1\;+$ {\rm{untag}}\,({\it{nat\/}})\index{untag})
\end{tabbing}

\begin{verbatim};; Booleans 
;; Piton uses the litatoms 't and 'f for the truth values.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{booleanp}$\;\;$
{\rm{booleanp}}\,({\it{x\/}})\index{booleanp} $=$ (({\it{x\/}} $=$ {\tt{'}}{\tt{t}}) $\vee$ ({\it{x\/}} $=$ {\tt{'}}{\tt{f}}))
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{bool} \\  
\=\+{\rm{bool}}\,({\it{x\/}})\index{bool} \\ 
$=$$\;\;\;\;${\rm{tag}}\,(\=\+{\tt{'}}{\tt{bool}}, \\ 
\=\+{\bf if }{\it{x\/}}$\;\;${\bf then }{\tt{'}}{\tt{t}} \\ 
{\bf else }{\tt{'}}{\tt{f}}$\;${\bf  endif}\-)\-\index{tag}\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{or-bool} \\  
\=\+{\rm{or-bool}}\,({\it{x\/}}, {\it{y\/}})\index{or-bool} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $=$ {\tt{'}}{\tt{f}}$\;\;${\bf then }{\it{y\/}} \\ 
{\bf else }{\tt{'}}{\tt{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{and-bool} \\  
\=\+{\rm{and-bool}}\,({\it{x\/}}, {\it{y\/}})\index{and-bool} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $=$ {\tt{'}}{\tt{f}}$\;\;${\bf then }{\tt{'}}{\tt{f}} \\ 
{\bf else }{\it{y\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{not-bool} \\  
\=\+{\rm{not-bool}}\,({\it{x\/}})\index{not-bool} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $=$ {\tt{'}}{\tt{f}}$\;\;${\bf then }{\tt{'}}{\tt{t}} \\ 
{\bf else }{\tt{'}}{\tt{f}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};; Naturals
;; Notice that, where full Piton allows word-size to be a parameter, I am making it
;; a constant.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{small-naturalp} \\  
{\rm{small-naturalp}}\,({\it{i\/}}, {\it{word-size\/}})\index{small-naturalp} $=$ (({\it{i\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{i\/}} $<$ {\rm{exp}}\,({\tt{2}}, {\it{word-size\/}})\index{exp}))
\end{tabbing}


\noindent{\sc Event}:   Disable small-naturalp.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{bool-to-nat} \\  
\=\+{\rm{bool-to-nat}}\,({\it{flg\/}})\index{bool-to-nat} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{flg\/}} $=$ {\tt{'}}{\tt{f}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\tt{1}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};; Integers
;; These functions are defined so that if given integerps they return integerps.
;; In particular, they never return (minus 0) though they may pass one through.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{small-integerp} \\  
\=\+{\rm{small-integerp}}\,({\it{i\/}}, {\it{word-size\/}})\index{small-integerp} \\ 
$=$$\;\;\;\;$(\=\+{\rm{integerp}}\,({\it{i\/}})\index{integerp} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,({\it{i\/}}, $-$ {\rm{exp}}\,({\tt{2}}, {\it{word-size\/}} $-\;1$)\index{exp})\index{ilessp}) \\ 
$\wedge$$\;\;\;\;${\rm{ilessp}}\,({\it{i\/}}, {\rm{exp}}\,({\tt{2}}, {\it{word-size\/}} $-\;1$)\index{exp})\index{ilessp})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable small-integerp.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{fix-small-integer} \\  
\=\+{\rm{fix-small-integer}}\,({\it{i\/}}, {\it{word-size\/}})\index{fix-small-integer} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{small-integerp}}\,({\it{i\/}}, {\it{word-size\/}})\index{small-integerp}$\;\;${\bf then }{\it{i\/}} \\ 
{\bf elseif }{\rm{negativep}}\,({\it{i\/}})$\;\;${\bf then }{\rm{iplus}}\,({\it{i\/}}, {\rm{exp}}\,({\tt{2}}, {\it{word-size\/}})\index{exp})\index{iplus} \\ 
{\bf else }{\rm{iplus}}\,({\it{i\/}}, $-$ {\rm{exp}}\,({\tt{2}}, {\it{word-size\/}})\index{exp})\index{iplus}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};; I don't currently know which Piton integer ops I'll need on integers so I'm 
;; leaving these out.

;; stacks

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{push}$\;\;$
{\rm{push}}\,({\it{x\/}}, {\it{stk\/}})\index{push} $=$ {\rm{cons}}\,({\it{x\/}}, {\it{stk\/}})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{top}$\;\;$
{\rm{top}}\,({\it{stk\/}})\index{top} $=$ {\rm{car}}\,({\it{stk\/}})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{pop}$\;\;$
{\rm{pop}}\,({\it{stk\/}})\index{pop} $=$ {\rm{cdr}}\,({\it{stk\/}})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{popn} \\  
\=\+{\rm{popn}}\,({\it{n\/}}, {\it{x\/}})\index{popn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\it{x\/}} \\ 
{\bf else }{\rm{popn}}\,({\it{n\/}} $-\;1$, {\rm{cdr}}\,({\it{x\/}}))\index{popn}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  popn-add1 \\ \index{popn-add1}
\=\+({\rm{popn}}\,($1\;+$ {\it{n\/}}, {\rm{push}}\,({\it{x\/}}, {\it{y\/}})\index{push})\index{popn} $=$ {\rm{popn}}\,({\it{n\/}}, {\it{y\/}})\index{popn}) \\ 
$\wedge$$\;\;\;\;$({\rm{popn}}\,($1\;+$ {\it{n\/}}, {\rm{cons}}\,({\it{x\/}}, {\it{y\/}}))\index{popn} $=$ {\rm{popn}}\,({\it{n\/}}, {\it{y\/}})\index{popn})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  popn-zero \\ \index{popn-zero}
{\rm{popn}}\,({\tt{0}}, {\it{x\/}})\index{popn} $=$ {\it{x\/}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  popn-length \\ \index{popn-length}
({\it{n\/}} $=$ {\rm{length}}\,({\it{lst\/}})\index{length}) $\rightarrow$ ({\rm{popn}}\,({\it{n\/}}, {\rm{append}}\,({\it{lst\/}}, {\it{stk\/}}))\index{popn} $=$ {\it{stk\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  popn-plus \\ \index{popn-plus}
({\it{m\/}} $=$ {\rm{length}}\,({\it{lst1\/}})\index{length}) $\rightarrow$ ({\rm{popn}}\,({\it{m\/}} $+$ {\it{n\/}}, {\rm{append}}\,({\it{lst1\/}}, {\it{lst2\/}}))\index{popn} $=$ {\rm{popn}}\,({\it{n\/}}, {\it{lst2\/}})\index{popn})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{top1}$\;\;$
{\rm{top1}}\,({\it{stk\/}})\index{top1} $=$ {\rm{top}}\,({\rm{pop}}\,({\it{stk\/}})\index{pop})\index{top}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{top2}$\;\;$
{\rm{top2}}\,({\it{stk\/}})\index{top2} $=$ {\rm{top}}\,({\rm{pop}}\,({\rm{pop}}\,({\it{stk\/}})\index{pop})\index{pop})\index{top}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  pop-push \\ \index{pop-push}
{\rm{pop}}\,({\rm{push}}\,({\it{x\/}}, {\it{y\/}})\index{push})\index{pop} $=$ {\it{y\/}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  pop-cons \\ \index{pop-cons}
{\rm{pop}}\,({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}))\index{pop} $=$ {\it{y\/}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  car-cdr-push \\ \index{car-cdr-push}
({\rm{car}}\,({\rm{push}}\,({\it{x\/}}, {\it{y\/}})\index{push}) $=$ {\it{x\/}}) $\wedge$ ({\rm{cdr}}\,({\rm{push}}\,({\it{x\/}}, {\it{y\/}})\index{push}) $=$ {\it{y\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  push-listp \\ \index{push-listp}
{\rm{listp}}\,({\rm{push}}\,({\it{x\/}}, {\it{y\/}})\index{push}) $\wedge$ (({\rm{push}}\,({\it{x\/}}, {\it{y\/}})\index{push} $\simeq\;${{\bf{nil}}}${}$) $=$ {\bf{f}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  top-push \\ \index{top-push}
{\rm{top}}\,({\rm{push}}\,({\it{x\/}}, {\it{y\/}})\index{push})\index{top} $=$ {\it{x\/}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  top1-push \\ \index{top1-push}
{\rm{top1}}\,({\rm{push}}\,({\it{x\/}}, {\rm{push}}\,({\it{y\/}}, {\it{z\/}})\index{push})\index{push})\index{top1} $=$ {\it{y\/}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  top2-push \\ \index{top2-push}
{\rm{top2}}\,({\rm{push}}\,({\it{x\/}}, {\rm{push}}\,({\it{y\/}}, {\rm{push}}\,({\it{z\/}}, {\it{w\/}})\index{push})\index{push})\index{push})\index{top2} $=$ {\it{z\/}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  length-push \\ \index{length-push}
{\rm{length}}\,({\rm{push}}\,({\it{x\/}}, {\it{y\/}})\index{push})\index{length} $=$ ($1\;+$ {\rm{length}}\,({\it{y\/}})\index{length})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  top-cons \\ \index{top-cons}
{\rm{top}}\,({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}))\index{top} $=$ {\it{x\/}}
\end{tabbing}

\begin{verbatim};;(prove-lemma top1-cons (rewrite)
;;      (equal (top1 (cons x (cons y z))) y))
;;
;;(prove-lemma top2-cons (rewrite)
;;      (equal (top2 (cons x (cons y (cons z w)))) z))

\end{verbatim}
\noindent{\sc Event}:   Disable pop.

\addvspace{18pt}

\noindent{\sc Event}:   Disable push.

\addvspace{18pt}

\noindent{\sc Event}:   Disable top.

\addvspace{18pt}

\noindent{\sc Event}:   Disable top1.

\addvspace{18pt}

\noindent{\sc Event}:   Disable top2.

\addvspace{18pt}

\noindent{\sc Event}:   Disable popn.

\addvspace{18pt}

\begin{verbatim};; Labels 
;; Notice that labelled instructions now have comments associated with them.

;;(defn dl (lab comment ins) (list 'dl lab comment ins))

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{labelledp}$\;\;$
{\rm{labelledp}}\,({\it{x\/}})\index{labelledp} $=$ ({\rm{car}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{dl}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  labelledp-expansion \\ \index{labelledp-expansion}
{\rm{labelledp}}\,({\rm{cons}}\,({\tt{'}}{\tt{dl}}, {\it{args\/}}))\index{labelledp} $=$ {\bf{t}}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{unlabel} \\  
\=\+{\rm{unlabel}}\,({\it{x\/}})\index{unlabel} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{labelledp}}\,({\it{x\/}})\index{labelledp}$\;\;${\bf then }{\rm{cadddr}}\,({\it{x\/}}) \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  unlabel-expansion \\ \index{unlabel-expansion}
{\rm{unlabel}}\,({\rm{cons}}\,({\tt{'}}{\tt{dl}}, {\it{args\/}}))\index{unlabel} $=$ {\rm{caddr}}\,({\it{args\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  unlabel-unlabelledp \\ \index{unlabel-unlabelledp}
({\it{x\/}} $\not=$ {\tt{'}}{\tt{dl}}) $\rightarrow$ ({\rm{unlabel}}\,({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}))\index{unlabel} $=$ {\rm{cons}}\,({\it{x\/}}, {\it{y\/}}))
\end{tabbing}


\noindent{\sc Event}:   Disable unlabel.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{find-labelp} \\  
\=\+{\rm{find-labelp}}\,({\it{x\/}}, {\it{lst\/}})\index{find-labelp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{lst\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{f}} \\ 
{\bf elseif }{\rm{labelledp}}\,({\rm{car}}\,({\it{lst\/}}))\index{labelledp} $\wedge$ ({\it{x\/}} $=$ {\rm{cadr}}\,({\rm{car}}\,({\it{lst\/}})))$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{find-labelp}}\,({\it{x\/}}, {\rm{cdr}}\,({\it{lst\/}}))\index{find-labelp}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};; This function counts the number of items in the list before the first one
;; labelled with x.  This is my get-pc function.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{find-label} \\  
\=\+{\rm{find-label}}\,({\it{x\/}}, {\it{lst\/}})\index{find-label} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{lst\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\rm{labelledp}}\,({\rm{car}}\,({\it{lst\/}}))\index{labelledp} $\wedge$ ({\it{x\/}} $=$ {\rm{cadr}}\,({\rm{car}}\,({\it{lst\/}})))$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }$1\;+$ {\rm{find-label}}\,({\it{x\/}}, {\rm{cdr}}\,({\it{lst\/}}))\index{find-label}$\;${\bf  endif}\-\-
\end{tabbing}


\begin{verbatim};;(defn all-find-labelp (lab-lst lst)
;;  (if (nlistp lab-lst)
;;      t
;;      (and (find-labelp (car lab-lst) lst)
;;           (all-find-labelp (cdr lab-lst) lst))))

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{pc} \\  
\=\+{\rm{pc}}\,({\it{label\/}}, {\it{program\/}})\index{pc} \\ 
$=$$\;\;\;\;${\rm{tag}}\,({\tt{'}}{\tt{pc}}, {\rm{cons}}\,({\rm{car}}\,({\it{program\/}}), {\rm{find-label}}\,({\it{label\/}}, {\rm{program-body}}\,({\it{program\/}})\index{program-body})\index{find-label}))\index{tag}\-
\end{tabbing}

\begin{verbatim};; Piton primitive objects

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{p-objectp} \\  
\=\+{\rm{p-objectp}}\,({\it{x\/}}, {\it{p\/}})\index{p-objectp} \\ 
$=$$\;\;\;\;$(\=\+{\rm{listp}}\,({\it{x\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{cddr}}\,({\it{x\/}}) $=$ {\bf{nil}}) \\ 
$\wedge$$\;\;\;\;$\=\+{\bf case on }{\rm{type}}\,({\it{x\/}})\index{type}: \\ 
{\bf case = }{\it{nat\/}} \\ 
{\bf then }{\rm{small-naturalp}}\,({\rm{untag}}\,({\it{x\/}})\index{untag}, {\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size})\index{small-naturalp} \\ 
{\bf case = }{\it{int\/}} \\ 
{\bf $\;\;$then }{\rm{small-integerp}}\,({\rm{untag}}\,({\it{x\/}})\index{untag}, {\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size})\index{small-integerp} \\ 
{\bf case = }{\it{bool\/}} \\ 
{\bf $\;\;$then }{\rm{booleanp}}\,({\rm{untag}}\,({\it{x\/}})\index{untag})\index{booleanp} \\ 
{\bf case = }{\it{addr\/}} \\ 
{\bf $\;\;$then }{\rm{adpp}}\,({\rm{untag}}\,({\it{x\/}})\index{untag}, {\rm{p-data-segment}}\,({\it{p\/}})\index{p-data-segment})\index{adpp} \\ 
{\bf case = }{\it{pc\/}} \\ 
{\bf $\;\;$then }{\rm{pcpp}}\,({\rm{untag}}\,({\it{x\/}})\index{untag}, {\rm{p-prog-segment}}\,({\it{p\/}})\index{p-prog-segment})\index{pcpp} \\ 
{\bf case = }{\it{subr\/}} \\ 
{\bf $\;\;$then }{\rm{definedp}}\,({\rm{untag}}\,({\it{x\/}})\index{untag}, {\rm{p-prog-segment}}\,({\it{p\/}})\index{p-prog-segment})\index{definedp} \\ 
{\bf otherwise }{\bf{f}}$\;${\bf  endcase}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-objectp-type} \\  
{\rm{p-objectp-type}}\,({\it{type\/}}, {\it{x\/}}, {\it{p\/}})\index{p-objectp-type} $=$ (({\rm{type}}\,({\it{x\/}})\index{type} $=$ {\it{type\/}}) $\wedge$ {\rm{p-objectp}}\,({\it{x\/}}, {\it{p\/}})\index{p-objectp})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{add1-p-pc}$\;\;$
{\rm{add1-p-pc}}\,({\it{p\/}})\index{add1-p-pc} $=$ {\rm{add1-addr}}\,({\rm{p-pc}}\,({\it{p\/}})\index{p-pc})\index{add1-addr}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-current-program} \\  
{\rm{p-current-program}}\,({\it{p\/}})\index{p-current-program} $=$ {\rm{definition}}\,({\rm{area-name}}\,({\rm{p-pc}}\,({\it{p\/}})\index{p-pc})\index{area-name}, {\rm{p-prog-segment}}\,({\it{p\/}})\index{p-prog-segment})\index{definition}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-current-instruction} \\  
\=\+{\rm{p-current-instruction}}\,({\it{p\/}})\index{p-current-instruction} \\ 
$=$$\;\;\;\;${\rm{unlabel}}\,({\rm{get}}\,({\rm{offset}}\,({\rm{p-pc}}\,({\it{p\/}})\index{p-pc})\index{offset}, {\rm{program-body}}\,({\rm{p-current-program}}\,({\it{p\/}})\index{p-current-program})\index{program-body})\index{get})\index{unlabel}\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-frame}$\;\;$
{\rm{p-frame}}\,({\it{bindings\/}}, {\it{ret-pc\/}})\index{p-frame} $=$ {\rm{list}}\,({\it{bindings\/}}, {\it{ret-pc\/}})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{bindings}$\;\;$
{\rm{bindings}}\,({\it{frame\/}})\index{bindings} $=$ {\rm{car}}\,({\it{frame\/}})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{ret-pc}$\;\;$
{\rm{ret-pc}}\,({\it{frame\/}})\index{ret-pc} $=$ {\rm{cadr}}\,({\it{frame\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  bindings-frame \\ \index{bindings-frame}
({\rm{bindings}}\,({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}))\index{bindings} $=$ {\it{x\/}}) $\wedge$ ({\rm{bindings}}\,({\rm{p-frame}}\,({\it{x\/}}, {\it{y\/}})\index{p-frame})\index{bindings} $=$ {\it{x\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ret-pc-frame \\ \index{ret-pc-frame}
({\rm{ret-pc}}\,({\rm{list}}\,({\it{x\/}}, {\it{y\/}}))\index{ret-pc} $=$ {\it{y\/}}) $\wedge$ ({\rm{ret-pc}}\,({\rm{p-frame}}\,({\it{x\/}}, {\it{y\/}})\index{p-frame})\index{ret-pc} $=$ {\it{y\/}})
\end{tabbing}


\noindent{\sc Event}:   Disable p-frame.

\addvspace{18pt}

\noindent{\sc Event}:   Disable bindings.

\addvspace{18pt}

\noindent{\sc Event}:   Disable ret-pc.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{p-frame-size} \\  
{\rm{p-frame-size}}\,({\it{frame\/}})\index{p-frame-size} $=$ ({\tt{2}} $+$ {\rm{length}}\,({\rm{bindings}}\,({\it{frame\/}})\index{bindings})\index{length})
\end{tabbing}


\noindent{\sc Event}:   Disable p-frame-size.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{p-ctrl-stk-size} \\  
\=\+{\rm{p-ctrl-stk-size}}\,({\it{ctrl-stk\/}})\index{p-ctrl-stk-size} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{ctrl-stk\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }\=\+{\rm{p-frame-size}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{p-frame-size} \\ 
$+$$\;\;\;\;${\rm{p-ctrl-stk-size}}\,({\rm{cdr}}\,({\it{ctrl-stk\/}}))\index{p-ctrl-stk-size}\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};;(defn local-varp (var ctrl-stk)
;;  (definedp var (bindings (top ctrl-stk))))

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{local-var-value} \\  
{\rm{local-var-value}}\,({\it{var\/}}, {\it{ctrl-stk\/}})\index{local-var-value} $=$ {\rm{value}}\,({\it{var\/}}, {\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\index{value}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{set-local-var-value} \\  
\=\+{\rm{set-local-var-value}}\,({\it{val\/}}, {\it{var\/}}, {\it{ctrl-stk\/}})\index{set-local-var-value} \\ 
$=$$\;\;\;\;${\rm{push}}\,(\=\+{\rm{p-frame}}\,(\=\+{\rm{put-value}}\,({\it{val\/}}, {\it{var\/}}, {\rm{bindings}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{bindings})\index{put-value}, \\ 
{\rm{ret-pc}}\,({\rm{top}}\,({\it{ctrl-stk\/}})\index{top})\index{ret-pc})\-\index{p-frame}, \\ 
{\rm{pop}}\,({\it{ctrl-stk\/}})\index{pop})\-\index{push}\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{first-n} \\  
\=\+{\rm{first-n}}\,({\it{n\/}}, {\it{x\/}})\index{first-n} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{cons}}\,({\rm{car}}\,({\it{x\/}}), {\rm{first-n}}\,({\it{n\/}} $-\;1$, {\rm{cdr}}\,({\it{x\/}}))\index{first-n})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  first-n-add1 \\ \index{first-n-add1}
\=\+({\rm{first-n}}\,($1\;+$ {\it{n\/}}, {\rm{push}}\,({\it{x\/}}, {\it{y\/}})\index{push})\index{first-n} $=$ {\rm{cons}}\,({\it{x\/}}, {\rm{first-n}}\,({\it{n\/}}, {\it{y\/}})\index{first-n})) \\ 
$\wedge$$\;\;\;\;$({\rm{first-n}}\,($1\;+$ {\it{n\/}}, {\rm{cons}}\,({\it{x\/}}, {\it{y\/}}))\index{first-n} $=$ {\rm{cons}}\,({\it{x\/}}, {\rm{first-n}}\,({\it{n\/}}, {\it{y\/}})\index{first-n})) \\ 
$\wedge$$\;\;\;\;$({\rm{first-n}}\,({\tt{0}}, {\it{y\/}})\index{first-n} $=$ {\bf{nil}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  first-n-plus-append \\ \index{first-n-plus-append}
\=\+({\it{n\/}} $=$ {\rm{length}}\,({\it{lst1\/}})\index{length}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{first-n}}\,({\it{n\/}} $+$ {\it{m\/}}, {\rm{append}}\,({\it{lst1\/}}, {\it{lst2\/}}))\index{first-n} $=$ {\rm{append}}\,({\it{lst1\/}}, {\rm{first-n}}\,({\it{m\/}}, {\it{lst2\/}})\index{first-n}))\-
\end{tabbing}


\noindent{\sc Event}:   Disable first-n-plus-append.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  first-n-append2 \\ \index{first-n-append2}
\=\+({\rm{plistp}}\,({\it{lst1\/}})\index{plistp} $\wedge$ ({\it{n\/}} $=$ {\rm{length}}\,({\it{lst1\/}})\index{length})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{first-n}}\,({\it{n\/}}, {\rm{append}}\,({\it{lst1\/}}, {\it{lst2\/}}))\index{first-n} $=$ {\it{lst1\/}})\-
\end{tabbing}


\noindent{\sc Event}:   Disable first-n-append2.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{pairlist} \\  
\=\+{\rm{pairlist}}\,({\it{lst1\/}}, {\it{lst2\/}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{lst1\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{cons}}\,(\=\+{\rm{cons}}\,({\rm{car}}\,({\it{lst1\/}}), {\rm{car}}\,({\it{lst2\/}})), \\ 
{\rm{pairlist}}\,({\rm{cdr}}\,({\it{lst1\/}}), {\rm{cdr}}\,({\it{lst2\/}})))\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  pairlist-plistp \\ \index{pairlist-plistp}
{\rm{plistp}}\,({\rm{pairlist}}\,({\it{x\/}}, {\it{y\/}}))\index{plistp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  length-pairlist \\ \index{length-pairlist}
{\rm{length}}\,({\rm{pairlist}}\,({\it{x\/}}, {\it{y\/}}))\index{length} $=$ {\rm{length}}\,({\it{x\/}})\index{length}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  pairlist-distributes \\ \index{pairlist-distributes}
\=\+({\rm{length}}\,({\it{lst1\/}})\index{length} $=$ {\rm{length}}\,({\it{lst3\/}})\index{length}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{pairlist}}\,({\rm{append}}\,({\it{lst1\/}}, {\it{lst2\/}}), {\rm{append}}\,({\it{lst3\/}}, {\it{lst4\/}})) \\ 
$=$$\;\;\;\;${\rm{append}}\,({\rm{pairlist}}\,({\it{lst1\/}}, {\it{lst3\/}}), {\rm{pairlist}}\,({\it{lst2\/}}, {\it{lst4\/}})))\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable pairlist-distributes.

\addvspace{18pt}


\begin{verbatim};; Given formal-vars '(X Y Z) we first push X, then Y, then Z.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{pair-formal-vars-with-actuals} \\  
\=\+{\rm{pair-formal-vars-with-actuals}}\,({\it{formal-vars\/}}, {\it{temp-stk\/}})\index{pair-formal-vars-with-actuals} \\ 
$=$$\;\;\;\;${\rm{pairlist}}\,({\it{formal-vars\/}}, {\rm{reverse}}\,({\rm{first-n}}\,({\rm{length}}\,({\it{formal-vars\/}})\index{length}, {\it{temp-stk\/}})\index{first-n})\index{reverse})\-
\end{tabbing}

\begin{verbatim};; This function converts from the external form of the temp-alists to
;; the internal.  That is, in programs, the temp alist is written as
;; (... (tempi vali) ...).  Internally, this is stored as 
;; (... (temp1 . vali) ...) to allow them to be accessed as all the
;; other alists.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{pair-temps-with-initial-values} \\  
\=\+{\rm{pair-temps-with-initial-values}}\,({\it{temp-var-dcls\/}})\index{pair-temps-with-initial-values} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{temp-var-dcls\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{cons}}\,(\=\+{\rm{cons}}\,({\rm{caar}}\,({\it{temp-var-dcls\/}}), {\rm{cadar}}\,({\it{temp-var-dcls\/}})), \\ 
{\rm{pair-temps-with-initial-values}}\,({\rm{cdr}}\,({\it{temp-var-dcls\/}}))\index{pair-temps-with-initial-values})\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  length-pair-temps-with-initial-values \\ \index{length-pair-temps-with-initial-v!alues}
{\rm{length}}\,({\rm{pair-temps-with-initial-values}}\,({\it{lst\/}})\index{pair-temps-with-initial-values})\index{length} $=$ {\rm{length}}\,({\it{lst\/}})\index{length}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{make-p-call-frame} \\  
\=\+{\rm{make-p-call-frame}}\,({\it{formal-vars\/}}, {\it{temp-stk\/}}, {\it{temp-var-dcls\/}}, {\it{ret-pc\/}})\index{make-p-call-frame} \\ 
$=$$\;\;\;\;${\rm{p-frame}}\,(\=\+{\rm{append}}\,(\=\+{\rm{pair-formal-vars-with-actuals}}\,({\it{formal-vars\/}}, {\it{temp-stk\/}})\index{pair-formal-vars-with-actuals}, \\ 
{\rm{pair-temps-with-initial-values}}\,({\it{temp-var-dcls\/}})\index{pair-temps-with-initial-values})\-, \\ 
{\it{ret-pc\/}})\-\index{p-frame}\-
\end{tabbing}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                             ;;
;;                   THE PITON INSTRUCTIONS                    ;;
;;                                                             ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


;  (CALL subr)          Push a new frame onto the ctrl-stk binding the
;                       formals and temps of the subroutine subr to their
;                       actual values and saving the current return pc.
;                       Transfer control to the beginning of subr.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{p-call-okp} \\  
\=\+{\rm{p-call-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-call-okp} \\ 
$=$$\;\;\;\;$(\=\+(\=\+{\rm{p-max-ctrl-stk-size}}\,({\it{p\/}})\index{p-max-ctrl-stk-size} \\ 
$\not<$$\;\;\;\;${\rm{p-ctrl-stk-size}}\,({\rm{push}}\,(\=\+{\rm{make-p-call-frame}}\,(\=\+{\rm{formal-vars}}\,({\rm{definition}}\,(\=\+{\rm{cadr}}\,({\it{ins\/}}), \\ 
{\rm{p-prog-segment}}\,({\it{p\/}})\index{p-prog-segment})\-\index{definition})\index{formal-vars}, \\ 
{\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk}, \\ 
{\rm{temp-var-dcls}}\,({\rm{definition}}\,(\=\+{\rm{cadr}}\,({\it{ins\/}}), \\ 
{\rm{p-prog-segment}}\,({\it{p\/}})\index{p-prog-segment})\-\index{definition})\index{temp-var-dcls}, \\ 
{\rm{add1-addr}}\,({\rm{p-pc}}\,({\it{p\/}})\index{p-pc})\index{add1-addr})\-\index{make-p-call-frame}, \\ 
{\rm{p-ctrl-stk}}\,({\it{p\/}})\index{p-ctrl-stk})\-\index{push})\index{p-ctrl-stk-size})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{length}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{length} \\ 
$\not<$$\;\;\;\;${\rm{length}}\,({\rm{formal-vars}}\,({\rm{definition}}\,(\=\+{\rm{cadr}}\,({\it{ins\/}}), \\ 
{\rm{p-prog-segment}}\,({\it{p\/}})\index{p-prog-segment})\-\index{definition})\index{formal-vars})\index{length})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-call-step} \\  
\=\+{\rm{p-call-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-call-step} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{pc}}, {\rm{cons}}\,({\rm{cadr}}\,({\it{ins\/}}), {\tt{0}}))\index{tag}, \\ 
{\rm{push}}\,(\=\+{\rm{make-p-call-frame}}\,(\=\+{\rm{formal-vars}}\,({\rm{definition}}\,(\=\+{\rm{cadr}}\,({\it{ins\/}}), \\ 
{\rm{p-prog-segment}}\,({\it{p\/}})\index{p-prog-segment})\-\index{definition})\index{formal-vars}, \\ 
{\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk}, \\ 
{\rm{temp-var-dcls}}\,({\rm{definition}}\,(\=\+{\rm{cadr}}\,({\it{ins\/}}), \\ 
{\rm{p-prog-segment}}\,({\it{p\/}})\index{p-prog-segment})\-\index{definition})\index{temp-var-dcls}, \\ 
{\rm{add1-addr}}\,({\rm{p-pc}}\,({\it{p\/}})\index{p-pc})\index{add1-addr})\-\index{make-p-call-frame}, \\ 
{\rm{p-ctrl-stk}}\,({\it{p\/}})\index{p-ctrl-stk})\-\index{push}, \\ 
{\rm{popn}}\,(\=\+{\rm{length}}\,({\rm{formal-vars}}\,({\rm{definition}}\,(\=\+{\rm{cadr}}\,({\it{ins\/}}), \\ 
{\rm{p-prog-segment}}\,({\it{p\/}})\index{p-prog-segment})\-\index{definition})\index{formal-vars})\index{length}, \\ 
{\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\-\index{popn}, \\ 
{\rm{p-prog-segment}}\,({\it{p\/}})\index{p-prog-segment}, \\ 
{\rm{p-data-segment}}\,({\it{p\/}})\index{p-data-segment}, \\ 
{\rm{p-max-ctrl-stk-size}}\,({\it{p\/}})\index{p-max-ctrl-stk-size}, \\ 
{\rm{p-max-temp-stk-size}}\,({\it{p\/}})\index{p-max-temp-stk-size}, \\ 
{\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state}\-
\end{tabbing}
      

\begin{verbatim};  (RET)              Return from the current subroutine, leaving temp-stk
;                     untouched but restoring ctrl-stk.  We make a special
;                     case out of top-level RETs:  halt the machine with the
;                     distinguished, non-erroneous psw HALT.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{p-ret-okp}$\;\;$
{\rm{p-ret-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-ret-okp} $=$ {\bf{t}}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-ret-step} \\  
\=\+{\rm{p-ret-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-ret-step} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\rm{pop}}\,({\rm{p-ctrl-stk}}\,({\it{p\/}})\index{p-ctrl-stk})\index{pop}) \\ 
{\bf then }{\rm{p-state}}\,(\=\+{\rm{ret-pc}}\,({\rm{top}}\,({\rm{p-ctrl-stk}}\,({\it{p\/}})\index{p-ctrl-stk})\index{top})\index{ret-pc}, \\ 
{\rm{pop}}\,({\rm{p-ctrl-stk}}\,({\it{p\/}})\index{p-ctrl-stk})\index{pop}, \\ 
{\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk}, \\ 
{\rm{p-prog-segment}}\,({\it{p\/}})\index{p-prog-segment}, \\ 
{\rm{p-data-segment}}\,({\it{p\/}})\index{p-data-segment}, \\ 
{\rm{p-max-ctrl-stk-size}}\,({\it{p\/}})\index{p-max-ctrl-stk-size}, \\ 
{\rm{p-max-temp-stk-size}}\,({\it{p\/}})\index{p-max-temp-stk-size}, \\ 
{\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state} \\ 
{\bf else }{\rm{p-halt}}\,({\it{p\/}}, {\tt{'}}{\tt{halt}})\index{p-halt}$\;${\bf  endif}\-\-
\end{tabbing}


\begin{verbatim};  (PUSH-CONSTANT c)    Push c onto temp-stk.  c is normally a tagged
;                       constant but we permit two abbreviations.
;                       If c is the atom 'pc, it denotes the pc
;                       of the instruction following this one.
;                       If c is a non-LISTP that is defined in
;                       the current program with a DL, it
;                       denotes the pc of that label.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{p-push-constant-okp} \\  
\=\+{\rm{p-push-constant-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-push-constant-okp} \\ 
$=$$\;\;\;\;$({\rm{length}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{length} $<$ {\rm{p-max-temp-stk-size}}\,({\it{p\/}})\index{p-max-temp-stk-size})\-
\end{tabbing}

\begin{verbatim};  First I define the ``unabbreviate'' function.  Observe that the
;  abbreviation depends upon the current state, p, since it permits the 
;  abbreviation of the current p-pc.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{unabbreviate-constant} \\  
\=\+{\rm{unabbreviate-constant}}\,({\it{c\/}}, {\it{p\/}})\index{unabbreviate-constant} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{c\/}} $=$ {\tt{'}}{\tt{pc}}$\;\;${\bf then }{\rm{add1-p-pc}}\,({\it{p\/}})\index{add1-p-pc} \\ 
{\bf elseif }{\it{c\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\rm{pc}}\,({\it{c\/}}, {\rm{p-current-program}}\,({\it{p\/}})\index{p-current-program})\index{pc} \\ 
{\bf else }{\it{c\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-push-constant-step} \\  
\=\+{\rm{p-push-constant-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-push-constant-step} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{add1-p-pc}}\,({\it{p\/}})\index{add1-p-pc}, \\ 
{\rm{p-ctrl-stk}}\,({\it{p\/}})\index{p-ctrl-stk}, \\ 
{\rm{push}}\,({\rm{unabbreviate-constant}}\,({\rm{cadr}}\,({\it{ins\/}}), {\it{p\/}})\index{unabbreviate-constant}, {\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{push}, \\ 
{\rm{p-prog-segment}}\,({\it{p\/}})\index{p-prog-segment}, \\ 
{\rm{p-data-segment}}\,({\it{p\/}})\index{p-data-segment}, \\ 
{\rm{p-max-ctrl-stk-size}}\,({\it{p\/}})\index{p-max-ctrl-stk-size}, \\ 
{\rm{p-max-temp-stk-size}}\,({\it{p\/}})\index{p-max-temp-stk-size}, \\ 
{\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state}\-
\end{tabbing}


\begin{verbatim};  (PUSH-LOCAL var)     Push the value of the local variable var onto
;                       the temp-stk.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{p-push-local-okp} \\  
\=\+{\rm{p-push-local-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-push-local-okp} \\ 
$=$$\;\;\;\;$({\rm{length}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{length} $<$ {\rm{p-max-temp-stk-size}}\,({\it{p\/}})\index{p-max-temp-stk-size})\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-push-local-step} \\  
\=\+{\rm{p-push-local-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-push-local-step} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{add1-p-pc}}\,({\it{p\/}})\index{add1-p-pc}, \\ 
{\rm{p-ctrl-stk}}\,({\it{p\/}})\index{p-ctrl-stk}, \\ 
{\rm{push}}\,({\rm{local-var-value}}\,({\rm{cadr}}\,({\it{ins\/}}), {\rm{p-ctrl-stk}}\,({\it{p\/}})\index{p-ctrl-stk})\index{local-var-value}, {\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{push}, \\ 
{\rm{p-prog-segment}}\,({\it{p\/}})\index{p-prog-segment}, \\ 
{\rm{p-data-segment}}\,({\it{p\/}})\index{p-data-segment}, \\ 
{\rm{p-max-ctrl-stk-size}}\,({\it{p\/}})\index{p-max-ctrl-stk-size}, \\ 
{\rm{p-max-temp-stk-size}}\,({\it{p\/}})\index{p-max-temp-stk-size}, \\ 
{\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state}\-
\end{tabbing}


\begin{verbatim};  (PUSH-GLOBAL var)    Push the value of the global variable var onto
;                       temp-stk.


\end{verbatim}\begin{tabbing}{\sc Definition}:\index{p-push-global-okp} \\  
\=\+{\rm{p-push-global-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-push-global-okp} \\ 
$=$$\;\;\;\;$({\rm{length}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{length} $<$ {\rm{p-max-temp-stk-size}}\,({\it{p\/}})\index{p-max-temp-stk-size})\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-push-global-step} \\  
\=\+{\rm{p-push-global-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-push-global-step} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{add1-p-pc}}\,({\it{p\/}})\index{add1-p-pc}, \\ 
{\rm{p-ctrl-stk}}\,({\it{p\/}})\index{p-ctrl-stk}, \\ 
{\rm{push}}\,(\=\+{\rm{fetch}}\,({\rm{tag}}\,({\tt{'}}{\tt{addr}}, {\rm{cons}}\,({\rm{cadr}}\,({\it{ins\/}}), {\tt{0}}))\index{tag}, {\rm{p-data-segment}}\,({\it{p\/}})\index{p-data-segment})\index{fetch}, \\ 
{\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\-\index{push}, \\ 
{\rm{p-prog-segment}}\,({\it{p\/}})\index{p-prog-segment}, \\ 
{\rm{p-data-segment}}\,({\it{p\/}})\index{p-data-segment}, \\ 
{\rm{p-max-ctrl-stk-size}}\,({\it{p\/}})\index{p-max-ctrl-stk-size}, \\ 
{\rm{p-max-temp-stk-size}}\,({\it{p\/}})\index{p-max-temp-stk-size}, \\ 
{\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state}\-
\end{tabbing}

\begin{verbatim};  (PUSH-TEMP-STK-INDEX n)

;                       Push onto temp-stk the temp stk index of the
;                       slot n below the current top.  n must be a
;                       natural number less than the length of the
;                       stack.  The object pushed is a NAT.
;                       Below is a picture of a temp-stk with
;                       of length 6, A being at the top:

;                       temp-stk:   (A B C D E F)    
;                       index:       5 4 3 2 1 0
;                       n:           0 1 2 3 4 5

;                       The index returned is suitable for use by
;                       FETCH-TEMP-STK and DEPOSIT-TEMP-STK.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{p-push-temp-stk-index-okp} \\  
\=\+{\rm{p-push-temp-stk-index-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-push-temp-stk-index-okp} \\ 
$=$$\;\;\;\;$(\=\+({\rm{length}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{length} $<$ {\rm{p-max-temp-stk-size}}\,({\it{p\/}})\index{p-max-temp-stk-size}) \\ 
$\wedge$$\;\;\;\;$({\rm{cadr}}\,({\it{ins\/}}) $<$ {\rm{length}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{length}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-push-temp-stk-index-step} \\  
\=\+{\rm{p-push-temp-stk-index-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-push-temp-stk-index-step} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{add1-p-pc}}\,({\it{p\/}})\index{add1-p-pc}, \\ 
{\rm{p-ctrl-stk}}\,({\it{p\/}})\index{p-ctrl-stk}, \\ 
{\rm{push}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{nat}}, ({\rm{length}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{length} $-$ {\rm{cadr}}\,({\it{ins\/}})) $-\;1$)\index{tag}, \\ 
{\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\-\index{push}, \\ 
{\rm{p-prog-segment}}\,({\it{p\/}})\index{p-prog-segment}, \\ 
{\rm{p-data-segment}}\,({\it{p\/}})\index{p-data-segment}, \\ 
{\rm{p-max-ctrl-stk-size}}\,({\it{p\/}})\index{p-max-ctrl-stk-size}, \\ 
{\rm{p-max-temp-stk-size}}\,({\it{p\/}})\index{p-max-temp-stk-size}, \\ 
{\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state}\-
\end{tabbing}


\begin{verbatim};  (POP)                Pop top of temp-stk and discard

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{p-pop-okp}$\;\;$
{\rm{p-pop-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-pop-okp} $=$ {\rm{listp}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-pop-step} \\  
\=\+{\rm{p-pop-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-pop-step} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{add1-p-pc}}\,({\it{p\/}})\index{add1-p-pc}, \\ 
{\rm{p-ctrl-stk}}\,({\it{p\/}})\index{p-ctrl-stk}, \\ 
{\rm{pop}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{pop}, \\ 
{\rm{p-prog-segment}}\,({\it{p\/}})\index{p-prog-segment}, \\ 
{\rm{p-data-segment}}\,({\it{p\/}})\index{p-data-segment}, \\ 
{\rm{p-max-ctrl-stk-size}}\,({\it{p\/}})\index{p-max-ctrl-stk-size}, \\ 
{\rm{p-max-temp-stk-size}}\,({\it{p\/}})\index{p-max-temp-stk-size}, \\ 
{\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state}\-
\end{tabbing}

\begin{verbatim};  (POP* n)                Pop temp-stk n times.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{p-pop*-okp} \\  
{\rm{p-pop*-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-pop*-okp} $=$ ({\rm{length}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{length} $\not<$ {\rm{cadr}}\,({\it{ins\/}}))
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-pop*-step} \\  
\=\+{\rm{p-pop*-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-pop*-step} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{add1-p-pc}}\,({\it{p\/}})\index{add1-p-pc}, \\ 
{\rm{p-ctrl-stk}}\,({\it{p\/}})\index{p-ctrl-stk}, \\ 
{\rm{popn}}\,({\rm{cadr}}\,({\it{ins\/}}), {\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{popn}, \\ 
{\rm{p-prog-segment}}\,({\it{p\/}})\index{p-prog-segment}, \\ 
{\rm{p-data-segment}}\,({\it{p\/}})\index{p-data-segment}, \\ 
{\rm{p-max-ctrl-stk-size}}\,({\it{p\/}})\index{p-max-ctrl-stk-size}, \\ 
{\rm{p-max-temp-stk-size}}\,({\it{p\/}})\index{p-max-temp-stk-size}, \\ 
{\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state}\-
\end{tabbing}

\begin{verbatim};  (POP-LOCAL var)      Pop top of temp-stk and put the value into the local
;                       variable var.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{p-pop-local-okp}$\;\;$
{\rm{p-pop-local-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-pop-local-okp} $=$ {\rm{listp}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-pop-local-step} \\  
\=\+{\rm{p-pop-local-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-pop-local-step} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{add1-p-pc}}\,({\it{p\/}})\index{add1-p-pc}, \\ 
{\rm{set-local-var-value}}\,(\=\+{\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top}, \\ 
{\rm{cadr}}\,({\it{ins\/}}), \\ 
{\rm{p-ctrl-stk}}\,({\it{p\/}})\index{p-ctrl-stk})\-\index{set-local-var-value}, \\ 
{\rm{pop}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{pop}, \\ 
{\rm{p-prog-segment}}\,({\it{p\/}})\index{p-prog-segment}, \\ 
{\rm{p-data-segment}}\,({\it{p\/}})\index{p-data-segment}, \\ 
{\rm{p-max-ctrl-stk-size}}\,({\it{p\/}})\index{p-max-ctrl-stk-size}, \\ 
{\rm{p-max-temp-stk-size}}\,({\it{p\/}})\index{p-max-temp-stk-size}, \\ 
{\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state}\-
\end{tabbing}

\begin{verbatim};  (POP-GLOBAL var)     Pop top of temp-stk and put the value into the global
;                       variable var.


\end{verbatim}\begin{tabbing}{\sc Definition}:\index{p-pop-global-okp}$\;\;$
{\rm{p-pop-global-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-pop-global-okp} $=$ {\rm{listp}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-pop-global-step} \\  
\=\+{\rm{p-pop-global-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-pop-global-step} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{add1-p-pc}}\,({\it{p\/}})\index{add1-p-pc}, \\ 
{\rm{p-ctrl-stk}}\,({\it{p\/}})\index{p-ctrl-stk}, \\ 
{\rm{pop}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{pop}, \\ 
{\rm{p-prog-segment}}\,({\it{p\/}})\index{p-prog-segment}, \\ 
{\rm{deposit}}\,(\=\+{\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top}, \\ 
{\rm{tag}}\,({\tt{'}}{\tt{addr}}, {\rm{cons}}\,({\rm{cadr}}\,({\it{ins\/}}), {\tt{0}}))\index{tag}, \\ 
{\rm{p-data-segment}}\,({\it{p\/}})\index{p-data-segment})\-\index{deposit}, \\ 
{\rm{p-max-ctrl-stk-size}}\,({\it{p\/}})\index{p-max-ctrl-stk-size}, \\ 
{\rm{p-max-temp-stk-size}}\,({\it{p\/}})\index{p-max-temp-stk-size}, \\ 
{\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state}\-
\end{tabbing}

\begin{verbatim};   (FETCH-TEMP-STK)    Pop top of temp-stk.  The result must
;                       be an index into the temp-stk, that is,
;                       a NAT less than the length of temp-stk.
;                       Push onto the temp-stk the contents of
;                       the indexed cell of temp-stk.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{p-fetch-temp-stk-okp} \\  
\=\+{\rm{p-fetch-temp-stk-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-fetch-temp-stk-okp} \\ 
$=$$\;\;\;\;$(\=\+{\rm{listp}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk}) \\ 
$\wedge$$\;\;\;\;${\rm{p-objectp-type}}\,({\tt{'}}{\tt{nat}}, {\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top}, {\it{p\/}})\index{p-objectp-type} \\ 
$\wedge$$\;\;\;\;$({\rm{untag}}\,({\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top})\index{untag} $<$ {\rm{length}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{length}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-fetch-temp-stk-step} \\  
\=\+{\rm{p-fetch-temp-stk-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-fetch-temp-stk-step} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{add1-p-pc}}\,({\it{p\/}})\index{add1-p-pc}, \\ 
{\rm{p-ctrl-stk}}\,({\it{p\/}})\index{p-ctrl-stk}, \\ 
{\rm{push}}\,(\=\+{\rm{rget}}\,({\rm{untag}}\,({\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top})\index{untag}, {\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{rget}, \\ 
{\rm{pop}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{pop})\-\index{push}, \\ 
{\rm{p-prog-segment}}\,({\it{p\/}})\index{p-prog-segment}, \\ 
{\rm{p-data-segment}}\,({\it{p\/}})\index{p-data-segment}, \\ 
{\rm{p-max-ctrl-stk-size}}\,({\it{p\/}})\index{p-max-ctrl-stk-size}, \\ 
{\rm{p-max-temp-stk-size}}\,({\it{p\/}})\index{p-max-temp-stk-size}, \\ 
{\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state}\-
\end{tabbing}

\begin{verbatim};   (DEPOSIT-TEMP-STK)  Pop top and top1 off of temp-stk.  top must be
;                       an index into temp-stk.  Deposit top1 into the indexed
;                       cell of temp-stk.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{p-deposit-temp-stk-okp} \\  
\=\+{\rm{p-deposit-temp-stk-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-deposit-temp-stk-okp} \\ 
$=$$\;\;\;\;$(\=\+{\rm{listp}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk}) \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\rm{pop}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{pop}) \\ 
$\wedge$$\;\;\;\;${\rm{p-objectp-type}}\,({\tt{'}}{\tt{nat}}, {\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top}, {\it{p\/}})\index{p-objectp-type} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{untag}}\,({\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top})\index{untag} \\ 
$<$$\;\;\;\;${\rm{length}}\,({\rm{pop}}\,({\rm{pop}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{pop})\index{pop})\index{length})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-deposit-temp-stk-step} \\  
\=\+{\rm{p-deposit-temp-stk-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-deposit-temp-stk-step} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{add1-p-pc}}\,({\it{p\/}})\index{add1-p-pc}, \\ 
{\rm{p-ctrl-stk}}\,({\it{p\/}})\index{p-ctrl-stk}, \\ 
{\rm{rput}}\,(\=\+{\rm{top1}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top1}, \\ 
{\rm{untag}}\,({\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top})\index{untag}, \\ 
{\rm{pop}}\,({\rm{pop}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{pop})\index{pop})\-\index{rput}, \\ 
{\rm{p-prog-segment}}\,({\it{p\/}})\index{p-prog-segment}, \\ 
{\rm{p-data-segment}}\,({\it{p\/}})\index{p-data-segment}, \\ 
{\rm{p-max-ctrl-stk-size}}\,({\it{p\/}})\index{p-max-ctrl-stk-size}, \\ 
{\rm{p-max-temp-stk-size}}\,({\it{p\/}})\index{p-max-temp-stk-size}, \\ 
{\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state}\-
\end{tabbing}

\begin{verbatim};  (JUMP lab)           Jump to the location named by lab in the current 
;                       program.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{p-jump-okp}$\;\;$
{\rm{p-jump-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-jump-okp} $=$ {\bf{t}}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-jump-step} \\  
\=\+{\rm{p-jump-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-jump-step} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{pc}}\,({\rm{cadr}}\,({\it{ins\/}}), {\rm{p-current-program}}\,({\it{p\/}})\index{p-current-program})\index{pc}, \\ 
{\rm{p-ctrl-stk}}\,({\it{p\/}})\index{p-ctrl-stk}, \\ 
{\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk}, \\ 
{\rm{p-prog-segment}}\,({\it{p\/}})\index{p-prog-segment}, \\ 
{\rm{p-data-segment}}\,({\it{p\/}})\index{p-data-segment}, \\ 
{\rm{p-max-ctrl-stk-size}}\,({\it{p\/}})\index{p-max-ctrl-stk-size}, \\ 
{\rm{p-max-temp-stk-size}}\,({\it{p\/}})\index{p-max-temp-stk-size}, \\ 
{\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state}\-
\end{tabbing}


\begin{verbatim};   (JUMP-CASE lab0 lab1 ... labn)
;                       Pop top of temp-stk.  It must be a some nat, i.
;                       Jump to labi.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{p-jump-case-okp} \\  
\=\+{\rm{p-jump-case-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-jump-case-okp} \\ 
$=$$\;\;\;\;$(\=\+{\rm{listp}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk}) \\ 
$\wedge$$\;\;\;\;${\rm{p-objectp-type}}\,({\tt{'}}{\tt{nat}}, {\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top}, {\it{p\/}})\index{p-objectp-type} \\ 
$\wedge$$\;\;\;\;$({\rm{untag}}\,({\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top})\index{untag} $<$ {\rm{length}}\,({\rm{cdr}}\,({\it{ins\/}}))\index{length}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-jump-case-step} \\  
\=\+{\rm{p-jump-case-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-jump-case-step} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{pc}}\,(\=\+{\rm{get}}\,({\rm{untag}}\,({\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top})\index{untag}, {\rm{cdr}}\,({\it{ins\/}}))\index{get}, \\ 
{\rm{p-current-program}}\,({\it{p\/}})\index{p-current-program})\-\index{pc}, \\ 
{\rm{p-ctrl-stk}}\,({\it{p\/}})\index{p-ctrl-stk}, \\ 
{\rm{pop}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{pop}, \\ 
{\rm{p-prog-segment}}\,({\it{p\/}})\index{p-prog-segment}, \\ 
{\rm{p-data-segment}}\,({\it{p\/}})\index{p-data-segment}, \\ 
{\rm{p-max-ctrl-stk-size}}\,({\it{p\/}})\index{p-max-ctrl-stk-size}, \\ 
{\rm{p-max-temp-stk-size}}\,({\it{p\/}})\index{p-max-temp-stk-size}, \\ 
{\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state}\-
\end{tabbing}

\begin{verbatim};  (SET-LOCAL var)      Set the local variable var to the top of the temp-stk
;                       but do not pop the temp-stk.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{p-set-local-okp}$\;\;$
{\rm{p-set-local-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-set-local-okp} $=$ {\rm{listp}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-set-local-step} \\  
\=\+{\rm{p-set-local-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-set-local-step} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{add1-p-pc}}\,({\it{p\/}})\index{add1-p-pc}, \\ 
{\rm{set-local-var-value}}\,(\=\+{\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top}, \\ 
{\rm{cadr}}\,({\it{ins\/}}), \\ 
{\rm{p-ctrl-stk}}\,({\it{p\/}})\index{p-ctrl-stk})\-\index{set-local-var-value}, \\ 
{\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk}, \\ 
{\rm{p-prog-segment}}\,({\it{p\/}})\index{p-prog-segment}, \\ 
{\rm{p-data-segment}}\,({\it{p\/}})\index{p-data-segment}, \\ 
{\rm{p-max-ctrl-stk-size}}\,({\it{p\/}})\index{p-max-ctrl-stk-size}, \\ 
{\rm{p-max-temp-stk-size}}\,({\it{p\/}})\index{p-max-temp-stk-size}, \\ 
{\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state}\-
\end{tabbing}

\begin{verbatim}; (TEST-type-AND-JUMP flg lab)
;                       Each instruction in this family pops one item, x, off
;                       temp-stk.  The item must be of the indicated type.
;                       The item is tested as indicated by the flg.  If the
;                       test is satisfied, we jump to the indicated label, lab.
;                       Otherwise, the next instruction is executed.  The 
;                       flags and tests available depend upon the type.
;                       We enumerate them in the documentation for each
;                       test-and-jump instruction.

;  For each member of the family I define p-test-xxx-and-jump-okp,
;  which approves the execution of the instruction.  Then I define
;  p-test-xxx-and-jump-step and
;  icode-test-xxx-and-jump.  Both the -okp and the
;  -step function are defined in terms of more general purpose functions.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{p-test-and-jump-okp} \\  
\=\+{\rm{p-test-and-jump-okp}}\,({\it{ins\/}}, {\it{type\/}}, {\it{test\/}}, {\it{p\/}})\index{p-test-and-jump-okp} \\ 
$=$$\;\;\;\;$({\rm{listp}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk}) $\wedge$ {\rm{p-objectp-type}}\,({\it{type\/}}, {\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top}, {\it{p\/}})\index{p-objectp-type})\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-test-and-jump-step} \\  
\=\+{\rm{p-test-and-jump-step}}\,({\it{test\/}}, {\it{lab\/}}, {\it{p\/}})\index{p-test-and-jump-step} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{test\/}} \\ 
{\bf then }{\rm{p-state}}\,(\=\+{\rm{pc}}\,({\it{lab\/}}, {\rm{p-current-program}}\,({\it{p\/}})\index{p-current-program})\index{pc}, \\ 
{\rm{p-ctrl-stk}}\,({\it{p\/}})\index{p-ctrl-stk}, \\ 
{\rm{pop}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{pop}, \\ 
{\rm{p-prog-segment}}\,({\it{p\/}})\index{p-prog-segment}, \\ 
{\rm{p-data-segment}}\,({\it{p\/}})\index{p-data-segment}, \\ 
{\rm{p-max-ctrl-stk-size}}\,({\it{p\/}})\index{p-max-ctrl-stk-size}, \\ 
{\rm{p-max-temp-stk-size}}\,({\it{p\/}})\index{p-max-temp-stk-size}, \\ 
{\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state} \\ 
{\bf else }{\rm{p-state}}\,(\=\+{\rm{add1-p-pc}}\,({\it{p\/}})\index{add1-p-pc}, \\ 
{\rm{p-ctrl-stk}}\,({\it{p\/}})\index{p-ctrl-stk}, \\ 
{\rm{pop}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{pop}, \\ 
{\rm{p-prog-segment}}\,({\it{p\/}})\index{p-prog-segment}, \\ 
{\rm{p-data-segment}}\,({\it{p\/}})\index{p-data-segment}, \\ 
{\rm{p-max-ctrl-stk-size}}\,({\it{p\/}})\index{p-max-ctrl-stk-size}, \\ 
{\rm{p-max-temp-stk-size}}\,({\it{p\/}})\index{p-max-temp-stk-size}, \\ 
{\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state}$\;${\bf  endif}\-\-
\end{tabbing}


\begin{verbatim}; (TEST-NAT-AND-JUMP flg lab)

;                          flg                test

;                          ZERO          jump if x is 0
;                      NOT-ZERO          jump if x is not 0

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{p-test-natp} \\  
\=\+{\rm{p-test-natp}}\,({\it{flg\/}}, {\it{x\/}})\index{p-test-natp} \\ 
$=$$\;\;\;\;$\=\+{\bf case on }{\it{flg\/}}: \\ 
{\bf case = }{\it{zero\/}} \\ 
{\bf then }{\it{x\/}} $=$ {\tt{0}} \\ 
{\bf otherwise }{\it{x\/}} $\not=$ {\tt{0}}$\;${\bf  endcase}\-\-
\end{tabbing}


\begin{tabbing}{\sc Definition}:\index{p-test-nat-and-jump-okp} \\  
\=\+{\rm{p-test-nat-and-jump-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-test-nat-and-jump-okp} \\ 
$=$$\;\;\;\;${\rm{p-test-and-jump-okp}}\,(\=\+{\it{ins\/}}, \\ 
{\tt{'}}{\tt{nat}}, \\ 
{\rm{p-test-natp}}\,({\rm{cadr}}\,({\it{ins\/}}), {\rm{untag}}\,({\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top})\index{untag})\index{p-test-natp}, \\ 
{\it{p\/}})\-\index{p-test-and-jump-okp}\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-test-nat-and-jump-step} \\  
\=\+{\rm{p-test-nat-and-jump-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-test-nat-and-jump-step} \\ 
$=$$\;\;\;\;${\rm{p-test-and-jump-step}}\,(\=\+{\rm{p-test-natp}}\,({\rm{cadr}}\,({\it{ins\/}}), {\rm{untag}}\,({\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top})\index{untag})\index{p-test-natp}, \\ 
{\rm{caddr}}\,({\it{ins\/}}), \\ 
{\it{p\/}})\-\index{p-test-and-jump-step}\-
\end{tabbing}

\begin{verbatim}; (TEST-INT-AND-JUMP flg lab)
;                          flg                test
;                          ZERO          jump if x is 0
;                      NOT-ZERO          jump if x is not 0
;                          NEG           jump if x is negative
;                      NOT-NEG           jump if x is not negative
;                          POS           jump if x is positive
;                      NOT-POS           jump if x is not positive


\end{verbatim}\begin{tabbing}{\sc Definition}:\index{p-test-intp} \\  
\=\+{\rm{p-test-intp}}\,({\it{flg\/}}, {\it{x\/}})\index{p-test-intp} \\ 
$=$$\;\;\;\;$\=\+{\bf case on }{\it{flg\/}}: \\ 
{\bf case = }{\it{zero\/}} \\ 
{\bf then }{\it{x\/}} $=$ {\tt{0}} \\ 
{\bf case = }{\it{not-zero\/}} \\ 
{\bf $\;\;$then }{\it{x\/}} $\not=$ {\tt{0}} \\ 
{\bf case = }{\it{neg\/}} \\ 
{\bf $\;\;$then }{\rm{negativep}}\,({\it{x\/}}) \\ 
{\bf case = }{\it{not-neg\/}} \\ 
{\bf $\;\;$then }$\neg$ {\rm{negativep}}\,({\it{x\/}}) \\ 
{\bf case = }{\it{pos\/}} \\ 
{\bf $\;\;$then }({\it{x\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{x\/}} $\not=$ {\tt{0}}) \\ 
{\bf otherwise }({\it{x\/}} $=$ {\tt{0}}) $\vee$ {\rm{negativep}}\,({\it{x\/}})$\;${\bf  endcase}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-test-int-and-jump-okp} \\  
\=\+{\rm{p-test-int-and-jump-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-test-int-and-jump-okp} \\ 
$=$$\;\;\;\;${\rm{p-test-and-jump-okp}}\,(\=\+{\it{ins\/}}, \\ 
{\tt{'}}{\tt{int}}, \\ 
{\rm{p-test-intp}}\,({\rm{cadr}}\,({\it{ins\/}}), {\rm{untag}}\,({\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top})\index{untag})\index{p-test-intp}, \\ 
{\it{p\/}})\-\index{p-test-and-jump-okp}\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-test-int-and-jump-step} \\  
\=\+{\rm{p-test-int-and-jump-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-test-int-and-jump-step} \\ 
$=$$\;\;\;\;${\rm{p-test-and-jump-step}}\,(\=\+{\rm{p-test-intp}}\,({\rm{cadr}}\,({\it{ins\/}}), {\rm{untag}}\,({\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top})\index{untag})\index{p-test-intp}, \\ 
{\rm{caddr}}\,({\it{ins\/}}), \\ 
{\it{p\/}})\-\index{p-test-and-jump-step}\-
\end{tabbing}


\begin{verbatim}; (TEST-BOOL-AND-JUMP flg lab)
;                          flg                test
;                          T            jump if x is T
;                          F            jump if x is F

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{p-test-boolp} \\  
\=\+{\rm{p-test-boolp}}\,({\it{flg\/}}, {\it{x\/}})\index{p-test-boolp} \\ 
$=$$\;\;\;\;$\=\+{\bf case on }{\it{flg\/}}: \\ 
{\bf case = }{\bf{t}} \\ 
{\bf then }{\it{x\/}} $=$ {\tt{'}}{\tt{t}} \\ 
{\bf otherwise }{\it{x\/}} $=$ {\tt{'}}{\tt{f}}$\;${\bf  endcase}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-test-bool-and-jump-okp} \\  
\=\+{\rm{p-test-bool-and-jump-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-test-bool-and-jump-okp} \\ 
$=$$\;\;\;\;${\rm{p-test-and-jump-okp}}\,(\=\+{\it{ins\/}}, \\ 
{\tt{'}}{\tt{bool}}, \\ 
{\rm{p-test-boolp}}\,({\rm{cadr}}\,({\it{ins\/}}), {\rm{untag}}\,({\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top})\index{untag})\index{p-test-boolp}, \\ 
{\it{p\/}})\-\index{p-test-and-jump-okp}\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-test-bool-and-jump-step} \\  
\=\+{\rm{p-test-bool-and-jump-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-test-bool-and-jump-step} \\ 
$=$$\;\;\;\;${\rm{p-test-and-jump-step}}\,(\=\+{\rm{p-test-boolp}}\,({\rm{cadr}}\,({\it{ins\/}}), {\rm{untag}}\,({\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top})\index{untag})\index{p-test-boolp}, \\ 
{\rm{caddr}}\,({\it{ins\/}}), \\ 
{\it{p\/}})\-\index{p-test-and-jump-step}\-
\end{tabbing}

\begin{verbatim};   (NO-OP)             Do nothing.  Advance the pc to the next instruction.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{p-no-op-okp}$\;\;$
{\rm{p-no-op-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-no-op-okp} $=$ {\bf{t}}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-no-op-step} \\  
\=\+{\rm{p-no-op-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-no-op-step} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{add1-p-pc}}\,({\it{p\/}})\index{add1-p-pc}, \\ 
{\rm{p-ctrl-stk}}\,({\it{p\/}})\index{p-ctrl-stk}, \\ 
{\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk}, \\ 
{\rm{p-prog-segment}}\,({\it{p\/}})\index{p-prog-segment}, \\ 
{\rm{p-data-segment}}\,({\it{p\/}})\index{p-data-segment}, \\ 
{\rm{p-max-ctrl-stk-size}}\,({\it{p\/}})\index{p-max-ctrl-stk-size}, \\ 
{\rm{p-max-temp-stk-size}}\,({\it{p\/}})\index{p-max-temp-stk-size}, \\ 
{\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state}\-
\end{tabbing}


\begin{verbatim};   (EQ)                Pop top and top1 off of temp-stk.  If they
;                       are both of the same type, push T or F according
;                       to whether they are equal.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{p-eq-okp} \\  
\=\+{\rm{p-eq-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-eq-okp} \\ 
$=$$\;\;\;\;$(\=\+{\rm{listp}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk}) \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\rm{pop}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{pop}) \\ 
$\wedge$$\;\;\;\;$({\rm{type}}\,({\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top})\index{type} $=$ {\rm{type}}\,({\rm{top1}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top1})\index{type}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-eq-step} \\  
\=\+{\rm{p-eq-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-eq-step} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{add1-p-pc}}\,({\it{p\/}})\index{add1-p-pc}, \\ 
{\rm{p-ctrl-stk}}\,({\it{p\/}})\index{p-ctrl-stk}, \\ 
{\rm{push}}\,(\=\+{\rm{bool}}\,(\=\+{\rm{untag}}\,({\rm{top1}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top1})\index{untag} \\ 
$=$$\;\;\;\;${\rm{untag}}\,({\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top})\index{untag}\-)\index{bool}, \\ 
{\rm{pop}}\,({\rm{pop}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{pop})\index{pop})\-\index{push}, \\ 
{\rm{p-prog-segment}}\,({\it{p\/}})\index{p-prog-segment}, \\ 
{\rm{p-data-segment}}\,({\it{p\/}})\index{p-data-segment}, \\ 
{\rm{p-max-ctrl-stk-size}}\,({\it{p\/}})\index{p-max-ctrl-stk-size}, \\ 
{\rm{p-max-temp-stk-size}}\,({\it{p\/}})\index{p-max-temp-stk-size}, \\ 
{\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state}\-
\end{tabbing}

\begin{verbatim};   (ADD-INT-WITH-CARRY)
;                       Pop three things off temp stack, top, top1 and
;                       top2.  Top and top1 must be INTs.  Top2 must
;                       be Boolean.  Add top+top1+top2 -- coercing T to 1
;                       and F to 0.  Push two results.  First, a boolean
;                       indicating whether top+top1+top2 is not small.
;                       On top of that, push the corrected sum.  The corrected
;                       sum is the sum, if that is a small-integerp; the
;                       sum+2**word-size, if the sum is not small and is 
;                       negative; and the sum-2**word-size, if the sum is
;                       not small and not negative.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{p-add-int-with-carry-okp} \\  
\=\+{\rm{p-add-int-with-carry-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-add-int-with-carry-okp} \\ 
$=$$\;\;\;\;$(\=\+{\rm{listp}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk}) \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\rm{pop}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{pop}) \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\rm{pop}}\,({\rm{pop}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{pop})\index{pop}) \\ 
$\wedge$$\;\;\;\;${\rm{p-objectp-type}}\,({\tt{'}}{\tt{int}}, {\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top}, {\it{p\/}})\index{p-objectp-type} \\ 
$\wedge$$\;\;\;\;${\rm{p-objectp-type}}\,({\tt{'}}{\tt{int}}, {\rm{top1}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top1}, {\it{p\/}})\index{p-objectp-type} \\ 
$\wedge$$\;\;\;\;${\rm{p-objectp-type}}\,({\tt{'}}{\tt{bool}}, {\rm{top2}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top2}, {\it{p\/}})\index{p-objectp-type})\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-add-int-with-carry-step} \\  
\=\+{\rm{p-add-int-with-carry-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-add-int-with-carry-step} \\ 
$=$$\;\;\;\;$\=\+{\bf let }\=\+{\it{sum\/}}{\bf $\;$ be$\;\;$}{\rm{iplus}}\,(\=\+{\rm{bool-to-nat}}\,({\rm{untag}}\,({\rm{top2}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top2})\index{untag})\index{bool-to-nat}, \\ 
{\rm{iplus}}\,(\=\+{\rm{untag}}\,({\rm{top1}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top1})\index{untag}, \\ 
{\rm{untag}}\,({\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top})\index{untag})\-\index{iplus})\-\index{iplus}\- \\ 
{\bf in} \\ 
{\rm{p-state}}\,(\=\+{\rm{add1-p-pc}}\,({\it{p\/}})\index{add1-p-pc}, \\ 
{\rm{p-ctrl-stk}}\,({\it{p\/}})\index{p-ctrl-stk}, \\ 
{\rm{push}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{int}}, {\rm{fix-small-integer}}\,({\it{sum\/}}, {\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size})\index{fix-small-integer})\index{tag}, \\ 
{\rm{push}}\,(\=\+{\rm{bool}}\,($\neg$ {\rm{small-integerp}}\,({\it{sum\/}}, {\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size})\index{small-integerp})\index{bool}, \\ 
{\rm{pop}}\,({\rm{pop}}\,({\rm{pop}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{pop})\index{pop})\index{pop})\-\index{push})\-\index{push}, \\ 
{\rm{p-prog-segment}}\,({\it{p\/}})\index{p-prog-segment}, \\ 
{\rm{p-data-segment}}\,({\it{p\/}})\index{p-data-segment}, \\ 
{\rm{p-max-ctrl-stk-size}}\,({\it{p\/}})\index{p-max-ctrl-stk-size}, \\ 
{\rm{p-max-temp-stk-size}}\,({\it{p\/}})\index{p-max-temp-stk-size}, \\ 
{\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state}$\;${\bf  endlet}\-\-
\end{tabbing}

\begin{verbatim};;  (SUB-INT)

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{p-sub-int-okp} \\  
\=\+{\rm{p-sub-int-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-sub-int-okp} \\ 
$=$$\;\;\;\;$(\=\+{\rm{listp}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk}) \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\rm{pop}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{pop}) \\ 
$\wedge$$\;\;\;\;${\rm{p-objectp-type}}\,({\tt{'}}{\tt{int}}, {\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top}, {\it{p\/}})\index{p-objectp-type} \\ 
$\wedge$$\;\;\;\;${\rm{p-objectp-type}}\,({\tt{'}}{\tt{int}}, {\rm{top1}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top1}, {\it{p\/}})\index{p-objectp-type} \\ 
$\wedge$$\;\;\;\;${\rm{small-integerp}}\,(\=\+{\rm{idifference}}\,(\=\+{\rm{untag}}\,({\rm{top1}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top1})\index{untag}, \\ 
{\rm{untag}}\,({\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top})\index{untag})\-\index{idifference}, \\ 
{\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size})\-\index{small-integerp})\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-sub-int-step} \\  
\=\+{\rm{p-sub-int-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-sub-int-step} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{add1-p-pc}}\,({\it{p\/}})\index{add1-p-pc}, \\ 
{\rm{p-ctrl-stk}}\,({\it{p\/}})\index{p-ctrl-stk}, \\ 
{\rm{push}}\,(\=\+{\rm{tag}}\,(\=\+{\tt{'}}{\tt{int}}, \\ 
{\rm{idifference}}\,(\=\+{\rm{untag}}\,({\rm{top1}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top1})\index{untag}, \\ 
{\rm{untag}}\,({\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top})\index{untag})\-\index{idifference})\-\index{tag}, \\ 
{\rm{pop}}\,({\rm{pop}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{pop})\index{pop})\-\index{push}, \\ 
{\rm{p-prog-segment}}\,({\it{p\/}})\index{p-prog-segment}, \\ 
{\rm{p-data-segment}}\,({\it{p\/}})\index{p-data-segment}, \\ 
{\rm{p-max-ctrl-stk-size}}\,({\it{p\/}})\index{p-max-ctrl-stk-size}, \\ 
{\rm{p-max-temp-stk-size}}\,({\it{p\/}})\index{p-max-temp-stk-size}, \\ 
{\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state}\-
\end{tabbing}

\begin{verbatim};   (SUB-INT-WITH-CARRY)
;                       Pop three things off temp stack, top, top1 and
;                       top2.  Top and top1 must be INTs.  Top2 must
;                       be Boolean.  Form top1-(top+top2) -- coercing T to 1
;                       and F to 0.  Push two results.  First, a boolean
;                       indicating whether top1-(top+top2) is not small.
;                       On top of that, push the corrected diff. The corrected
;                       diff is the diff, if that is a small-integerp; the
;                       diff+2**word-size, if the diff is not small and is 
;                       negative; and the diff-2**word-size, if the diff is
;                       not small and not negative.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{p-sub-int-with-carry-okp} \\  
\=\+{\rm{p-sub-int-with-carry-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-sub-int-with-carry-okp} \\ 
$=$$\;\;\;\;$(\=\+{\rm{listp}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk}) \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\rm{pop}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{pop}) \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\rm{pop}}\,({\rm{pop}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{pop})\index{pop}) \\ 
$\wedge$$\;\;\;\;${\rm{p-objectp-type}}\,({\tt{'}}{\tt{int}}, {\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top}, {\it{p\/}})\index{p-objectp-type} \\ 
$\wedge$$\;\;\;\;${\rm{p-objectp-type}}\,({\tt{'}}{\tt{int}}, {\rm{top1}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top1}, {\it{p\/}})\index{p-objectp-type} \\ 
$\wedge$$\;\;\;\;${\rm{p-objectp-type}}\,({\tt{'}}{\tt{bool}}, {\rm{top2}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top2}, {\it{p\/}})\index{p-objectp-type})\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-sub-int-with-carry-step} \\  
\=\+{\rm{p-sub-int-with-carry-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-sub-int-with-carry-step} \\ 
$=$$\;\;\;\;$\=\+{\bf let }\=\+{\it{diff\/}}{\bf $\;$ be$\;\;$}{\rm{idifference}}\,(\=\+{\rm{untag}}\,({\rm{top1}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top1})\index{untag}, \\ 
{\rm{iplus}}\,(\=\+{\rm{untag}}\,({\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top})\index{untag}, \\ 
{\rm{bool-to-nat}}\,({\rm{untag}}\,({\rm{top2}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top2})\index{untag})\index{bool-to-nat})\-\index{iplus})\-\index{idifference}\- \\ 
{\bf in} \\ 
{\rm{p-state}}\,(\=\+{\rm{add1-p-pc}}\,({\it{p\/}})\index{add1-p-pc}, \\ 
{\rm{p-ctrl-stk}}\,({\it{p\/}})\index{p-ctrl-stk}, \\ 
{\rm{push}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{int}}, {\rm{fix-small-integer}}\,({\it{diff\/}}, {\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size})\index{fix-small-integer})\index{tag}, \\ 
{\rm{push}}\,(\=\+{\rm{bool}}\,($\neg$ {\rm{small-integerp}}\,({\it{diff\/}}, {\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size})\index{small-integerp})\index{bool}, \\ 
{\rm{pop}}\,({\rm{pop}}\,({\rm{pop}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{pop})\index{pop})\index{pop})\-\index{push})\-\index{push}, \\ 
{\rm{p-prog-segment}}\,({\it{p\/}})\index{p-prog-segment}, \\ 
{\rm{p-data-segment}}\,({\it{p\/}})\index{p-data-segment}, \\ 
{\rm{p-max-ctrl-stk-size}}\,({\it{p\/}})\index{p-max-ctrl-stk-size}, \\ 
{\rm{p-max-temp-stk-size}}\,({\it{p\/}})\index{p-max-temp-stk-size}, \\ 
{\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state}$\;${\bf  endlet}\-\-
\end{tabbing}

\begin{verbatim};   (NEG-INT)           Pop top of temp-stk.  It must be an INT.
;                       Negate it and push the result provided it is
;                       representable as an INT.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{p-neg-int-okp} \\  
\=\+{\rm{p-neg-int-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-neg-int-okp} \\ 
$=$$\;\;\;\;$(\=\+{\rm{listp}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk}) \\ 
$\wedge$$\;\;\;\;${\rm{p-objectp-type}}\,({\tt{'}}{\tt{int}}, {\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top}, {\it{p\/}})\index{p-objectp-type} \\ 
$\wedge$$\;\;\;\;${\rm{small-integerp}}\,(\=\+{\rm{inegate}}\,({\rm{untag}}\,({\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top})\index{untag})\index{inegate}, \\ 
{\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size})\-\index{small-integerp})\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-neg-int-step} \\  
\=\+{\rm{p-neg-int-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-neg-int-step} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{add1-p-pc}}\,({\it{p\/}})\index{add1-p-pc}, \\ 
{\rm{p-ctrl-stk}}\,({\it{p\/}})\index{p-ctrl-stk}, \\ 
{\rm{push}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{int}}, {\rm{inegate}}\,({\rm{untag}}\,({\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top})\index{untag})\index{inegate})\index{tag}, \\ 
{\rm{pop}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{pop})\-\index{push}, \\ 
{\rm{p-prog-segment}}\,({\it{p\/}})\index{p-prog-segment}, \\ 
{\rm{p-data-segment}}\,({\it{p\/}})\index{p-data-segment}, \\ 
{\rm{p-max-ctrl-stk-size}}\,({\it{p\/}})\index{p-max-ctrl-stk-size}, \\ 
{\rm{p-max-temp-stk-size}}\,({\it{p\/}})\index{p-max-temp-stk-size}, \\ 
{\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state}\-
\end{tabbing}

\begin{verbatim};   (LT-INT)            Pop top and top1 off of temp-stk, and push T or F
;                       according to whether top1 < top.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{p-lt-int-okp} \\  
\=\+{\rm{p-lt-int-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-lt-int-okp} \\ 
$=$$\;\;\;\;$(\=\+{\rm{listp}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk}) \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\rm{pop}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{pop}) \\ 
$\wedge$$\;\;\;\;${\rm{p-objectp-type}}\,({\tt{'}}{\tt{int}}, {\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top}, {\it{p\/}})\index{p-objectp-type} \\ 
$\wedge$$\;\;\;\;${\rm{p-objectp-type}}\,({\tt{'}}{\tt{int}}, {\rm{top1}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top1}, {\it{p\/}})\index{p-objectp-type})\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-lt-int-step} \\  
\=\+{\rm{p-lt-int-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-lt-int-step} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{add1-p-pc}}\,({\it{p\/}})\index{add1-p-pc}, \\ 
{\rm{p-ctrl-stk}}\,({\it{p\/}})\index{p-ctrl-stk}, \\ 
{\rm{push}}\,(\=\+{\rm{bool}}\,({\rm{ilessp}}\,(\=\+{\rm{untag}}\,({\rm{top1}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top1})\index{untag}, \\ 
{\rm{untag}}\,({\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top})\index{untag})\-\index{ilessp})\index{bool}, \\ 
{\rm{pop}}\,({\rm{pop}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{pop})\index{pop})\-\index{push}, \\ 
{\rm{p-prog-segment}}\,({\it{p\/}})\index{p-prog-segment}, \\ 
{\rm{p-data-segment}}\,({\it{p\/}})\index{p-data-segment}, \\ 
{\rm{p-max-ctrl-stk-size}}\,({\it{p\/}})\index{p-max-ctrl-stk-size}, \\ 
{\rm{p-max-temp-stk-size}}\,({\it{p\/}})\index{p-max-temp-stk-size}, \\ 
{\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state}\-
\end{tabbing}

\begin{verbatim};   (INT-TO-NAT)        Pop top off of temp-stk.  Top should
;                       be of type INT and be nonnegative.
;                       Push the NAT corresponding to top.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{p-int-to-nat-okp} \\  
\=\+{\rm{p-int-to-nat-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-int-to-nat-okp} \\ 
$=$$\;\;\;\;$(\=\+{\rm{listp}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk}) \\ 
$\wedge$$\;\;\;\;${\rm{p-objectp-type}}\,({\tt{'}}{\tt{int}}, {\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top}, {\it{p\/}})\index{p-objectp-type} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{negativep}}\,({\rm{untag}}\,({\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top})\index{untag})))\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-int-to-nat-step} \\  
\=\+{\rm{p-int-to-nat-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-int-to-nat-step} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{add1-p-pc}}\,({\it{p\/}})\index{add1-p-pc}, \\ 
{\rm{p-ctrl-stk}}\,({\it{p\/}})\index{p-ctrl-stk}, \\ 
{\rm{push}}\,({\rm{tag}}\,({\tt{'}}{\tt{nat}}, {\rm{untag}}\,({\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top})\index{untag})\index{tag}, {\rm{pop}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{pop})\index{push}, \\ 
{\rm{p-prog-segment}}\,({\it{p\/}})\index{p-prog-segment}, \\ 
{\rm{p-data-segment}}\,({\it{p\/}})\index{p-data-segment}, \\ 
{\rm{p-max-ctrl-stk-size}}\,({\it{p\/}})\index{p-max-ctrl-stk-size}, \\ 
{\rm{p-max-temp-stk-size}}\,({\it{p\/}})\index{p-max-temp-stk-size}, \\ 
{\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state}\-
\end{tabbing}

\begin{verbatim};   (ADD-NAT)           Pop top and top1 off of temp-stk.
;                       Both top and top1 must be NATs.  Push
;                       their NAT sum.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{p-add-nat-okp} \\  
\=\+{\rm{p-add-nat-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-add-nat-okp} \\ 
$=$$\;\;\;\;$(\=\+{\rm{listp}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk}) \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\rm{pop}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{pop}) \\ 
$\wedge$$\;\;\;\;${\rm{p-objectp-type}}\,({\tt{'}}{\tt{nat}}, {\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top}, {\it{p\/}})\index{p-objectp-type} \\ 
$\wedge$$\;\;\;\;${\rm{p-objectp-type}}\,({\tt{'}}{\tt{nat}}, {\rm{top1}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top1}, {\it{p\/}})\index{p-objectp-type} \\ 
$\wedge$$\;\;\;\;${\rm{small-naturalp}}\,(\=\+\=\+{\rm{untag}}\,({\rm{top1}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top1})\index{untag} \\ 
$+$$\;\;\;\;${\rm{untag}}\,({\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top})\index{untag}\-, \\ 
{\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size})\-\index{small-naturalp})\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-add-nat-step} \\  
\=\+{\rm{p-add-nat-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-add-nat-step} \\ 
$=$$\;\;\;\;$\=\+{\bf let }\=\+{\it{sum\/}}{\bf $\;$ be$\;\;$}\=\+{\rm{untag}}\,({\rm{top1}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top1})\index{untag} \\ 
$+$$\;\;\;\;${\rm{untag}}\,({\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top})\index{untag}\-\- \\ 
{\bf in} \\ 
{\rm{p-state}}\,(\=\+{\rm{add1-p-pc}}\,({\it{p\/}})\index{add1-p-pc}, \\ 
{\rm{p-ctrl-stk}}\,({\it{p\/}})\index{p-ctrl-stk}, \\ 
{\rm{push}}\,({\rm{tag}}\,({\tt{'}}{\tt{nat}}, {\it{sum\/}})\index{tag}, {\rm{pop}}\,({\rm{pop}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{pop})\index{pop})\index{push}, \\ 
{\rm{p-prog-segment}}\,({\it{p\/}})\index{p-prog-segment}, \\ 
{\rm{p-data-segment}}\,({\it{p\/}})\index{p-data-segment}, \\ 
{\rm{p-max-ctrl-stk-size}}\,({\it{p\/}})\index{p-max-ctrl-stk-size}, \\ 
{\rm{p-max-temp-stk-size}}\,({\it{p\/}})\index{p-max-temp-stk-size}, \\ 
{\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state}$\;${\bf  endlet}\-\-
\end{tabbing}

\begin{verbatim};   (SUB-NAT)           Pop top, top1 off of temp-stk.
;                       Both top and top1 must be NATs.
;                       If top1 >= top
;                          then push top1-top.
;                       Else, error.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{p-sub-nat-okp} \\  
\=\+{\rm{p-sub-nat-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-sub-nat-okp} \\ 
$=$$\;\;\;\;$(\=\+{\rm{listp}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk}) \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\rm{pop}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{pop}) \\ 
$\wedge$$\;\;\;\;${\rm{p-objectp-type}}\,({\tt{'}}{\tt{nat}}, {\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top}, {\it{p\/}})\index{p-objectp-type} \\ 
$\wedge$$\;\;\;\;${\rm{p-objectp-type}}\,({\tt{'}}{\tt{nat}}, {\rm{top1}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top1}, {\it{p\/}})\index{p-objectp-type} \\ 
$\wedge$$\;\;\;\;$({\rm{untag}}\,({\rm{top1}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top1})\index{untag} $\not<$ {\rm{untag}}\,({\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top})\index{untag}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-sub-nat-step} \\  
\=\+{\rm{p-sub-nat-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-sub-nat-step} \\ 
$=$$\;\;\;\;$\=\+{\bf let }\=\+{\it{y\/}}{\bf $\;$ be$\;\;$}{\rm{untag}}\,({\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top})\index{untag}, \\ 
{\it{x\/}}{\bf $\;$ be$\;\;$}{\rm{untag}}\,({\rm{top1}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top1})\index{untag}\- \\ 
{\bf in} \\ 
{\rm{p-state}}\,(\=\+{\rm{add1-p-pc}}\,({\it{p\/}})\index{add1-p-pc}, \\ 
{\rm{p-ctrl-stk}}\,({\it{p\/}})\index{p-ctrl-stk}, \\ 
{\rm{push}}\,({\rm{tag}}\,({\tt{'}}{\tt{nat}}, {\it{x\/}} $-$ {\it{y\/}})\index{tag}, {\rm{pop}}\,({\rm{pop}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{pop})\index{pop})\index{push}, \\ 
{\rm{p-prog-segment}}\,({\it{p\/}})\index{p-prog-segment}, \\ 
{\rm{p-data-segment}}\,({\it{p\/}})\index{p-data-segment}, \\ 
{\rm{p-max-ctrl-stk-size}}\,({\it{p\/}})\index{p-max-ctrl-stk-size}, \\ 
{\rm{p-max-temp-stk-size}}\,({\it{p\/}})\index{p-max-temp-stk-size}, \\ 
{\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state}$\;${\bf  endlet}\-\-
\end{tabbing}

\begin{verbatim};   (SUB1-NAT)          Pop top off of temp-stk.
;                       Top must be a NAT other than
;                       0.  Push top-1.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{p-sub1-nat-okp} \\  
\=\+{\rm{p-sub1-nat-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-sub1-nat-okp} \\ 
$=$$\;\;\;\;$(\=\+{\rm{listp}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk}) \\ 
$\wedge$$\;\;\;\;${\rm{p-objectp-type}}\,({\tt{'}}{\tt{nat}}, {\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top}, {\it{p\/}})\index{p-objectp-type} \\ 
$\wedge$$\;\;\;\;$({\rm{untag}}\,({\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top})\index{untag} $\not\simeq {\tt{0}}$))\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-sub1-nat-step} \\  
\=\+{\rm{p-sub1-nat-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-sub1-nat-step} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{add1-p-pc}}\,({\it{p\/}})\index{add1-p-pc}, \\ 
{\rm{p-ctrl-stk}}\,({\it{p\/}})\index{p-ctrl-stk}, \\ 
{\rm{push}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{nat}}, {\rm{untag}}\,({\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top})\index{untag} $-\;1$)\index{tag}, \\ 
{\rm{pop}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{pop})\-\index{push}, \\ 
{\rm{p-prog-segment}}\,({\it{p\/}})\index{p-prog-segment}, \\ 
{\rm{p-data-segment}}\,({\it{p\/}})\index{p-data-segment}, \\ 
{\rm{p-max-ctrl-stk-size}}\,({\it{p\/}})\index{p-max-ctrl-stk-size}, \\ 
{\rm{p-max-temp-stk-size}}\,({\it{p\/}})\index{p-max-temp-stk-size}, \\ 
{\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state}\-
\end{tabbing}

\begin{verbatim};   (OR-BOOL)           Pop top and top1 off of temp-stk, or them together
;                       and push the result.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{p-or-bool-okp} \\  
\=\+{\rm{p-or-bool-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-or-bool-okp} \\ 
$=$$\;\;\;\;$(\=\+{\rm{listp}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk}) \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\rm{pop}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{pop}) \\ 
$\wedge$$\;\;\;\;${\rm{p-objectp-type}}\,({\tt{'}}{\tt{bool}}, {\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top}, {\it{p\/}})\index{p-objectp-type} \\ 
$\wedge$$\;\;\;\;${\rm{p-objectp-type}}\,({\tt{'}}{\tt{bool}}, {\rm{top1}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top1}, {\it{p\/}})\index{p-objectp-type})\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-or-bool-step} \\  
\=\+{\rm{p-or-bool-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-or-bool-step} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{add1-p-pc}}\,({\it{p\/}})\index{add1-p-pc}, \\ 
{\rm{p-ctrl-stk}}\,({\it{p\/}})\index{p-ctrl-stk}, \\ 
{\rm{push}}\,(\=\+{\rm{tag}}\,(\=\+{\tt{'}}{\tt{bool}}, \\ 
{\rm{or-bool}}\,(\=\+{\rm{untag}}\,({\rm{top1}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top1})\index{untag}, \\ 
{\rm{untag}}\,({\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top})\index{untag})\-\index{or-bool})\-\index{tag}, \\ 
{\rm{pop}}\,({\rm{pop}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{pop})\index{pop})\-\index{push}, \\ 
{\rm{p-prog-segment}}\,({\it{p\/}})\index{p-prog-segment}, \\ 
{\rm{p-data-segment}}\,({\it{p\/}})\index{p-data-segment}, \\ 
{\rm{p-max-ctrl-stk-size}}\,({\it{p\/}})\index{p-max-ctrl-stk-size}, \\ 
{\rm{p-max-temp-stk-size}}\,({\it{p\/}})\index{p-max-temp-stk-size}, \\ 
{\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state}\-
\end{tabbing}

\begin{verbatim};   (AND-BOOL)          Pop top and top1 off of temp-stk, and them together
;                       and push the result.
;                       

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{p-and-bool-okp} \\  
\=\+{\rm{p-and-bool-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-and-bool-okp} \\ 
$=$$\;\;\;\;$(\=\+{\rm{listp}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk}) \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\rm{pop}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{pop}) \\ 
$\wedge$$\;\;\;\;${\rm{p-objectp-type}}\,({\tt{'}}{\tt{bool}}, {\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top}, {\it{p\/}})\index{p-objectp-type} \\ 
$\wedge$$\;\;\;\;${\rm{p-objectp-type}}\,({\tt{'}}{\tt{bool}}, {\rm{top1}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top1}, {\it{p\/}})\index{p-objectp-type})\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-and-bool-step} \\  
\=\+{\rm{p-and-bool-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-and-bool-step} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{add1-p-pc}}\,({\it{p\/}})\index{add1-p-pc}, \\ 
{\rm{p-ctrl-stk}}\,({\it{p\/}})\index{p-ctrl-stk}, \\ 
{\rm{push}}\,(\=\+{\rm{tag}}\,(\=\+{\tt{'}}{\tt{bool}}, \\ 
{\rm{and-bool}}\,(\=\+{\rm{untag}}\,({\rm{top1}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top1})\index{untag}, \\ 
{\rm{untag}}\,({\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top})\index{untag})\-\index{and-bool})\-\index{tag}, \\ 
{\rm{pop}}\,({\rm{pop}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{pop})\index{pop})\-\index{push}, \\ 
{\rm{p-prog-segment}}\,({\it{p\/}})\index{p-prog-segment}, \\ 
{\rm{p-data-segment}}\,({\it{p\/}})\index{p-data-segment}, \\ 
{\rm{p-max-ctrl-stk-size}}\,({\it{p\/}})\index{p-max-ctrl-stk-size}, \\ 
{\rm{p-max-temp-stk-size}}\,({\it{p\/}})\index{p-max-temp-stk-size}, \\ 
{\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state}\-
\end{tabbing}

\begin{verbatim};   (NOT-BOOL)          Pop top of temp-stk, not it, and push the result.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{p-not-bool-okp} \\  
\=\+{\rm{p-not-bool-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-not-bool-okp} \\ 
$=$$\;\;\;\;$(\=\+{\rm{listp}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk}) \\ 
$\wedge$$\;\;\;\;${\rm{p-objectp-type}}\,({\tt{'}}{\tt{bool}}, {\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top}, {\it{p\/}})\index{p-objectp-type})\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{p-not-bool-step} \\  
\=\+{\rm{p-not-bool-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-not-bool-step} \\ 
$=$$\;\;\;\;${\rm{p-state}}\,(\=\+{\rm{add1-p-pc}}\,({\it{p\/}})\index{add1-p-pc}, \\ 
{\rm{p-ctrl-stk}}\,({\it{p\/}})\index{p-ctrl-stk}, \\ 
{\rm{push}}\,(\=\+{\rm{tag}}\,({\tt{'}}{\tt{bool}}, {\rm{not-bool}}\,({\rm{untag}}\,({\rm{top}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{top})\index{untag})\index{not-bool})\index{tag}, \\ 
{\rm{pop}}\,({\rm{p-temp-stk}}\,({\it{p\/}})\index{p-temp-stk})\index{pop})\-\index{push}, \\ 
{\rm{p-prog-segment}}\,({\it{p\/}})\index{p-prog-segment}, \\ 
{\rm{p-data-segment}}\,({\it{p\/}})\index{p-data-segment}, \\ 
{\rm{p-max-ctrl-stk-size}}\,({\it{p\/}})\index{p-max-ctrl-stk-size}, \\ 
{\rm{p-max-temp-stk-size}}\,({\it{p\/}})\index{p-max-temp-stk-size}, \\ 
{\rm{p-word-size}}\,({\it{p\/}})\index{p-word-size}, \\ 
{\tt{'}}{\tt{run}})\-\index{p-state}\-
\end{tabbing}

\begin{verbatim};;(defn piton-opcodes nil
;;  '(call ret push-constant push-local push-global
;;    push-temp-stk-index pop pop* pop-local pop-global
;;    fetch-temp-stk deposit-temp-stk jump jump-case set-local
;;    test-nat-and-jump test-int-and-jump test-bool-and-jump no-op
;;    eq add-int-with-carry sub-int sub-int-with-carry neg-int
;;    lt-int int-to-nat add-nat sub-nat sub1-nat lt-nat or-bool and-bool
;;    not-bool))

; The following function generates the name of the error
; message produced when an illegal instruction is hit.  The
; first argument is the ``level'' name, e.g., 'P or 'R.
; the (cdr (unpack 'g-instruction)) is used instead of
; (unpack '-instruction) only because '-instruction is an
; illegal evg in the logic, since it does not start with an
; alphabetic character.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{x-y-error-msg} \\  
\=\+{\rm{x-y-error-msg}}\,({\it{x\/}}, {\it{y\/}})\index{x-y-error-msg} \\ 
$=$$\;\;\;\;${\rm{pack}}\,({\rm{append}}\,(\=\+{\rm{unpack}}\,({\tt{'}}{\tt{illegal-}}), \\ 
{\rm{append}}\,({\rm{unpack}}\,({\it{y\/}}), {\rm{cdr}}\,({\rm{unpack}}\,({\tt{'}}{\tt{g-instruction}}))))\-)\-
\end{tabbing}

\begin{verbatim}; The function checks that it is legal to execute ins in state
; p:

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{p-ins-okp} \\  
\=\+{\rm{p-ins-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-ins-okp} \\ 
$=$$\;\;\;\;$\=\+{\bf case on }{\rm{car}}\,({\it{ins\/}}): \\ 
{\bf case = }{\it{call\/}} \\ 
{\bf then }{\rm{p-call-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-call-okp} \\ 
{\bf case = }{\it{ret\/}} \\ 
{\bf $\;\;$then }{\rm{p-ret-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-ret-okp} \\ 
{\bf case = }{\it{push-constant\/}} \\ 
{\bf $\;\;$then }{\rm{p-push-constant-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-push-constant-okp} \\ 
{\bf case = }{\it{push-local\/}} \\ 
{\bf $\;\;$then }{\rm{p-push-local-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-push-local-okp} \\ 
{\bf case = }{\it{push-global\/}} \\ 
{\bf $\;\;$then }{\rm{p-push-global-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-push-global-okp} \\ 
{\bf case = }{\it{push-temp-stk-index\/}} \\ 
{\bf $\;\;$then }{\rm{p-push-temp-stk-index-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-push-temp-stk-index-okp} \\ 
{\bf case = }{\it{pop\/}} \\ 
{\bf $\;\;$then }{\rm{p-pop-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-pop-okp} \\ 
{\bf case = }{\it{pop*\/}} \\ 
{\bf $\;\;$then }{\rm{p-pop*-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-pop*-okp} \\ 
{\bf case = }{\it{pop-local\/}} \\ 
{\bf $\;\;$then }{\rm{p-pop-local-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-pop-local-okp} \\ 
{\bf case = }{\it{pop-global\/}} \\ 
{\bf $\;\;$then }{\rm{p-pop-global-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-pop-global-okp} \\ 
{\bf case = }{\it{fetch-temp-stk\/}} \\ 
{\bf $\;\;$then }{\rm{p-fetch-temp-stk-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-fetch-temp-stk-okp} \\ 
{\bf case = }{\it{deposit-temp-stk\/}} \\ 
{\bf $\;\;$then }{\rm{p-deposit-temp-stk-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-deposit-temp-stk-okp} \\ 
{\bf case = }{\it{jump\/}} \\ 
{\bf $\;\;$then }{\rm{p-jump-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-jump-okp} \\ 
{\bf case = }{\it{jump-case\/}} \\ 
{\bf $\;\;$then }{\rm{p-jump-case-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-jump-case-okp} \\ 
{\bf case = }{\it{set-local\/}} \\ 
{\bf $\;\;$then }{\rm{p-set-local-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-set-local-okp} \\ 
{\bf case = }{\it{test-nat-and-jump\/}} \\ 
{\bf $\;\;$then }{\rm{p-test-nat-and-jump-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-test-nat-and-jump-okp} \\ 
{\bf case = }{\it{test-int-and-jump\/}} \\ 
{\bf $\;\;$then }{\rm{p-test-int-and-jump-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-test-int-and-jump-okp} \\ 
{\bf case = }{\it{test-bool-and-jump\/}} \\ 
{\bf $\;\;$then }{\rm{p-test-bool-and-jump-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-test-bool-and-jump-okp} \\ 
{\bf case = }{\it{no-op\/}} \\ 
{\bf $\;\;$then }{\rm{p-no-op-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-no-op-okp} \\ 
{\bf case = }{\it{eq\/}} \\ 
{\bf $\;\;$then }{\rm{p-eq-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-eq-okp} \\ 
{\bf case = }{\it{add-int-with-carry\/}} \\ 
{\bf $\;\;$then }{\rm{p-add-int-with-carry-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-add-int-with-carry-okp} \\ 
{\bf case = }{\it{sub-int\/}} \\ 
{\bf $\;\;$then }{\rm{p-sub-int-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-sub-int-okp} \\ 
{\bf case = }{\it{sub-int-with-carry\/}} \\ 
{\bf $\;\;$then }{\rm{p-sub-int-with-carry-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-sub-int-with-carry-okp} \\ 
{\bf case = }{\it{neg-int\/}} \\ 
{\bf $\;\;$then }{\rm{p-neg-int-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-neg-int-okp} \\ 
{\bf case = }{\it{lt-int\/}} \\ 
{\bf $\;\;$then }{\rm{p-lt-int-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-lt-int-okp} \\ 
{\bf case = }{\it{int-to-nat\/}} \\ 
{\bf $\;\;$then }{\rm{p-int-to-nat-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-int-to-nat-okp} \\ 
{\bf case = }{\it{add-nat\/}} \\ 
{\bf $\;\;$then }{\rm{p-add-nat-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-add-nat-okp} \\ 
{\bf case = }{\it{sub-nat\/}} \\ 
{\bf $\;\;$then }{\rm{p-sub-nat-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-sub-nat-okp} \\ 
{\bf case = }{\it{sub1-nat\/}} \\ 
{\bf $\;\;$then }{\rm{p-sub1-nat-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-sub1-nat-okp} \\ 
{\bf case = }{\it{or-bool\/}} \\ 
{\bf $\;\;$then }{\rm{p-or-bool-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-or-bool-okp} \\ 
{\bf case = }{\it{and-bool\/}} \\ 
{\bf $\;\;$then }{\rm{p-and-bool-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-and-bool-okp} \\ 
{\bf case = }{\it{not-bool\/}} \\ 
{\bf $\;\;$then }{\rm{p-not-bool-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-not-bool-okp} \\ 
{\bf otherwise }{\bf{f}}$\;${\bf  endcase}\-\-
\end{tabbing}

\begin{verbatim}; If ins is legal, the following function steps the state forward one.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{p-ins-step} \\  
\=\+{\rm{p-ins-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-ins-step} \\ 
$=$$\;\;\;\;$\=\+{\bf case on }{\rm{car}}\,({\it{ins\/}}): \\ 
{\bf case = }{\it{call\/}} \\ 
{\bf then }{\rm{p-call-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-call-step} \\ 
{\bf case = }{\it{ret\/}} \\ 
{\bf $\;\;$then }{\rm{p-ret-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-ret-step} \\ 
{\bf case = }{\it{push-constant\/}} \\ 
{\bf $\;\;$then }{\rm{p-push-constant-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-push-constant-step} \\ 
{\bf case = }{\it{push-local\/}} \\ 
{\bf $\;\;$then }{\rm{p-push-local-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-push-local-step} \\ 
{\bf case = }{\it{push-global\/}} \\ 
{\bf $\;\;$then }{\rm{p-push-global-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-push-global-step} \\ 
{\bf case = }{\it{push-temp-stk-index\/}} \\ 
{\bf $\;\;$then }{\rm{p-push-temp-stk-index-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-push-temp-stk-index-step} \\ 
{\bf case = }{\it{pop\/}} \\ 
{\bf $\;\;$then }{\rm{p-pop-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-pop-step} \\ 
{\bf case = }{\it{pop*\/}} \\ 
{\bf $\;\;$then }{\rm{p-pop*-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-pop*-step} \\ 
{\bf case = }{\it{pop-local\/}} \\ 
{\bf $\;\;$then }{\rm{p-pop-local-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-pop-local-step} \\ 
{\bf case = }{\it{pop-global\/}} \\ 
{\bf $\;\;$then }{\rm{p-pop-global-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-pop-global-step} \\ 
{\bf case = }{\it{fetch-temp-stk\/}} \\ 
{\bf $\;\;$then }{\rm{p-fetch-temp-stk-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-fetch-temp-stk-step} \\ 
{\bf case = }{\it{deposit-temp-stk\/}} \\ 
{\bf $\;\;$then }{\rm{p-deposit-temp-stk-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-deposit-temp-stk-step} \\ 
{\bf case = }{\it{jump\/}} \\ 
{\bf $\;\;$then }{\rm{p-jump-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-jump-step} \\ 
{\bf case = }{\it{jump-case\/}} \\ 
{\bf $\;\;$then }{\rm{p-jump-case-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-jump-case-step} \\ 
{\bf case = }{\it{set-local\/}} \\ 
{\bf $\;\;$then }{\rm{p-set-local-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-set-local-step} \\ 
{\bf case = }{\it{test-nat-and-jump\/}} \\ 
{\bf $\;\;$then }{\rm{p-test-nat-and-jump-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-test-nat-and-jump-step} \\ 
{\bf case = }{\it{test-int-and-jump\/}} \\ 
{\bf $\;\;$then }{\rm{p-test-int-and-jump-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-test-int-and-jump-step} \\ 
{\bf case = }{\it{test-bool-and-jump\/}} \\ 
{\bf $\;\;$then }{\rm{p-test-bool-and-jump-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-test-bool-and-jump-step} \\ 
{\bf case = }{\it{no-op\/}} \\ 
{\bf $\;\;$then }{\rm{p-no-op-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-no-op-step} \\ 
{\bf case = }{\it{eq\/}} \\ 
{\bf $\;\;$then }{\rm{p-eq-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-eq-step} \\ 
{\bf case = }{\it{add-int-with-carry\/}} \\ 
{\bf $\;\;$then }{\rm{p-add-int-with-carry-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-add-int-with-carry-step} \\ 
{\bf case = }{\it{sub-int\/}} \\ 
{\bf $\;\;$then }{\rm{p-sub-int-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-sub-int-step} \\ 
{\bf case = }{\it{sub-int-with-carry\/}} \\ 
{\bf $\;\;$then }{\rm{p-sub-int-with-carry-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-sub-int-with-carry-step} \\ 
{\bf case = }{\it{neg-int\/}} \\ 
{\bf $\;\;$then }{\rm{p-neg-int-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-neg-int-step} \\ 
{\bf case = }{\it{lt-int\/}} \\ 
{\bf $\;\;$then }{\rm{p-lt-int-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-lt-int-step} \\ 
{\bf case = }{\it{int-to-nat\/}} \\ 
{\bf $\;\;$then }{\rm{p-int-to-nat-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-int-to-nat-step} \\ 
{\bf case = }{\it{add-nat\/}} \\ 
{\bf $\;\;$then }{\rm{p-add-nat-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-add-nat-step} \\ 
{\bf case = }{\it{sub-nat\/}} \\ 
{\bf $\;\;$then }{\rm{p-sub-nat-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-sub-nat-step} \\ 
{\bf case = }{\it{sub1-nat\/}} \\ 
{\bf $\;\;$then }{\rm{p-sub1-nat-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-sub1-nat-step} \\ 
{\bf case = }{\it{or-bool\/}} \\ 
{\bf $\;\;$then }{\rm{p-or-bool-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-or-bool-step} \\ 
{\bf case = }{\it{and-bool\/}} \\ 
{\bf $\;\;$then }{\rm{p-and-bool-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-and-bool-step} \\ 
{\bf case = }{\it{not-bool\/}} \\ 
{\bf $\;\;$then }{\rm{p-not-bool-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-not-bool-step} \\ 
{\bf otherwise }{\rm{p-halt}}\,({\it{p\/}}, {\tt{'}}{\tt{run}})\index{p-halt}$\;${\bf  endcase}\-\-
\end{tabbing}

\begin{verbatim}; We now package these up into a single function that takes an
; instruction and a state and returns the result of executing the
; given instruction in the state or causing an error.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{p-step1} \\  
\=\+{\rm{p-step1}}\,({\it{ins\/}}, {\it{p\/}})\index{p-step1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{p-ins-okp}}\,({\it{ins\/}}, {\it{p\/}})\index{p-ins-okp}$\;\;${\bf then }{\rm{p-ins-step}}\,({\it{ins\/}}, {\it{p\/}})\index{p-ins-step} \\ 
{\bf else }{\rm{p-halt}}\,({\it{p\/}}, {\rm{x-y-error-msg}}\,({\tt{'}}{\tt{p}}, {\rm{car}}\,({\it{ins\/}}))\index{x-y-error-msg})\index{p-halt}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; Of course, we are only interested in executing the current
; instruction of a state.  That is what we call stepping the state.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{p-step} \\  
\=\+{\rm{p-step}}\,({\it{p\/}})\index{p-step} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{p-psw}}\,({\it{p\/}})\index{p-psw} $=$ {\tt{'}}{\tt{run}}$\;\;${\bf then }{\rm{p-step1}}\,({\rm{p-current-instruction}}\,({\it{p\/}})\index{p-current-instruction}, {\it{p\/}})\index{p-step1} \\ 
{\bf else }{\it{p\/}}$\;${\bf  endif}\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable p-step.

\addvspace{18pt}

\begin{verbatim}; Note that p-step is a no-op if the psw is anything besides RUN.

; And given the ability to step a state, here is how you step it n
; times.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{p} \\  
\=\+{\rm{p}}\,({\it{p\/}}, {\it{n\/}})\index{p} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\it{p\/}} \\ 
{\bf else }{\rm{p}}\,({\rm{p-step}}\,({\it{p\/}})\index{p-step}, {\it{n\/}} $-\;1$)\index{p}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                             ;;
;;                       Lemmas on Piton                       ;;
;;                                                             ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

\end{verbatim}
\noindent{\sc Event}:   Disable p-step.

\addvspace{18pt}

\noindent{\sc Event}:   Disable p-halt.

\addvspace{18pt}

\noindent{\sc Event}:   Disable p-ins-step.

\addvspace{18pt}

\noindent{\sc Event}:   Disable p-ins-okp.

\addvspace{18pt}

\noindent{\sc Event}:   Disable p-step1.

\addvspace{18pt}

\noindent{\sc Event}:   Disable x-y-error-msg.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  p-step-expansion \\ \index{p-step-expansion}
\=\+{\rm{p-step}}\,({\rm{p-state}}\,(\=\+{\it{pc\/}}, \\ 
{\it{ctr-stk\/}}, \\ 
{\it{temp-stk\/}}, \\ 
{\it{prog-seg\/}}, \\ 
{\it{data-seg\/}}, \\ 
{\it{p-max-ctrl-stk-size\/}}, \\ 
{\it{p-max-temp-stk-size\/}}, \\ 
{\it{p-word-size\/}}, \\ 
{\it{psw\/}})\-\index{p-state})\index{p-step} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{psw\/}} $=$ {\tt{'}}{\tt{run}} \\ 
{\bf then }{\rm{p-step1}}\,(\=\+{\rm{p-current-instruction}}\,({\rm{p-state}}\,(\=\+{\it{pc\/}}, \\ 
{\it{ctr-stk\/}}, \\ 
{\it{temp-stk\/}}, \\ 
{\it{prog-seg\/}}, \\ 
{\it{data-seg\/}}, \\ 
{\it{p-max-ctrl-stk-size\/}}, \\ 
{\it{p-max-temp-stk-size\/}}, \\ 
{\it{p-word-size\/}}, \\ 
{\it{psw\/}})\-\index{p-state})\index{p-current-instruction}, \\ 
{\rm{p-state}}\,(\=\+{\it{pc\/}}, \\ 
{\it{ctr-stk\/}}, \\ 
{\it{temp-stk\/}}, \\ 
{\it{prog-seg\/}}, \\ 
{\it{data-seg\/}}, \\ 
{\it{p-max-ctrl-stk-size\/}}, \\ 
{\it{p-max-temp-stk-size\/}}, \\ 
{\it{p-word-size\/}}, \\ 
{\it{psw\/}})\-\index{p-state})\-\index{p-step1} \\ 
{\bf else }{\rm{p-state}}\,(\=\+{\it{pc\/}}, \\ 
{\it{ctr-stk\/}}, \\ 
{\it{temp-stk\/}}, \\ 
{\it{prog-seg\/}}, \\ 
{\it{data-seg\/}}, \\ 
{\it{p-max-ctrl-stk-size\/}}, \\ 
{\it{p-max-temp-stk-size\/}}, \\ 
{\it{p-word-size\/}}, \\ 
{\it{psw\/}})\-\index{p-state}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  p-ins-step-expansion \\ \index{p-ins-step-expansion}
\=\+{\rm{p-ins-step}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-ins-step} \\ 
$=$$\;\;\;\;$\=\+{\bf case on }{\rm{pack}}\,({\it{opr\/}}): \\ 
{\bf case = }{\it{call\/}} \\ 
{\bf then }{\rm{p-call-step}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-call-step} \\ 
{\bf case = }{\it{ret\/}} \\ 
{\bf $\;\;$then }{\rm{p-ret-step}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-ret-step} \\ 
{\bf case = }{\it{push-constant\/}} \\ 
{\bf $\;\;$then }{\rm{p-push-constant-step}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-push-constant-step} \\ 
{\bf case = }{\it{push-local\/}} \\ 
{\bf $\;\;$then }{\rm{p-push-local-step}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-push-local-step} \\ 
{\bf case = }{\it{push-global\/}} \\ 
{\bf $\;\;$then }{\rm{p-push-global-step}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-push-global-step} \\ 
{\bf case = }{\it{push-temp-stk-index\/}} \\ 
{\bf $\;\;$then }{\rm{p-push-temp-stk-index-step}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-push-temp-stk-index-step} \\ 
{\bf case = }{\it{pop\/}} \\ 
{\bf $\;\;$then }{\rm{p-pop-step}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-pop-step} \\ 
{\bf case = }{\it{pop*\/}} \\ 
{\bf $\;\;$then }{\rm{p-pop*-step}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-pop*-step} \\ 
{\bf case = }{\it{pop-local\/}} \\ 
{\bf $\;\;$then }{\rm{p-pop-local-step}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-pop-local-step} \\ 
{\bf case = }{\it{pop-global\/}} \\ 
{\bf $\;\;$then }{\rm{p-pop-global-step}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-pop-global-step} \\ 
{\bf case = }{\it{fetch-temp-stk\/}} \\ 
{\bf $\;\;$then }{\rm{p-fetch-temp-stk-step}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-fetch-temp-stk-step} \\ 
{\bf case = }{\it{deposit-temp-stk\/}} \\ 
{\bf $\;\;$then }{\rm{p-deposit-temp-stk-step}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-deposit-temp-stk-step} \\ 
{\bf case = }{\it{jump\/}} \\ 
{\bf $\;\;$then }{\rm{p-jump-step}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-jump-step} \\ 
{\bf case = }{\it{jump-case\/}} \\ 
{\bf $\;\;$then }{\rm{p-jump-case-step}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-jump-case-step} \\ 
{\bf case = }{\it{set-local\/}} \\ 
{\bf $\;\;$then }{\rm{p-set-local-step}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-set-local-step} \\ 
{\bf case = }{\it{test-nat-and-jump\/}} \\ 
{\bf $\;\;$then }{\rm{p-test-nat-and-jump-step}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-test-nat-and-jump-step} \\ 
{\bf case = }{\it{test-int-and-jump\/}} \\ 
{\bf $\;\;$then }{\rm{p-test-int-and-jump-step}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-test-int-and-jump-step} \\ 
{\bf case = }{\it{test-bool-and-jump\/}} \\ 
{\bf $\;\;$then }{\rm{p-test-bool-and-jump-step}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-test-bool-and-jump-step} \\ 
{\bf case = }{\it{no-op\/}} \\ 
{\bf $\;\;$then }{\rm{p-no-op-step}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-no-op-step} \\ 
{\bf case = }{\it{eq\/}} \\ 
{\bf $\;\;$then }{\rm{p-eq-step}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-eq-step} \\ 
{\bf case = }{\it{add-int-with-carry\/}} \\ 
{\bf $\;\;$then }{\rm{p-add-int-with-carry-step}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-add-int-with-carry-step} \\ 
{\bf case = }{\it{sub-int\/}} \\ 
{\bf $\;\;$then }{\rm{p-sub-int-step}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-sub-int-step} \\ 
{\bf case = }{\it{sub-int-with-carry\/}} \\ 
{\bf $\;\;$then }{\rm{p-sub-int-with-carry-step}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-sub-int-with-carry-step} \\ 
{\bf case = }{\it{neg-int\/}} \\ 
{\bf $\;\;$then }{\rm{p-neg-int-step}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-neg-int-step} \\ 
{\bf case = }{\it{lt-int\/}} \\ 
{\bf $\;\;$then }{\rm{p-lt-int-step}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-lt-int-step} \\ 
{\bf case = }{\it{int-to-nat\/}} \\ 
{\bf $\;\;$then }{\rm{p-int-to-nat-step}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-int-to-nat-step} \\ 
{\bf case = }{\it{add-nat\/}} \\ 
{\bf $\;\;$then }{\rm{p-add-nat-step}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-add-nat-step} \\ 
{\bf case = }{\it{sub-nat\/}} \\ 
{\bf $\;\;$then }{\rm{p-sub-nat-step}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-sub-nat-step} \\ 
{\bf case = }{\it{sub1-nat\/}} \\ 
{\bf $\;\;$then }{\rm{p-sub1-nat-step}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-sub1-nat-step} \\ 
{\bf case = }{\it{or-bool\/}} \\ 
{\bf $\;\;$then }{\rm{p-or-bool-step}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-or-bool-step} \\ 
{\bf case = }{\it{and-bool\/}} \\ 
{\bf $\;\;$then }{\rm{p-and-bool-step}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-and-bool-step} \\ 
{\bf case = }{\it{not-bool\/}} \\ 
{\bf $\;\;$then }{\rm{p-not-bool-step}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-not-bool-step} \\ 
{\bf otherwise }{\rm{p-halt}}\,({\it{p\/}}, {\tt{'}}{\tt{run}})\index{p-halt}$\;${\bf  endcase}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  p-ins-okp-expansion \\ \index{p-ins-okp-expansion}
\=\+{\rm{p-ins-okp}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-ins-okp} \\ 
$=$$\;\;\;\;$\=\+{\bf case on }{\rm{pack}}\,({\it{opr\/}}): \\ 
{\bf case = }{\it{call\/}} \\ 
{\bf then }{\rm{p-call-okp}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-call-okp} \\ 
{\bf case = }{\it{ret\/}} \\ 
{\bf $\;\;$then }{\rm{p-ret-okp}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-ret-okp} \\ 
{\bf case = }{\it{push-constant\/}} \\ 
{\bf $\;\;$then }{\rm{p-push-constant-okp}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-push-constant-okp} \\ 
{\bf case = }{\it{push-local\/}} \\ 
{\bf $\;\;$then }{\rm{p-push-local-okp}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-push-local-okp} \\ 
{\bf case = }{\it{push-global\/}} \\ 
{\bf $\;\;$then }{\rm{p-push-global-okp}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-push-global-okp} \\ 
{\bf case = }{\it{push-temp-stk-index\/}} \\ 
{\bf $\;\;$then }{\rm{p-push-temp-stk-index-okp}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-push-temp-stk-index-okp} \\ 
{\bf case = }{\it{pop\/}} \\ 
{\bf $\;\;$then }{\rm{p-pop-okp}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-pop-okp} \\ 
{\bf case = }{\it{pop*\/}} \\ 
{\bf $\;\;$then }{\rm{p-pop*-okp}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-pop*-okp} \\ 
{\bf case = }{\it{pop-local\/}} \\ 
{\bf $\;\;$then }{\rm{p-pop-local-okp}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-pop-local-okp} \\ 
{\bf case = }{\it{pop-global\/}} \\ 
{\bf $\;\;$then }{\rm{p-pop-global-okp}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-pop-global-okp} \\ 
{\bf case = }{\it{fetch-temp-stk\/}} \\ 
{\bf $\;\;$then }{\rm{p-fetch-temp-stk-okp}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-fetch-temp-stk-okp} \\ 
{\bf case = }{\it{deposit-temp-stk\/}} \\ 
{\bf $\;\;$then }{\rm{p-deposit-temp-stk-okp}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-deposit-temp-stk-okp} \\ 
{\bf case = }{\it{jump\/}} \\ 
{\bf $\;\;$then }{\rm{p-jump-okp}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-jump-okp} \\ 
{\bf case = }{\it{jump-case\/}} \\ 
{\bf $\;\;$then }{\rm{p-jump-case-okp}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-jump-case-okp} \\ 
{\bf case = }{\it{set-local\/}} \\ 
{\bf $\;\;$then }{\rm{p-set-local-okp}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-set-local-okp} \\ 
{\bf case = }{\it{test-nat-and-jump\/}} \\ 
{\bf $\;\;$then }{\rm{p-test-nat-and-jump-okp}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-test-nat-and-jump-okp} \\ 
{\bf case = }{\it{test-int-and-jump\/}} \\ 
{\bf $\;\;$then }{\rm{p-test-int-and-jump-okp}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-test-int-and-jump-okp} \\ 
{\bf case = }{\it{test-bool-and-jump\/}} \\ 
{\bf $\;\;$then }{\rm{p-test-bool-and-jump-okp}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-test-bool-and-jump-okp} \\ 
{\bf case = }{\it{no-op\/}} \\ 
{\bf $\;\;$then }{\rm{p-no-op-okp}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-no-op-okp} \\ 
{\bf case = }{\it{eq\/}} \\ 
{\bf $\;\;$then }{\rm{p-eq-okp}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-eq-okp} \\ 
{\bf case = }{\it{add-int-with-carry\/}} \\ 
{\bf $\;\;$then }{\rm{p-add-int-with-carry-okp}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-add-int-with-carry-okp} \\ 
{\bf case = }{\it{sub-int\/}} \\ 
{\bf $\;\;$then }{\rm{p-sub-int-okp}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-sub-int-okp} \\ 
{\bf case = }{\it{sub-int-with-carry\/}} \\ 
{\bf $\;\;$then }{\rm{p-sub-int-with-carry-okp}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-sub-int-with-carry-okp} \\ 
{\bf case = }{\it{neg-int\/}} \\ 
{\bf $\;\;$then }{\rm{p-neg-int-okp}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-neg-int-okp} \\ 
{\bf case = }{\it{lt-int\/}} \\ 
{\bf $\;\;$then }{\rm{p-lt-int-okp}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-lt-int-okp} \\ 
{\bf case = }{\it{int-to-nat\/}} \\ 
{\bf $\;\;$then }{\rm{p-int-to-nat-okp}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-int-to-nat-okp} \\ 
{\bf case = }{\it{add-nat\/}} \\ 
{\bf $\;\;$then }{\rm{p-add-nat-okp}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-add-nat-okp} \\ 
{\bf case = }{\it{sub-nat\/}} \\ 
{\bf $\;\;$then }{\rm{p-sub-nat-okp}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-sub-nat-okp} \\ 
{\bf case = }{\it{sub1-nat\/}} \\ 
{\bf $\;\;$then }{\rm{p-sub1-nat-okp}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-sub1-nat-okp} \\ 
{\bf case = }{\it{or-bool\/}} \\ 
{\bf $\;\;$then }{\rm{p-or-bool-okp}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-or-bool-okp} \\ 
{\bf case = }{\it{and-bool\/}} \\ 
{\bf $\;\;$then }{\rm{p-and-bool-okp}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-and-bool-okp} \\ 
{\bf case = }{\it{not-bool\/}} \\ 
{\bf $\;\;$then }{\rm{p-not-bool-okp}}\,({\rm{cons}}\,({\rm{pack}}\,({\it{opr\/}}), {\it{args\/}}), {\it{p\/}})\index{p-not-bool-okp} \\ 
{\bf otherwise }{\bf{f}}$\;${\bf  endcase}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  p-0-unwinding-lemma \\ \index{p-0-unwinding-lemma}
{\rm{p}}\,({\it{s\/}}, {\tt{0}})\index{p} $=$ {\it{s\/}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  p-plus-lemma \\ \index{p-plus-lemma}
{\rm{p}}\,({\it{state\/}}, {\it{j\/}} $+$ {\it{k\/}})\index{p} $=$ {\rm{p}}\,({\rm{p}}\,({\it{state\/}}, {\it{j\/}})\index{p}, {\it{k\/}})\index{p}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  p-add1 \\ \index{p-add1}
{\rm{p}}\,({\it{state\/}}, $1\;+$ {\it{x\/}})\index{p} $=$ {\rm{p}}\,({\rm{p}}\,({\it{state\/}}, {\it{x\/}})\index{p}, {\tt{1}})\index{p}
\end{tabbing}


\noindent{\sc Event}:   Disable p-add1.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  p-rearrange-times-lemma \\ \index{p-rearrange-times-lemma}
{\rm{p}}\,({\rm{p}}\,({\it{state\/}}, {\it{k\/}})\index{p}, {\it{j\/}})\index{p} $=$ {\rm{p}}\,({\rm{p}}\,({\it{state\/}}, {\it{j\/}})\index{p}, {\it{k\/}})\index{p}
\end{tabbing}


\noindent{\sc Event}:   Disable p-rearrange-times-lemma.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  p-add1-3 \\ \index{p-add1-3}
{\rm{p}}\,({\it{state\/}}, $1\;+$ {\it{x\/}})\index{p} $=$ {\rm{p}}\,({\rm{p-step}}\,({\it{state\/}})\index{p-step}, {\it{x\/}})\index{p}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  find-label-append \\ \index{find-label-append}
\=\+($\neg$ {\rm{find-labelp}}\,({\it{label\/}}, {\it{code1\/}})\index{find-labelp}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{find-label}}\,({\it{label\/}}, {\rm{append}}\,({\it{code1\/}}, {\it{code2\/}}))\index{find-label} \\ 
$=$$\;\;\;\;$({\rm{length}}\,({\it{code1\/}})\index{length} $+$ {\rm{find-label}}\,({\it{label\/}}, {\it{code2\/}})\index{find-label}))\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable find-label-append.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  find-labelp-append2 \\ \index{find-labelp-append2}
\=\+{\rm{find-labelp}}\,({\it{n\/}}, {\rm{append}}\,({\it{lst1\/}}, {\it{lst2\/}}))\index{find-labelp} \\ 
$=$$\;\;\;\;$({\rm{find-labelp}}\,({\it{n\/}}, {\it{lst1\/}})\index{find-labelp} $\vee$ {\rm{find-labelp}}\,({\it{n\/}}, {\it{lst2\/}})\index{find-labelp})\-
\end{tabbing}


\noindent{\sc Event}:   Disable find-labelp-append2.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  rget-inverts-rput \\ \index{rget-inverts-rput}
{\rm{rget}}\,({\it{n\/}}, {\rm{rput}}\,({\it{value\/}}, {\it{n\/}}, {\it{lst\/}})\index{rput})\index{rget} $=$ {\it{value\/}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  rput-same-value-doesnt-disturb-temp-stk \\ \index{rput-same-value-doesnt-disturb-te!mp-stk}
\=\+({\it{n\/}} $=$ {\rm{length}}\,({\it{temp-stk\/}})\index{length}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{rput}}\,({\it{value\/}}, {\it{n\/}}, {\rm{append}}\,({\it{lst\/}}, {\rm{cons}}\,({\it{value\/}}, {\it{temp-stk\/}})))\index{rput} \\ 
$=$$\;\;\;\;${\rm{append}}\,({\it{lst\/}}, {\rm{cons}}\,({\it{value\/}}, {\it{temp-stk\/}})))\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable ilessp.

\addvspace{18pt}

\noindent{\sc Event}:   Disable not-bool.

\addvspace{18pt}

\noindent{\sc Event}:   Disable and-bool.

\addvspace{18pt}

\noindent{\sc Event}:   Disable or-bool.

\addvspace{18pt}

\noindent{\sc Event}:   Disable inegate.

\addvspace{18pt}

\noindent{\sc Event}:   Disable fix-small-integer.

\addvspace{18pt}

\noindent{\sc Event}:   Disable iplus.

\addvspace{18pt}

\noindent{\sc Event}:   Disable idifference.

\addvspace{18pt}



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

\addvspace{18pt}

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