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

\addvspace{18pt}


\begin{tabbing}{\sc Definition}:\index{value}$\;\;$
{\rm{value}}\,({\it{alist\/}}, {\it{key\/}})\index{value} $=$ {\rm{cdr}}\,({\rm{assoc}}\,({\it{key\/}}, {\it{alist\/}}))
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{ct}$\;\;$
{\rm{ct}}\,({\it{i\/}})\index{ct} $=$ {\rm{cons}}\,({\tt{'}}{\tt{ct}}, {\it{i\/}})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{cf}$\;\;$
{\rm{cf}}\,({\it{i\/}})\index{cf} $=$ {\rm{cons}}\,({\tt{'}}{\tt{cf}}, {\it{i\/}})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{temp}$\;\;$
{\rm{temp}}\,({\it{i\/}})\index{temp} $=$ {\rm{cons}}\,({\tt{'}}{\tt{temp}}, {\it{i\/}})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{c-element} \\  
\=\+{\rm{c-element}}\,({\it{old\/}}, {\it{new\/}}, {\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{c-element} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{value}}\,({\it{old\/}}, {\it{a\/}})\index{value} $\leftrightarrow$ {\rm{value}}\,({\it{old\/}}, {\it{b\/}})\index{value} \\ 
{\bf then }({\rm{value}}\,({\it{new\/}}, {\it{c\/}})\index{value} $\leftrightarrow$ {\rm{value}}\,({\it{old\/}}, {\it{a\/}})\index{value}) $\wedge$ {\rm{changed}}\,({\it{old\/}}, {\it{new\/}}, {\rm{list}}\,({\it{c\/}}))\index{changed} \\ 
{\bf else }{\rm{changed}}\,({\it{old\/}}, {\it{new\/}}, {\bf{nil}})\index{changed}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{nor-gate} \\  
\=\+{\rm{nor-gate}}\,({\it{old\/}}, {\it{new\/}}, {\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{nor-gate} \\ 
$=$$\;\;\;\;$(\=\+({\rm{value}}\,({\it{new\/}}, {\it{c\/}})\index{value} $\leftrightarrow$ ($\neg$ ({\rm{value}}\,({\it{old\/}}, {\it{a\/}})\index{value} $\vee$ {\rm{value}}\,({\it{old\/}}, {\it{b\/}})\index{value}))) \\ 
$\wedge$$\;\;\;\;${\rm{changed}}\,({\it{old\/}}, {\it{new\/}}, {\rm{list}}\,({\it{c\/}}))\index{changed})\-\-
\end{tabbing}


\begin{tabbing}{\sc Definition}:\index{fifo-node} \\  
\=\+{\rm{fifo-node}}\,({\it{i\/}})\index{fifo-node} \\ 
$=$$\;\;\;\;${\rm{list}}\,(\=\+{\rm{list}}\,({\tt{'}}{\tt{c-element}}, {\rm{ct}}\,($1\;+$ {\it{i\/}})\index{ct}, {\rm{temp}}\,({\it{i\/}})\index{temp}, {\rm{ct}}\,({\it{i\/}})\index{ct}), \\ 
{\rm{list}}\,({\tt{'}}{\tt{c-element}}, {\rm{cf}}\,($1\;+$ {\it{i\/}})\index{cf}, {\rm{temp}}\,({\it{i\/}})\index{temp}, {\rm{cf}}\,({\it{i\/}})\index{cf}), \\ 
{\rm{list}}\,({\tt{'}}{\tt{nor-gate}}, {\rm{ct}}\,({\it{i\/}} $-\;1$)\index{ct}, {\rm{cf}}\,({\it{i\/}} $-\;1$)\index{cf}, {\rm{temp}}\,({\it{i\/}})\index{temp}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{empty-node} \\  
\=\+{\rm{empty-node}}\,({\it{state\/}}, {\it{i\/}})\index{empty-node} \\ 
$=$$\;\;\;\;$(($\neg$ {\rm{value}}\,({\it{state\/}}, {\rm{ct}}\,({\it{i\/}})\index{ct})\index{value}) $\wedge$ ($\neg$ {\rm{value}}\,({\it{state\/}}, {\rm{cf}}\,({\it{i\/}})\index{cf})\index{value}))\-
\end{tabbing}


\begin{tabbing}{\sc Definition}:\index{true-node} \\  
{\rm{true-node}}\,({\it{state\/}}, {\it{i\/}})\index{true-node} $=$ ({\rm{value}}\,({\it{state\/}}, {\rm{ct}}\,({\it{i\/}})\index{ct})\index{value} $\wedge$ ($\neg$ {\rm{value}}\,({\it{state\/}}, {\rm{cf}}\,({\it{i\/}})\index{cf})\index{value}))
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{false-node} \\  
{\rm{false-node}}\,({\it{state\/}}, {\it{i\/}})\index{false-node} $=$ (($\neg$ {\rm{value}}\,({\it{state\/}}, {\rm{ct}}\,({\it{i\/}})\index{ct})\index{value}) $\wedge$ {\rm{value}}\,({\it{state\/}}, {\rm{cf}}\,({\it{i\/}})\index{cf})\index{value})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{in-node} \\  
\=\+{\rm{in-node}}\,({\it{old\/}}, {\it{new\/}}, {\it{i\/}})\index{in-node} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{value}}\,({\it{old\/}}, {\rm{temp}}\,({\it{i\/}})\index{temp})\index{value} $\leftrightarrow$ {\rm{empty-node}}\,({\it{old\/}}, {\it{i\/}})\index{empty-node} \\ 
{\bf then }\=\+{\bf if }{\rm{empty-node}}\,({\it{old\/}}, {\it{i\/}})\index{empty-node} \\ 
{\bf then }\=\+{\rm{changed}}\,({\it{old\/}}, {\it{new\/}}, {\bf{nil}})\index{changed} \\ 
$\vee$$\;\;\;\;$(\=\+({\rm{true-node}}\,({\it{new\/}}, {\it{i\/}})\index{true-node} $\vee$ {\rm{false-node}}\,({\it{new\/}}, {\it{i\/}})\index{false-node}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{value}}\,({\it{new\/}}, {\tt{'}}{\tt{input}})\index{value} \\ 
$=$$\;\;\;\;${\rm{cons}}\,(\=\+{\rm{true-node}}\,({\it{new\/}}, {\it{i\/}})\index{true-node}, \\ 
{\rm{value}}\,({\it{old\/}}, {\tt{'}}{\tt{input}})\index{value})\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{changed}}\,({\it{old\/}}, {\it{new\/}}, {\rm{list}}\,({\rm{ct}}\,({\it{i\/}})\index{ct}, {\rm{cf}}\,({\it{i\/}})\index{cf}, {\tt{'}}{\tt{input}}))\index{changed})\-\- \\ 
{\bf else }\=\+{\rm{changed}}\,({\it{old\/}}, {\it{new\/}}, {\bf{nil}})\index{changed} \\ 
$\vee$$\;\;\;\;$(\=\+{\rm{empty-node}}\,({\it{new\/}}, {\it{i\/}})\index{empty-node} \\ 
$\wedge$$\;\;\;\;${\rm{changed}}\,({\it{old\/}}, {\it{new\/}}, {\rm{list}}\,({\rm{ct}}\,({\it{i\/}})\index{ct}, {\rm{cf}}\,({\it{i\/}})\index{cf}))\index{changed})\-\-$\;${\bf  endif}\- \\ 
{\bf else }{\rm{changed}}\,({\it{old\/}}, {\it{new\/}}, {\bf{nil}})\index{changed}$\;${\bf  endif}\-\-
\end{tabbing}


\begin{tabbing}{\sc Definition}:\index{out-node} \\  
\=\+{\rm{out-node}}\,({\it{old\/}}, {\it{new\/}})\index{out-node} \\ 
$=$$\;\;\;\;$(\=\+({\rm{value}}\,({\it{new\/}}, {\rm{ct}}\,({\tt{0}})\index{ct})\index{value} $\leftrightarrow$ {\rm{value}}\,({\it{old\/}}, {\rm{ct}}\,({\tt{1}})\index{ct})\index{value}) \\ 
$\wedge$$\;\;\;\;$({\rm{value}}\,({\it{new\/}}, {\rm{cf}}\,({\tt{0}})\index{cf})\index{value} $\leftrightarrow$ {\rm{value}}\,({\it{old\/}}, {\rm{cf}}\,({\tt{1}})\index{cf})\index{value}) \\ 
$\wedge$$\;\;\;\;$\=\+{\bf if }{\rm{empty-node}}\,({\it{old\/}}, {\tt{0}})\index{empty-node} $\wedge$ ($\neg$ {\rm{empty-node}}\,({\it{new\/}}, {\tt{0}})\index{empty-node}) \\ 
{\bf then }\=\+{\rm{value}}\,({\it{new\/}}, {\tt{'}}{\tt{output}})\index{value} \\ 
$=$$\;\;\;\;${\rm{cons}}\,({\rm{true-node}}\,({\it{new\/}}, {\tt{0}})\index{true-node}, {\rm{value}}\,({\it{old\/}}, {\tt{'}}{\tt{output}})\index{value})\- \\ 
{\bf else }{\rm{value}}\,({\it{new\/}}, {\tt{'}}{\tt{output}})\index{value} $=$ {\rm{value}}\,({\it{old\/}}, {\tt{'}}{\tt{output}})\index{value}$\;${\bf  endif}\- \\ 
$\wedge$$\;\;\;\;${\rm{changed}}\,({\it{old\/}}, {\it{new\/}}, {\rm{list}}\,({\rm{ct}}\,({\tt{0}})\index{ct}, {\rm{cf}}\,({\tt{0}})\index{cf}, {\tt{'}}{\tt{output}}))\index{changed})\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{internal-nodes} \\  
\=\+{\rm{internal-nodes}}\,({\it{n\/}})\index{internal-nodes} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{append}}\,({\rm{fifo-node}}\,({\it{n\/}})\index{fifo-node}, {\rm{internal-nodes}}\,({\it{n\/}} $-\;1$)\index{internal-nodes})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{external-nodes} \\  
\=\+{\rm{external-nodes}}\,({\it{n\/}})\index{external-nodes} \\ 
$=$$\;\;\;\;${\rm{list}}\,(\=\+{\rm{list}}\,({\tt{'}}{\tt{in-node}}, {\it{n\/}}), \\ 
{\rm{list}}\,({\tt{'}}{\tt{out-node}}), \\ 
{\rm{list}}\,({\tt{'}}{\tt{nor-gate}}, {\rm{ct}}\,({\it{n\/}} $-\;1$)\index{ct}, {\rm{cf}}\,({\it{n\/}} $-\;1$)\index{cf}, {\rm{temp}}\,({\it{n\/}})\index{temp}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{fifo-queue} \\  
{\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue} $=$ {\rm{append}}\,({\rm{external-nodes}}\,({\it{n\/}})\index{external-nodes}, {\rm{internal-nodes}}\,({\it{n\/}} $-\;1$)\index{internal-nodes})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member-internal-nodes \\ \index{member-internal-nodes}
\=\+({\it{statement\/}} $\in$ {\rm{internal-nodes}}\,({\it{n\/}})\index{internal-nodes}) \\ 
$=$$\;\;\;\;$(\=\+({\it{statement\/}} $\in$ {\rm{fifo-node}}\,({\rm{cdadddr}}\,({\it{statement\/}}))\index{fifo-node}) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not<$ {\rm{cdadddr}}\,({\it{statement\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{cdadddr}}\,({\it{statement\/}}) $\not\simeq {\tt{0}}$))\-\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  member-fifo-queue \\ \index{member-fifo-queue}
\=\+({\tt{1}} $<$ {\it{n\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\it{statement\/}} $\in$ {\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue}) \\ 
$=$$\;\;\;\;$(\=\+({\it{statement\/}} $\in$ {\rm{internal-nodes}}\,({\it{n\/}} $-\;1$)\index{internal-nodes}) \\ 
$\vee$$\;\;\;\;$({\it{statement\/}} $\in$ {\rm{external-nodes}}\,({\it{n\/}})\index{external-nodes}))\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  listp-fifo-queue \\ \index{listp-fifo-queue}
{\rm{listp}}\,({\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})
\end{tabbing}


\noindent{\sc Event}:   Disable fifo-queue.

\addvspace{18pt}

\noindent{\sc Event}:   Disable *1*fifo-queue.

\addvspace{18pt}


\begin{tabbing}{\sc Definition}:\index{proper-node} \\  
\=\+{\rm{proper-node}}\,({\it{state\/}}, {\it{i\/}})\index{proper-node} \\ 
$=$$\;\;\;\;$(\=\+(\=\+(($\neg$ {\rm{empty-node}}\,({\it{state\/}}, {\it{i\/}})\index{empty-node}) $\wedge$ {\rm{empty-node}}\,({\it{state\/}}, {\it{i\/}} $-\;1$)\index{empty-node}) \\ 
$\rightarrow$$\;\;\;\;${\rm{value}}\,({\it{state\/}}, {\rm{temp}}\,({\it{i\/}})\index{temp})\index{value})\- \\ 
$\wedge$$\;\;\;\;$(\=\+({\rm{empty-node}}\,({\it{state\/}}, {\it{i\/}})\index{empty-node} $\wedge$ ($\neg$ {\rm{empty-node}}\,({\it{state\/}}, {\it{i\/}} $-\;1$)\index{empty-node})) \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{value}}\,({\it{state\/}}, {\rm{temp}}\,({\it{i\/}})\index{temp})\index{value}))\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{true-node}}\,({\it{state\/}}, {\it{i\/}})\index{true-node} \\ 
$\vee$$\;\;\;\;${\rm{false-node}}\,({\it{state\/}}, {\it{i\/}})\index{false-node} \\ 
$\vee$$\;\;\;\;${\rm{empty-node}}\,({\it{state\/}}, {\it{i\/}})\index{empty-node})\- \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{empty-node}}\,({\it{state\/}}, {\it{i\/}})\index{empty-node}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{empty-node}}\,({\it{state\/}}, {\it{i\/}} $-\;1$)\index{empty-node} \\ 
$\vee$$\;\;\;\;$\=\+{\bf if }{\rm{true-node}}\,({\it{state\/}}, {\it{i\/}})\index{true-node} \\ 
{\bf then }{\rm{true-node}}\,({\it{state\/}}, {\it{i\/}} $-\;1$)\index{true-node} \\ 
{\bf else }{\rm{false-node}}\,({\it{state\/}}, {\it{i\/}} $-\;1$)\index{false-node}$\;${\bf  endif}\-)\-)\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{proper-nodes} \\  
\=\+{\rm{proper-nodes}}\,({\it{state\/}}, {\it{n\/}})\index{proper-nodes} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{proper-node}}\,({\it{state\/}}, {\it{n\/}})\index{proper-node} $\wedge$ {\rm{proper-nodes}}\,({\it{state\/}}, {\it{n\/}} $-\;1$)\index{proper-nodes}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  proper-nodes-implies \\ \index{proper-nodes-implies}
({\rm{proper-nodes}}\,({\it{state\/}}, {\it{n\/}})\index{proper-nodes} $\wedge$ ({\it{n\/}} $\not<$ {\it{i\/}}) $\wedge$ ({\it{i\/}} $\not\simeq {\tt{0}}$)) $\rightarrow$ {\rm{proper-node}}\,({\it{state\/}}, {\it{i\/}})\index{proper-node}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  proper-nodes-preserved-general \\ \index{proper-nodes-preserved-general}
\=\+(\=\+{\rm{n}}\,({\it{old\/}}, {\it{new\/}}, {\it{statement\/}})\index{n} \\ 
$\wedge$$\;\;\;\;${\rm{proper-nodes}}\,({\it{old\/}}, {\it{n\/}})\index{proper-nodes} \\ 
$\wedge$$\;\;\;\;$({\it{statement\/}} $\in$ {\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue}) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not<$ {\it{i\/}}) \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{n\/}}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{proper-nodes}}\,({\it{new\/}}, {\it{i\/}})\index{proper-nodes}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  proper-nodes-preserved \\ \index{proper-nodes-preserved}
\=\+(\=\+{\rm{n}}\,({\it{old\/}}, {\it{new\/}}, {\it{statement\/}})\index{n} \\ 
$\wedge$$\;\;\;\;$({\it{statement\/}} $\in$ {\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue}) \\ 
$\wedge$$\;\;\;\;${\rm{proper-nodes}}\,({\it{old\/}}, {\it{n\/}})\index{proper-nodes} \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{n\/}}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{proper-nodes}}\,({\it{new\/}}, {\it{n\/}})\index{proper-nodes}\-
\end{tabbing}


\noindent{\sc Event}:   Disable proper-nodes-preserved-general.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  proper-nodes-unless-false \\ \index{proper-nodes-unless-false}
\=\+({\tt{1}} $<$ {\it{n\/}}) \\ 
$\rightarrow$$\;\;\;\;${\rm{unless}}\,({\tt{`}}{\tt{(}}{\tt{proper-nodes}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}, {\tt{'}}{\tt{(}}{\tt{false}}{\tt{)}}, {\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\index{unless}\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  proper-nodes-invariant \\ \index{proper-nodes-invariant}
\=\+(\=\+({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{initial-condition}}\,({\tt{`}}{\tt{(}}{\tt{proper-nodes}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}, {\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\index{initial-condition})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{invariant}}\,({\tt{`}}{\tt{(}}{\tt{proper-nodes}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}, {\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\index{invariant}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  proper-node-invariant \\ \index{proper-node-invariant}
\=\+(\=\+({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not<$ {\it{i\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{initial-condition}}\,({\tt{`}}{\tt{(}}{\tt{proper-nodes}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}, {\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\index{initial-condition})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{invariant}}\,({\tt{`}}{\tt{(}}{\tt{proper-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{i}}{\tt{)}}, {\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\index{invariant}\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{queue-values} \\  
\=\+{\rm{queue-values}}\,({\it{state\/}}, {\it{n\/}})\index{queue-values} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf elseif }($\neg$ {\rm{empty-node}}\,({\it{state\/}}, {\it{n\/}})\index{empty-node}) $\wedge$ {\rm{empty-node}}\,({\it{state\/}}, {\it{n\/}} $-\;1$)\index{empty-node} \\ 
{\bf then }{\rm{cons}}\,({\rm{true-node}}\,({\it{state\/}}, {\it{n\/}})\index{true-node}, {\rm{queue-values}}\,({\it{state\/}}, {\it{n\/}} $-\;1$)\index{queue-values}) \\ 
{\bf else }{\rm{queue-values}}\,({\it{state\/}}, {\it{n\/}} $-\;1$)\index{queue-values}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  empty-empty-empty \\ \index{empty-empty-empty}
\=\+(\=\+({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{n}}\,({\it{old\/}}, {\it{new\/}}, {\it{statement\/}})\index{n} \\ 
$\wedge$$\;\;\;\;$({\it{statement\/}} $\in$ {\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue}) \\ 
$\wedge$$\;\;\;\;${\rm{empty-node}}\,({\it{old\/}}, $1\;+$ {\it{i\/}})\index{empty-node} \\ 
$\wedge$$\;\;\;\;${\rm{empty-node}}\,({\it{old\/}}, {\it{i\/}})\index{empty-node} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\it{n\/}}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{empty-node}}\,({\it{new\/}}, {\it{i\/}})\index{empty-node}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  full-full-full \\ \index{full-full-full}
\=\+(\=\+({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{n}}\,({\it{old\/}}, {\it{new\/}}, {\it{statement\/}})\index{n} \\ 
$\wedge$$\;\;\;\;$({\it{statement\/}} $\in$ {\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{empty-node}}\,({\it{old\/}}, $1\;+$ {\it{i\/}})\index{empty-node}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{empty-node}}\,({\it{old\/}}, {\it{i\/}})\index{empty-node}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\rm{true-node}}\,({\it{old\/}}, $1\;+$ {\it{i\/}})\index{true-node} $\leftrightarrow$ {\rm{true-node}}\,({\it{old\/}}, {\it{i\/}})\index{true-node}) \\ 
$\vee$$\;\;\;\;$({\rm{false-node}}\,({\it{old\/}}, $1\;+$ {\it{i\/}})\index{false-node} $\leftrightarrow$ {\rm{false-node}}\,({\it{old\/}}, {\it{i\/}})\index{false-node}))\- \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\it{n\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{empty-node}}\,({\it{new\/}}, {\it{i\/}})\index{empty-node})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  queue-empty-preserved \\ \index{queue-empty-preserved}
\=\+(\=\+({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{n}}\,({\it{old\/}}, {\it{new\/}}, {\it{statement\/}})\index{n} \\ 
$\wedge$$\;\;\;\;$({\it{statement\/}} $\in$ {\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue}) \\ 
$\wedge$$\;\;\;\;${\rm{proper-nodes}}\,({\it{old\/}}, {\it{n\/}})\index{proper-nodes} \\ 
$\wedge$$\;\;\;\;$({\rm{queue-values}}\,({\it{old\/}}, $1\;+$ {\it{i\/}})\index{queue-values} $=$ {\bf{nil}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\it{n\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{queue-values}}\,({\it{new\/}}, {\it{i\/}})\index{queue-values} $=$ {\bf{nil}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  value-moves-forward \\ \index{value-moves-forward}
\=\+(\=\+({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{n}}\,({\it{old\/}}, {\it{new\/}}, {\it{statement\/}})\index{n} \\ 
$\wedge$$\;\;\;\;$({\it{statement\/}} $\in$ {\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue}) \\ 
$\wedge$$\;\;\;\;${\rm{proper-nodes}}\,({\it{old\/}}, {\it{n\/}})\index{proper-nodes} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{empty-node}}\,({\it{old\/}}, $1\;+$ {\it{i\/}})\index{empty-node}) \\ 
$\wedge$$\;\;\;\;${\rm{empty-node}}\,({\it{old\/}}, {\it{i\/}})\index{empty-node} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not\simeq {\tt{0}}$))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+(($\neg$ {\rm{empty-node}}\,({\it{new\/}}, $1\;+$ {\it{i\/}})\index{empty-node}) $\wedge$ {\rm{empty-node}}\,({\it{new\/}}, {\it{i\/}})\index{empty-node}) \\ 
$\vee$$\;\;\;\;$(($\neg$ {\rm{empty-node}}\,({\it{new\/}}, {\it{i\/}})\index{empty-node}) $\wedge$ {\rm{empty-node}}\,({\it{new\/}}, {\it{i\/}} $-\;1$)\index{empty-node}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  not-listp-queue-values-equals \\ \index{not-listp-queue-values-equals}
{\rm{listp}}\,({\rm{queue-values}}\,({\it{state\/}}, {\it{n\/}})\index{queue-values}) $=$ ({\rm{queue-values}}\,({\it{state\/}}, {\it{n\/}})\index{queue-values} $\not=$ {\bf{nil}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  full-empty-rest-unless-moves-forward \\ \index{full-empty-rest-unless-moves-fo!rward}
\=\+(({\tt{1}} $<$ {\it{n\/}}) $\wedge$ ({\it{i\/}} $<$ {\it{n\/}}) $\wedge$ ({\it{i\/}} $\not\simeq {\tt{0}}$)) \\ 
$\rightarrow$$\;\;\;\;${\rm{unless}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{proper-nodes}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{not}}{\tt{ }}{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{i}}{\tt{)}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{i}}{\tt{)}} \\ 
{\tt{(}}{\tt{not}}{\tt{ }}{\tt{(}}{\tt{listp}}{\tt{ }}{\tt{(}}{\tt{queue-values}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{i}}{\tt{)}}{\tt{)}}{\tt{)}}{\tt{)}}\-{\tt{)}}\-{\tt{)}}\-, \\ 
{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{not}}{\tt{ }}{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{i}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{sub1}}{\tt{ }}{\tt{i}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{not}} \\ 
{\tt{(}}{\tt{listp}}{\tt{ }}{\tt{(}}{\tt{queue-values}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{sub1}}{\tt{ }}{\tt{i}}{\tt{)}}{\tt{)}}{\tt{)}}{\tt{)}}\-{\tt{)}}\-{\tt{)}}\-, \\ 
{\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\-\index{unless}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  output-only-adds-boolean \\ \index{output-only-adds-boolean}
\=\+({\tt{1}} $<$ {\it{n\/}}) \\ 
$\rightarrow$$\;\;\;\;${\rm{unless}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{equal}}{\tt{ }}{\tt{(}}{\tt{value}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{output}}{\tt{)}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{k}}{\tt{)}}, \\ 
{\tt{`}}{\tt{(}}\=\+{\tt{or}} \\ 
{\tt{(}}\=\+{\tt{equal}} \\ 
{\tt{(}}{\tt{value}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{output}}{\tt{)}} \\ 
{\tt{(}}{\tt{cons}}{\tt{ }}{\tt{(}}{\tt{true}}{\tt{)}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{k}}{\tt{)}}{\tt{)}}\- \\ 
{\tt{(}}\=\+{\tt{equal}} \\ 
{\tt{(}}{\tt{value}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{output}}{\tt{)}} \\ 
{\tt{(}}{\tt{cons}}{\tt{ }}{\tt{(}}{\tt{false}}{\tt{)}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{k}}{\tt{)}}{\tt{)}}\-{\tt{)}}\-, \\ 
{\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\-\index{unless}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  input-only-adds-boolean \\ \index{input-only-adds-boolean}
\=\+({\tt{1}} $<$ {\it{n\/}}) \\ 
$\rightarrow$$\;\;\;\;${\rm{unless}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{equal}}{\tt{ }}{\tt{(}}{\tt{value}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{input}}{\tt{)}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{k}}{\tt{)}}, \\ 
{\tt{`}}{\tt{(}}\=\+{\tt{or}} \\ 
{\tt{(}}\=\+{\tt{equal}} \\ 
{\tt{(}}{\tt{value}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{input}}{\tt{)}} \\ 
{\tt{(}}{\tt{cons}}{\tt{ }}{\tt{(}}{\tt{true}}{\tt{)}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{k}}{\tt{)}}{\tt{)}}\- \\ 
{\tt{(}}\=\+{\tt{equal}} \\ 
{\tt{(}}{\tt{value}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{input}}{\tt{)}} \\ 
{\tt{(}}{\tt{cons}}{\tt{ }}{\tt{(}}{\tt{false}}{\tt{)}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{k}}{\tt{)}}{\tt{)}}\-{\tt{)}}\-, \\ 
{\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\-\index{unless}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  output-never-shortens \\ \index{output-never-shortens}
\=\+({\tt{1}} $<$ {\it{n\/}}) \\ 
$\rightarrow$$\;\;\;\;${\rm{unless}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{equal}}{\tt{ }}{\tt{(}}{\tt{length}}{\tt{ }}{\tt{(}}{\tt{value}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{output}}{\tt{)}}{\tt{)}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{k}}{\tt{)}}, \\ 
{\tt{`}}{\tt{(}}{\tt{lessp}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{k}}{\tt{ }}{\tt{(}}{\tt{length}}{\tt{ }}{\tt{(}}{\tt{value}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{output}}{\tt{)}}{\tt{)}}{\tt{)}}, \\ 
{\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\-\index{unless}\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  total-sufficient-fifo-queue \\ \index{total-sufficient-fifo-queue}
\=\+({\tt{1}} $<$ {\it{n\/}}) \\ 
$\rightarrow$$\;\;\;\;${\rm{total-sufficient}}\,(\=\+{\it{statement\/}}, \\ 
{\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue}, \\ 
{\it{old\/}}, \\ 
\=\+{\bf if }{\rm{car}}\,({\it{statement\/}}) $=$ {\tt{'}}{\tt{c-element}} \\ 
{\bf then }\=\+{\bf if }\=\+{\rm{value}}\,({\it{old\/}}, {\rm{cadr}}\,({\it{statement\/}}))\index{value} \\ 
$\leftrightarrow$$\;\;\;\;${\rm{value}}\,({\it{old\/}}, {\rm{caddr}}\,({\it{statement\/}}))\index{value}\- \\ 
{\bf then }{\rm{update-assoc}}\,(\=\+{\rm{cadddr}}\,({\it{statement\/}}), \\ 
{\rm{value}}\,({\it{old\/}}, {\rm{cadr}}\,({\it{statement\/}}))\index{value}, \\ 
{\it{old\/}})\-\index{update-assoc} \\ 
{\bf else }{\it{old\/}}$\;${\bf  endif}\- \\ 
{\bf elseif }{\rm{car}}\,({\it{statement\/}}) $=$ {\tt{'}}{\tt{nor-gate}} \\ 
{\bf then }{\rm{update-assoc}}\,(\=\+{\rm{cadddr}}\,({\it{statement\/}}), \\ 
$\neg$ (\=\+{\rm{value}}\,({\it{old\/}}, {\rm{cadr}}\,({\it{statement\/}}))\index{value} \\ 
$\vee$$\;\;\;\;${\rm{value}}\,(\=\+{\it{old\/}}, \\ 
{\rm{caddr}}\,({\it{statement\/}}))\-\index{value})\-, \\ 
{\it{old\/}})\-\index{update-assoc} \\ 
{\bf elseif }{\rm{car}}\,({\it{statement\/}}) $=$ {\tt{'}}{\tt{in-node}} \\ 
{\bf then }\=\+{\bf if }\=\+(\=\+{\rm{value}}\,({\it{old\/}}, {\rm{temp}}\,({\rm{cadr}}\,({\it{statement\/}}))\index{temp})\index{value} \\ 
$=$$\;\;\;\;${\rm{empty-node}}\,({\it{old\/}}, {\rm{cadr}}\,({\it{statement\/}}))\index{empty-node})\- \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{empty-node}}\,({\it{old\/}}, {\rm{cadr}}\,({\it{statement\/}}))\index{empty-node})\- \\ 
{\bf then }{\rm{update-assoc}}\,(\=\+{\rm{ct}}\,({\rm{cadr}}\,({\it{statement\/}}))\index{ct}, \\ 
{\bf{f}}, \\ 
{\rm{update-assoc}}\,(\=\+{\rm{cf}}\,({\rm{cadr}}\,({\it{statement\/}}))\index{cf}, \\ 
{\bf{f}}, \\ 
{\it{old\/}})\-\index{update-assoc})\-\index{update-assoc} \\ 
{\bf else }{\it{old\/}}$\;${\bf  endif}\- \\ 
{\bf elseif }{\rm{car}}\,({\it{statement\/}}) $=$ {\tt{'}}{\tt{out-node}} \\ 
{\bf then }{\rm{update-assoc}}\,(\=\+{\rm{ct}}\,({\tt{0}})\index{ct}, \\ 
{\rm{value}}\,({\it{old\/}}, {\rm{ct}}\,({\tt{1}})\index{ct})\index{value}, \\ 
{\rm{update-assoc}}\,(\=\+{\rm{cf}}\,({\tt{0}})\index{cf}, \\ 
{\rm{value}}\,({\it{old\/}}, {\rm{cf}}\,({\tt{1}})\index{cf})\index{value}, \\ 
\=\+{\bf if }\=\+{\rm{empty-node}}\,({\it{old\/}}, {\tt{0}})\index{empty-node} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{empty-node}}\,(\=\+{\it{old\/}}, \\ 
{\tt{1}})\-\index{empty-node})\- \\ 
{\bf then }{\rm{update-assoc}}\,(\=\+{\tt{'}}{\tt{output}}, \\ 
{\rm{cons}}\,(\=\+{\rm{true-node}}\,(\=\+{\it{old\/}}, \\ 
{\tt{1}})\-\index{true-node}, \\ 
{\rm{value}}\,(\=\+{\it{old\/}}, \\ 
{\tt{'}}{\tt{output}})\-\index{value})\-, \\ 
{\it{old\/}})\-\index{update-assoc} \\ 
{\bf else }{\it{old\/}}$\;${\bf  endif}\-)\-\index{update-assoc})\-\index{update-assoc} \\ 
{\bf else }{\it{old\/}}$\;${\bf  endif}\-)\-\index{total-sufficient}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  total-fifo-queue \\ \index{total-fifo-queue}
({\tt{1}} $<$ {\it{n\/}}) $\rightarrow$ {\rm{total}}\,({\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\index{total}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  output-grows-immediately \\ \index{output-grows-immediately}
\=\+(\=\+{\rm{initial-condition}}\,({\tt{`}}{\tt{(}}{\tt{proper-nodes}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}, {\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\index{initial-condition} \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{n\/}}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{not}}{\tt{ }}{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{1}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{0}}{\tt{)}} \\ 
{\tt{(}}{\tt{equal}}{\tt{ }}{\tt{(}}{\tt{length}}{\tt{ }}{\tt{(}}{\tt{value}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{output}}{\tt{)}}{\tt{)}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{k}}{\tt{)}}{\tt{)}}\-{\tt{)}}\-, \\ 
{\tt{`}}{\tt{(}}{\tt{lessp}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{k}}{\tt{ }}{\tt{(}}{\tt{length}}{\tt{ }}{\tt{(}}{\tt{value}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{output}}{\tt{)}}{\tt{)}}{\tt{)}}, \\ 
{\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\-\index{leads-to}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  true-empty-temp-moves \\ \index{true-empty-temp-moves}
\=\+(\=\+{\rm{initial-condition}}\,({\tt{`}}{\tt{(}}{\tt{proper-nodes}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}, {\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\index{initial-condition} \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\it{n\/}}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{true-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{i}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}{\tt{value}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{(}}{\tt{temp}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{i}}{\tt{)}}{\tt{)}}{\tt{)}}\-, \\ 
{\tt{`}}{\tt{(}}{\tt{not}}{\tt{ }}{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{i}}{\tt{)}}{\tt{)}}, \\ 
{\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\-\index{leads-to}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  false-empty-temp-moves \\ \index{false-empty-temp-moves}
\=\+(\=\+{\rm{initial-condition}}\,({\tt{`}}{\tt{(}}{\tt{proper-nodes}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}, {\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\index{initial-condition} \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\it{n\/}}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{false-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{i}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}{\tt{value}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{(}}{\tt{temp}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{i}}{\tt{)}}{\tt{)}}{\tt{)}}\-, \\ 
{\tt{`}}{\tt{(}}{\tt{not}}{\tt{ }}{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{i}}{\tt{)}}{\tt{)}}, \\ 
{\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\-\index{leads-to}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  not-empty-empty-temp-moves \\ \index{not-empty-empty-temp-moves}
\=\+(\=\+{\rm{initial-condition}}\,({\tt{`}}{\tt{(}}{\tt{proper-nodes}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}, {\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\index{initial-condition} \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\it{n\/}}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{not}}{\tt{ }}{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{i}}{\tt{)}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}{\tt{value}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{(}}{\tt{temp}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{i}}{\tt{)}}{\tt{)}}{\tt{)}}\-, \\ 
{\tt{`}}{\tt{(}}{\tt{not}}{\tt{ }}{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{i}}{\tt{)}}{\tt{)}}, \\ 
{\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\-\index{leads-to}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  empty-empty-sets-temp \\ \index{empty-empty-sets-temp}
\=\+(\=\+{\rm{initial-condition}}\,({\tt{`}}{\tt{(}}{\tt{proper-nodes}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}, {\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\index{initial-condition} \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\it{n\/}}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{i}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{i}}{\tt{)}}{\tt{)}}\-, \\ 
{\tt{`}}{\tt{(}}{\tt{value}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{(}}{\tt{temp}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{i}}{\tt{)}}{\tt{)}}{\tt{)}}, \\ 
{\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\-\index{leads-to}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  full-full-unsets-temp \\ \index{full-full-unsets-temp}
\=\+(\=\+{\rm{initial-condition}}\,({\tt{`}}{\tt{(}}{\tt{proper-nodes}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}, {\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\index{initial-condition} \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\it{n\/}}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{not}}{\tt{ }}{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{i}}{\tt{)}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}{\tt{not}}{\tt{ }}{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{i}}{\tt{)}}{\tt{)}}{\tt{)}}\-, \\ 
{\tt{`}}{\tt{(}}{\tt{not}}{\tt{ }}{\tt{(}}{\tt{value}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{(}}{\tt{temp}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{i}}{\tt{)}}{\tt{)}}{\tt{)}}{\tt{)}}, \\ 
{\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\-\index{leads-to}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  empty-true-not-temp-moves \\ \index{empty-true-not-temp-moves}
\=\+(\=\+{\rm{initial-condition}}\,({\tt{`}}{\tt{(}}{\tt{proper-nodes}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}, {\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\index{initial-condition} \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\it{n\/}}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{i}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{true-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{i}}{\tt{)}} \\ 
{\tt{(}}{\tt{not}}{\tt{ }}{\tt{(}}{\tt{value}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{(}}{\tt{temp}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{i}}{\tt{)}}{\tt{)}}{\tt{)}}{\tt{)}}\-{\tt{)}}\-, \\ 
{\tt{`}}{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{i}}{\tt{)}}, \\ 
{\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\-\index{leads-to}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  empty-false-not-temp-moves \\ \index{empty-false-not-temp-moves}
\=\+(\=\+{\rm{initial-condition}}\,({\tt{`}}{\tt{(}}{\tt{proper-nodes}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}, {\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\index{initial-condition} \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\it{n\/}}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{i}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{false-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{i}}{\tt{)}} \\ 
{\tt{(}}{\tt{not}}{\tt{ }}{\tt{(}}{\tt{value}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{(}}{\tt{temp}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{i}}{\tt{)}}{\tt{)}}{\tt{)}}{\tt{)}}\-{\tt{)}}\-, \\ 
{\tt{`}}{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{i}}{\tt{)}}, \\ 
{\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\-\index{leads-to}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  empty-not-temp-moves \\ \index{empty-not-temp-moves}
\=\+(\=\+{\rm{initial-condition}}\,({\tt{`}}{\tt{(}}{\tt{proper-nodes}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}, {\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\index{initial-condition} \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\it{n\/}}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{i}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}{\tt{not}}{\tt{ }}{\tt{(}}{\tt{value}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{(}}{\tt{temp}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{i}}{\tt{)}}{\tt{)}}{\tt{)}}{\tt{)}}\-, \\ 
{\tt{`}}{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{i}}{\tt{)}}, \\ 
{\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\-\index{leads-to}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  empty-1-leads-to-empty-0 \\ \index{empty-1-leads-to-empty-0}
\=\+(\=\+{\rm{initial-condition}}\,({\tt{`}}{\tt{(}}{\tt{proper-nodes}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}, {\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\index{initial-condition} \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{n\/}}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{1}}{\tt{)}}, \\ 
{\tt{`}}{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{0}}{\tt{)}}, \\ 
{\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\-\index{leads-to}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  full-empty-empty-moves-forward \\ \index{full-empty-empty-moves-forward}
\=\+(\=\+{\rm{initial-condition}}\,({\tt{`}}{\tt{(}}{\tt{proper-nodes}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}, {\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\index{initial-condition} \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not<$ ($1\;+$ ($1\;+$ {\it{i\/}}))) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\in\;${\bf{N}}${}$))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{not}}{\tt{ }}{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{i}}{\tt{)}}{\tt{)}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{i}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{i}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{not}} \\ 
{\tt{(}}{\tt{listp}}{\tt{ }}{\tt{(}}{\tt{queue-values}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{i}}{\tt{)}}{\tt{)}}{\tt{)}}{\tt{)}}\-{\tt{)}}\-{\tt{)}}\-{\tt{)}}\-, \\ 
{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{not}}{\tt{ }}{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{i}}{\tt{)}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{i}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\-\index{leads-to}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  full-empty-full-moves-forward \\ \index{full-empty-full-moves-forward}
\=\+(\=\+{\rm{initial-condition}}\,({\tt{`}}{\tt{(}}{\tt{proper-nodes}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}, {\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\index{initial-condition} \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not<$ ($1\;+$ ($1\;+$ {\it{i\/}}))) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\in\;${\bf{N}}${}$))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{not}}{\tt{ }}{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{i}}{\tt{)}}{\tt{)}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{i}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{not}}{\tt{ }}{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{i}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{not}} \\ 
{\tt{(}}{\tt{listp}}{\tt{ }}{\tt{(}}{\tt{queue-values}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{i}}{\tt{)}}{\tt{)}}{\tt{)}}{\tt{)}}\-{\tt{)}}\-{\tt{)}}\-{\tt{)}}\-, \\ 
{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{not}}{\tt{ }}{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{i}}{\tt{)}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{i}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\-\index{leads-to}\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  full-empty-moves-forward \\ \index{full-empty-moves-forward}
\=\+(\=\+{\rm{initial-condition}}\,({\tt{`}}{\tt{(}}{\tt{proper-nodes}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}, {\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\index{initial-condition} \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not<$ ($1\;+$ ($1\;+$ {\it{i\/}}))) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\in\;${\bf{N}}${}$))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{not}}{\tt{ }}{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{i}}{\tt{)}}{\tt{)}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{i}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{not}} \\ 
{\tt{(}}{\tt{listp}}{\tt{ }}{\tt{(}}{\tt{queue-values}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{i}}{\tt{)}}{\tt{)}}{\tt{)}}{\tt{)}}\-{\tt{)}}\-{\tt{)}}\-, \\ 
{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{not}}{\tt{ }}{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{i}}{\tt{)}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{i}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\-\index{leads-to}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  full-rest-empty-moves-forward \\ \index{full-rest-empty-moves-forward}
\=\+(\=\+{\rm{initial-condition}}\,({\tt{`}}{\tt{(}}{\tt{proper-nodes}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}, {\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\index{initial-condition} \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not\simeq {\tt{0}}$))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{not}}{\tt{ }}{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{i}}{\tt{)}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{i}}{\tt{)}} \\ 
{\tt{(}}{\tt{not}}{\tt{ }}{\tt{(}}{\tt{listp}}{\tt{ }}{\tt{(}}{\tt{queue-values}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{i}}{\tt{)}}{\tt{)}}{\tt{)}}{\tt{)}}\-{\tt{)}}\-, \\ 
{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{not}}{\tt{ }}{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{i}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{sub1}}{\tt{ }}{\tt{i}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{not}} \\ 
{\tt{(}}{\tt{listp}}{\tt{ }}{\tt{(}}{\tt{queue-values}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{sub1}}{\tt{ }}{\tt{i}}{\tt{)}}{\tt{)}}{\tt{)}}{\tt{)}}\-{\tt{)}}\-{\tt{)}}\-, \\ 
{\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\-\index{leads-to}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  full-rest-empty-output-grows \\ \index{full-rest-empty-output-grows}
\=\+(\=\+{\rm{initial-condition}}\,({\tt{`}}{\tt{(}}{\tt{proper-nodes}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}, {\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\index{initial-condition} \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\in\;${\bf{N}}${}$))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{not}}{\tt{ }}{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{i}}{\tt{)}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{empty-node}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{i}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{not}}{\tt{ }}{\tt{(}}{\tt{listp}}{\tt{ }}{\tt{(}}{\tt{queue-values}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{i}}{\tt{)}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{equal}} \\ 
{\tt{(}}{\tt{length}}{\tt{ }}{\tt{(}}{\tt{value}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{output}}{\tt{)}}{\tt{)}} \\ 
{\tt{'}}{\tt{,}}{\tt{k}}{\tt{)}}\-{\tt{)}}\-{\tt{)}}\-{\tt{)}}\-, \\ 
{\tt{`}}{\tt{(}}{\tt{lessp}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{k}}{\tt{ }}{\tt{(}}{\tt{length}}{\tt{ }}{\tt{(}}{\tt{value}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{output}}{\tt{)}}{\tt{)}}{\tt{)}}, \\ 
{\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\-\index{leads-to}\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{first-empty-subqueue} \\  
\=\+{\rm{first-empty-subqueue}}\,({\it{state\/}}, {\it{n\/}})\index{first-empty-subqueue} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\rm{listp}}\,({\rm{queue-values}}\,({\it{state\/}}, {\it{n\/}})\index{queue-values}) \\ 
{\bf then }{\rm{first-empty-subqueue}}\,({\it{state\/}}, {\it{n\/}} $-\;1$)\index{first-empty-subqueue} \\ 
{\bf else }{\it{n\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  first-empty-subqueue-is-empty \\ \index{first-empty-subqueue-is-empty}
$\neg$ {\rm{listp}}\,({\rm{queue-values}}\,({\it{state\/}}, {\rm{first-empty-subqueue}}\,({\it{state\/}}, {\it{n\/}})\index{first-empty-subqueue})\index{queue-values})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  queue-not-empty-implies \\ \index{queue-not-empty-implies}
\=\+{\rm{listp}}\,({\rm{queue-values}}\,({\it{state\/}}, {\it{n\/}})\index{queue-values}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+($\neg$ {\rm{empty-node}}\,({\it{state\/}}, $1\;+$ {\rm{first-empty-subqueue}}\,({\it{state\/}}, {\it{n\/}})\index{first-empty-subqueue})\index{empty-node}) \\ 
$\wedge$$\;\;\;\;${\rm{empty-node}}\,({\it{state\/}}, {\rm{first-empty-subqueue}}\,({\it{state\/}}, {\it{n\/}})\index{first-empty-subqueue})\index{empty-node})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  not-lessp-first-empty-subqueue \\ \index{not-lessp-first-empty-subqueue}
{\it{n\/}} $\not<$ {\rm{first-empty-subqueue}}\,({\it{state\/}}, {\it{n\/}})\index{first-empty-subqueue}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-first-empty-subqueue \\ \index{lessp-first-empty-subqueue}
{\rm{listp}}\,({\rm{queue-values}}\,({\it{state\/}}, {\it{n\/}})\index{queue-values}) $\rightarrow$ ({\rm{first-empty-subqueue}}\,({\it{state\/}}, {\it{n\/}})\index{first-empty-subqueue} $<$ {\it{n\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  output-grows \\ \index{output-grows}
\=\+(\=\+{\rm{initial-condition}}\,({\tt{`}}{\tt{(}}{\tt{proper-nodes}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}, {\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\index{initial-condition} \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{n\/}}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{listp}}{\tt{ }}{\tt{(}}{\tt{queue-values}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{n}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}{\tt{equal}}{\tt{ }}{\tt{(}}{\tt{length}}{\tt{ }}{\tt{(}}{\tt{value}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{output}}{\tt{)}}{\tt{)}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{k}}{\tt{)}}{\tt{)}}\-, \\ 
{\tt{`}}{\tt{(}}{\tt{lessp}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{k}}{\tt{ }}{\tt{(}}{\tt{length}}{\tt{ }}{\tt{(}}{\tt{value}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{output}}{\tt{)}}{\tt{)}}{\tt{)}}, \\ 
{\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\-\index{leads-to}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  in-node-leaves-rest-of-queue-unchanged \\ \index{in-node-leaves-rest-of-queue-un!changed}
\=\+({\rm{n}}\,({\it{old\/}}, {\it{new\/}}, {\rm{list}}\,({\tt{'}}{\tt{in-node}}, {\it{n\/}}))\index{n} $\wedge$ ({\tt{1}} $<$ {\it{n\/}}) $\wedge$ ({\it{i\/}} $<$ {\it{n\/}}) $\wedge$ ({\it{i\/}} $\in\;${\bf{N}}${}$)) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{value}}\,({\it{new\/}}, {\tt{'}}{\tt{output}})\index{value} $=$ {\rm{value}}\,({\it{old\/}}, {\tt{'}}{\tt{output}})\index{value}) \\ 
$\wedge$$\;\;\;\;$({\rm{queue-values}}\,({\it{new\/}}, {\it{i\/}})\index{queue-values} $=$ {\rm{queue-values}}\,({\it{old\/}}, {\it{i\/}})\index{queue-values}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  in-node-preserves-values \\ \index{in-node-preserves-values}
\=\+(\=\+{\rm{n}}\,({\it{old\/}}, {\it{new\/}}, {\rm{list}}\,({\tt{'}}{\tt{in-node}}, {\it{n\/}}))\index{n} \\ 
$\wedge$$\;\;\;\;${\rm{proper-node}}\,({\it{old\/}}, {\it{n\/}})\index{proper-node} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{value}}\,({\it{old\/}}, {\tt{'}}{\tt{input}})\index{value} \\ 
$=$$\;\;\;\;${\rm{append}}\,({\rm{queue-values}}\,({\it{old\/}}, {\it{n\/}})\index{queue-values}, {\rm{value}}\,({\it{old\/}}, {\tt{'}}{\tt{output}})\index{value}))\- \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{n\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{value}}\,({\it{new\/}}, {\tt{'}}{\tt{input}})\index{value} \\ 
$=$$\;\;\;\;${\rm{append}}\,({\rm{queue-values}}\,({\it{new\/}}, {\it{n\/}})\index{queue-values}, {\rm{value}}\,({\it{new\/}}, {\tt{'}}{\tt{output}})\index{value}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  out-node-preserves-queue-values \\ \index{out-node-preserves-queue-values}
\=\+({\rm{n}}\,({\it{old\/}}, {\it{new\/}}, {\tt{'}}{\tt{(}}{\tt{out-node}}{\tt{)}})\index{n} $\wedge$ ({\tt{1}} $<$ {\it{n\/}}) $\wedge$ ({\it{n\/}} $\not<$ {\it{i\/}}) $\wedge$ ({\it{i\/}} $\not\simeq {\tt{0}}$)) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{value}}\,({\it{new\/}}, {\tt{'}}{\tt{input}})\index{value} $=$ {\rm{value}}\,({\it{old\/}}, {\tt{'}}{\tt{input}})\index{value}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{append}}\,({\rm{queue-values}}\,({\it{new\/}}, {\it{i\/}})\index{queue-values}, {\rm{value}}\,({\it{new\/}}, {\tt{'}}{\tt{output}})\index{value}) \\ 
$=$$\;\;\;\;${\rm{append}}\,({\rm{queue-values}}\,({\it{old\/}}, {\it{i\/}})\index{queue-values}, {\rm{value}}\,({\it{old\/}}, {\tt{'}}{\tt{output}})\index{value}))\-)\-\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  external-nor-gates-preserves-values \\ \index{external-nor-gates-preserves-va!lues}
\=\+(\=\+{\rm{n}}\,({\it{old\/}}, {\it{new\/}}, {\rm{list}}\,({\tt{'}}{\tt{nor-gate}}, {\rm{ct}}\,({\it{n\/}} $-\;1$)\index{ct}, {\rm{cf}}\,({\it{n\/}} $-\;1$)\index{cf}, {\rm{temp}}\,({\it{n\/}})\index{temp}))\index{n} \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not<$ {\it{i\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\in\;${\bf{N}}${}$))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{value}}\,({\it{new\/}}, {\tt{'}}{\tt{input}})\index{value} $=$ {\rm{value}}\,({\it{old\/}}, {\tt{'}}{\tt{input}})\index{value}) \\ 
$\wedge$$\;\;\;\;$({\rm{value}}\,({\it{new\/}}, {\tt{'}}{\tt{output}})\index{value} $=$ {\rm{value}}\,({\it{old\/}}, {\tt{'}}{\tt{output}})\index{value}) \\ 
$\wedge$$\;\;\;\;$({\rm{queue-values}}\,({\it{new\/}}, {\it{i\/}})\index{queue-values} $=$ {\rm{queue-values}}\,({\it{old\/}}, {\it{i\/}})\index{queue-values}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  internal-nodes-preserves-rest-of-queue \\ \index{internal-nodes-preserves-rest-o!f-queue}
\=\+(\=\+{\rm{n}}\,({\it{old\/}}, {\it{new\/}}, {\it{statement\/}})\index{n} \\ 
$\wedge$$\;\;\;\;$({\it{statement\/}} $\in$ {\rm{fifo-node}}\,({\it{i\/}})\index{fifo-node}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $<$ {\it{i\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{queue-values}}\,({\it{new\/}}, {\it{j\/}})\index{queue-values} $=$ {\rm{queue-values}}\,({\it{old\/}}, {\it{j\/}})\index{queue-values})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  internal-nodes-preserve-values \\ \index{internal-nodes-preserve-values}
\=\+(\=\+{\rm{n}}\,({\it{old\/}}, {\it{new\/}}, {\it{statement\/}})\index{n} \\ 
$\wedge$$\;\;\;\;$({\it{statement\/}} $\in$ {\rm{fifo-node}}\,({\it{i\/}})\index{fifo-node}) \\ 
$\wedge$$\;\;\;\;${\rm{proper-node}}\,({\it{old\/}}, $1\;+$ {\it{i\/}})\index{proper-node} \\ 
$\wedge$$\;\;\;\;${\rm{proper-node}}\,({\it{old\/}}, {\it{i\/}})\index{proper-node} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\it{j\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{value}}\,({\it{new\/}}, {\tt{'}}{\tt{input}})\index{value} $=$ {\rm{value}}\,({\it{old\/}}, {\tt{'}}{\tt{input}})\index{value}) \\ 
$\wedge$$\;\;\;\;$({\rm{value}}\,({\it{new\/}}, {\tt{'}}{\tt{output}})\index{value} $=$ {\rm{value}}\,({\it{old\/}}, {\tt{'}}{\tt{output}})\index{value}) \\ 
$\wedge$$\;\;\;\;$({\rm{queue-values}}\,({\it{new\/}}, {\it{j\/}})\index{queue-values} $=$ {\rm{queue-values}}\,({\it{old\/}}, {\it{j\/}})\index{queue-values}))\-\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  values-preserved \\ \index{values-preserved}
\=\+(\=\+{\rm{n}}\,({\it{old\/}}, {\it{new\/}}, {\it{statement\/}})\index{n} \\ 
$\wedge$$\;\;\;\;${\rm{proper-nodes}}\,({\it{old\/}}, {\it{n\/}})\index{proper-nodes} \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{value}}\,({\it{old\/}}, {\tt{'}}{\tt{input}})\index{value} \\ 
$=$$\;\;\;\;${\rm{append}}\,({\rm{queue-values}}\,({\it{old\/}}, {\it{n\/}})\index{queue-values}, {\rm{value}}\,({\it{old\/}}, {\tt{'}}{\tt{output}})\index{value}))\- \\ 
$\wedge$$\;\;\;\;$({\it{statement\/}} $\in$ {\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{value}}\,({\it{new\/}}, {\tt{'}}{\tt{input}})\index{value} \\ 
$=$$\;\;\;\;${\rm{append}}\,({\rm{queue-values}}\,({\it{new\/}}, {\it{n\/}})\index{queue-values}, {\rm{value}}\,({\it{new\/}}, {\tt{'}}{\tt{output}})\index{value}))\-\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  values-invariant \\ \index{values-invariant}
\=\+({\tt{1}} $<$ {\it{n\/}}) \\ 
$\rightarrow$$\;\;\;\;${\rm{unless}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{proper-nodes}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{equal}} \\ 
{\tt{(}}{\tt{value}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{input}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{append}} \\ 
{\tt{(}}{\tt{queue-values}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}} \\ 
{\tt{(}}{\tt{value}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{output}}{\tt{)}}{\tt{)}}\-{\tt{)}}\-{\tt{)}}\-, \\ 
{\tt{'}}{\tt{(}}{\tt{false}}{\tt{)}}, \\ 
{\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\-\index{unless}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  queue-values-invariant \\ \index{queue-values-invariant}
\=\+(\=\+{\rm{initial-condition}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{proper-nodes}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{equal}} \\ 
{\tt{(}}{\tt{value}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{input}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{append}} \\ 
{\tt{(}}{\tt{queue-values}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}} \\ 
{\tt{(}}{\tt{value}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{output}}{\tt{)}}{\tt{)}}\-{\tt{)}}\-{\tt{)}}\-, \\ 
{\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\-\index{initial-condition} \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{n\/}}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{invariant}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{equal}} \\ 
{\tt{(}}{\tt{value}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{input}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{append}} \\ 
{\tt{(}}{\tt{queue-values}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}} \\ 
{\tt{(}}{\tt{value}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{output}}{\tt{)}}{\tt{)}}\-{\tt{)}}\-, \\ 
{\rm{fifo-queue}}\,({\it{n\/}})\index{fifo-queue})\-\index{invariant}\-
\end{tabbing}


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