\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{verbatim};;;this files defines a token passing solution to the n processor
;;;mutual exclusion problem.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{status} \\  
{\rm{status}}\,({\it{state\/}}, {\it{index\/}})\index{status} $=$ {\rm{cdr}}\,({\rm{assoc}}\,({\rm{cons}}\,({\tt{'}}{\tt{me}}, {\it{index\/}}), {\it{state\/}}))
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{wait} \\  
{\rm{wait}}\,({\it{state\/}}, {\it{index\/}})\index{wait} $=$ ({\rm{status}}\,({\it{state\/}}, {\it{index\/}})\index{status} $=$ {\tt{'}}{\tt{wait}})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{non-critical} \\  
{\rm{non-critical}}\,({\it{state\/}}, {\it{index\/}})\index{non-critical} $=$ ({\rm{status}}\,({\it{state\/}}, {\it{index\/}})\index{status} $=$ {\tt{'}}{\tt{non-critical}})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{critical} \\  
\=\+{\rm{critical}}\,({\it{state\/}}, {\it{index\/}})\index{critical} \\ 
$=$$\;\;\;\;$(($\neg$ {\rm{non-critical}}\,({\it{state\/}}, {\it{index\/}})\index{non-critical}) $\wedge$ ($\neg$ {\rm{wait}}\,({\it{state\/}}, {\it{index\/}})\index{wait}))\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{ticks}$\;\;$
{\rm{ticks}}\,({\it{state\/}}, {\it{index\/}})\index{ticks} $=$ {\rm{fix}}\,({\rm{status}}\,({\it{state\/}}, {\it{index\/}})\index{status})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{critical-ticks} \\  
\=\+{\rm{critical-ticks}}\,({\it{state\/}}, {\it{index\/}}, {\it{ticks\/}})\index{critical-ticks} \\ 
$=$$\;\;\;\;$({\rm{critical}}\,({\it{state\/}}, {\it{index\/}})\index{critical} $\wedge$ ({\rm{ticks}}\,({\it{state\/}}, {\it{index\/}})\index{ticks} $=$ {\rm{fix}}\,({\it{ticks\/}})))\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{channel} \\  
{\rm{channel}}\,({\it{state\/}}, {\it{index\/}})\index{channel} $=$ {\rm{cdr}}\,({\rm{assoc}}\,({\rm{cons}}\,({\tt{'}}{\tt{c}}, {\it{index\/}}), {\it{state\/}}))
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{token}$\;\;$
{\rm{token}}\,({\it{state\/}}, {\it{index\/}})\index{token} $=$ {\rm{listp}}\,({\rm{channel}}\,({\it{state\/}}, {\it{index\/}})\index{channel})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{me} \\  
\=\+{\rm{me}}\,({\it{old\/}}, {\it{new\/}}, {\it{index\/}}, {\it{size\/}})\index{me} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{non-critical}}\,({\it{old\/}}, {\it{index\/}})\index{non-critical} \\ 
{\bf then }\=\+{\bf if }{\rm{non-critical}}\,({\it{new\/}}, {\it{index\/}})\index{non-critical} \\ 
{\bf then }\=\+{\bf if }{\rm{token}}\,({\it{old\/}}, {\it{index\/}})\index{token} \\ 
{\bf then }\=\+{\bf if }{\rm{add1-mod}}\,({\it{size\/}}, {\it{index\/}})\index{add1-mod} $=$ {\it{index\/}} \\ 
{\bf then }\=\+(\=\+{\rm{length}}\,({\rm{channel}}\,({\it{new\/}}, {\it{index\/}})\index{channel})\index{length} \\ 
$=$$\;\;\;\;${\rm{length}}\,({\rm{channel}}\,({\it{old\/}}, {\it{index\/}})\index{channel})\index{length})\- \\ 
$\wedge$$\;\;\;\;${\rm{changed}}\,({\it{old\/}}, {\it{new\/}}, {\rm{list}}\,({\rm{cons}}\,({\tt{'}}{\tt{c}}, {\it{index\/}})))\index{changed}\- \\ 
{\bf else }\=\+(\=\+{\rm{channel}}\,({\it{new\/}}, {\it{index\/}})\index{channel} \\ 
$=$$\;\;\;\;${\rm{cdr}}\,({\rm{channel}}\,({\it{old\/}}, {\it{index\/}})\index{channel}))\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{length}}\,({\rm{channel}}\,(\=\+{\it{new\/}}, \\ 
{\rm{add1-mod}}\,({\it{size\/}}, {\it{index\/}})\index{add1-mod})\-\index{channel})\index{length} \\ 
$=$$\;\;\;\;$($1\;+$ {\rm{length}}\,({\rm{channel}}\,(\=\+{\it{old\/}}, \\ 
{\rm{add1-mod}}\,(\=\+{\it{size\/}}, \\ 
{\it{index\/}})\-\index{add1-mod})\-\index{channel})\index{length}))\- \\ 
$\wedge$$\;\;\;\;${\rm{changed}}\,(\=\+{\it{old\/}}, \\ 
{\it{new\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{cons}}\,({\tt{'}}{\tt{c}}, {\it{index\/}}), \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{c}}, \\ 
{\rm{add1-mod}}\,(\=\+{\it{size\/}}, \\ 
{\it{index\/}})\-\index{add1-mod})\-)\-)\-\index{changed}\-$\;${\bf  endif}\- \\ 
{\bf else }{\rm{changed}}\,({\it{old\/}}, {\it{new\/}}, {\bf{nil}})\index{changed}$\;${\bf  endif}\- \\ 
{\bf else }\=\+{\rm{wait}}\,({\it{new\/}}, {\it{index\/}})\index{wait} \\ 
$\wedge$$\;\;\;\;${\rm{changed}}\,({\it{old\/}}, {\it{new\/}}, {\rm{list}}\,({\rm{cons}}\,({\tt{'}}{\tt{me}}, {\it{index\/}})))\index{changed}\-$\;${\bf  endif}\- \\ 
{\bf elseif }{\rm{wait}}\,({\it{old\/}}, {\it{index\/}})\index{wait} \\ 
{\bf then }\=\+{\bf if }{\rm{token}}\,({\it{old\/}}, {\it{index\/}})\index{token} \\ 
{\bf then }\=\+({\rm{channel}}\,({\it{new\/}}, {\it{index\/}})\index{channel} $=$ {\rm{cdr}}\,({\rm{channel}}\,({\it{old\/}}, {\it{index\/}})\index{channel})) \\ 
$\wedge$$\;\;\;\;${\rm{critical}}\,({\it{new\/}}, {\it{index\/}})\index{critical} \\ 
$\wedge$$\;\;\;\;${\rm{changed}}\,(\=\+{\it{old\/}}, \\ 
{\it{new\/}}, \\ 
{\rm{list}}\,({\rm{cons}}\,({\tt{'}}{\tt{me}}, {\it{index\/}}), {\rm{cons}}\,({\tt{'}}{\tt{c}}, {\it{index\/}})))\-\index{changed}\- \\ 
{\bf else }{\rm{changed}}\,({\it{old\/}}, {\it{new\/}}, {\bf{nil}})\index{changed}$\;${\bf  endif}\- \\ 
{\bf else }\=\+(\=\+({\rm{ticks}}\,({\it{new\/}}, {\it{index\/}})\index{ticks} $<$ {\rm{ticks}}\,({\it{old\/}}, {\it{index\/}})\index{ticks}) \\ 
$\wedge$$\;\;\;\;${\rm{critical}}\,({\it{new\/}}, {\it{index\/}})\index{critical} \\ 
$\wedge$$\;\;\;\;${\rm{changed}}\,({\it{old\/}}, {\it{new\/}}, {\rm{list}}\,({\rm{cons}}\,({\tt{'}}{\tt{me}}, {\it{index\/}})))\index{changed})\- \\ 
$\vee$$\;\;\;\;$(\=\+{\rm{non-critical}}\,({\it{new\/}}, {\it{index\/}})\index{non-critical} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{length}}\,({\rm{channel}}\,({\it{new\/}}, {\rm{add1-mod}}\,({\it{size\/}}, {\it{index\/}})\index{add1-mod})\index{channel})\index{length} \\ 
$=$$\;\;\;\;$($1\;+$ {\rm{length}}\,({\rm{channel}}\,(\=\+{\it{old\/}}, \\ 
{\rm{add1-mod}}\,(\=\+{\it{size\/}}, \\ 
{\it{index\/}})\-\index{add1-mod})\-\index{channel})\index{length}))\- \\ 
$\wedge$$\;\;\;\;${\rm{changed}}\,(\=\+{\it{old\/}}, \\ 
{\it{new\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{cons}}\,({\tt{'}}{\tt{c}}, {\rm{add1-mod}}\,({\it{size\/}}, {\it{index\/}})\index{add1-mod}), \\ 
{\rm{cons}}\,({\tt{'}}{\tt{me}}, {\it{index\/}}))\-)\-\index{changed})\-\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{me-function} \\  
\=\+{\rm{me-function}}\,({\it{index\/}}, {\it{size\/}}, {\it{state\/}})\index{me-function} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{non-critical}}\,({\it{state\/}}, {\it{index\/}})\index{non-critical} \\ 
{\bf then }\=\+{\bf if }{\rm{token}}\,({\it{state\/}}, {\it{index\/}})\index{token} \\ 
{\bf then }{\rm{update-assoc}}\,(\=\+{\rm{cons}}\,({\tt{'}}{\tt{c}}, {\rm{add1-mod}}\,({\it{size\/}}, {\it{index\/}})\index{add1-mod}), \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{token}}, \\ 
{\rm{channel}}\,(\=\+{\rm{update-assoc}}\,(\=\+{\rm{cons}}\,({\tt{'}}{\tt{c}}, {\it{index\/}}), \\ 
{\rm{cdr}}\,({\rm{channel}}\,(\=\+{\it{state\/}}, \\ 
{\it{index\/}})\-\index{channel}), \\ 
{\it{state\/}})\-\index{update-assoc}, \\ 
{\rm{add1-mod}}\,({\it{size\/}}, {\it{index\/}})\index{add1-mod})\-\index{channel})\-, \\ 
{\rm{update-assoc}}\,(\=\+{\rm{cons}}\,({\tt{'}}{\tt{c}}, {\it{index\/}}), \\ 
{\rm{cdr}}\,({\rm{channel}}\,({\it{state\/}}, {\it{index\/}})\index{channel}), \\ 
{\it{state\/}})\-\index{update-assoc})\-\index{update-assoc} \\ 
{\bf else }{\it{state\/}}$\;${\bf  endif}\- \\ 
{\bf elseif }{\rm{wait}}\,({\it{state\/}}, {\it{index\/}})\index{wait} \\ 
{\bf then }\=\+{\bf if }{\rm{token}}\,({\it{state\/}}, {\it{index\/}})\index{token} \\ 
{\bf then }{\rm{update-assoc}}\,(\=\+{\rm{cons}}\,({\tt{'}}{\tt{c}}, {\it{index\/}}), \\ 
{\rm{cdr}}\,({\rm{channel}}\,({\it{state\/}}, {\it{index\/}})\index{channel}), \\ 
{\rm{update-assoc}}\,({\rm{cons}}\,({\tt{'}}{\tt{me}}, {\it{index\/}}), {\tt{0}}, {\it{state\/}})\index{update-assoc})\-\index{update-assoc} \\ 
{\bf else }{\it{state\/}}$\;${\bf  endif}\- \\ 
{\bf elseif }{\rm{ticks}}\,({\it{state\/}}, {\it{index\/}})\index{ticks} $\simeq {\tt{0}}$ \\ 
{\bf then }{\rm{update-assoc}}\,(\=\+{\rm{cons}}\,({\tt{'}}{\tt{c}}, {\rm{add1-mod}}\,({\it{size\/}}, {\it{index\/}})\index{add1-mod}), \\ 
{\rm{cons}}\,({\tt{'}}{\tt{token}}, {\rm{channel}}\,({\it{state\/}}, {\rm{add1-mod}}\,({\it{size\/}}, {\it{index\/}})\index{add1-mod})\index{channel}), \\ 
{\rm{update-assoc}}\,(\=\+{\rm{cons}}\,({\tt{'}}{\tt{me}}, {\it{index\/}}), \\ 
{\tt{'}}{\tt{non-critical}}, \\ 
{\it{state\/}})\-\index{update-assoc})\-\index{update-assoc} \\ 
{\bf else }{\rm{update-assoc}}\,({\rm{cons}}\,({\tt{'}}{\tt{me}}, {\it{index\/}}), {\rm{ticks}}\,({\it{state\/}}, {\it{index\/}})\index{ticks} $-\;1$, {\it{state\/}})\index{update-assoc}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  total-me \\ \index{total-me}
\=\+(({\it{index\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{index\/}} $<$ {\it{size\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{me}}\,({\it{old\/}}, {\rm{me-function}}\,({\it{index\/}}, {\it{size\/}}, {\it{old\/}})\index{me-function}, {\it{index\/}}, {\it{size\/}})\index{me}\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{program} \\  
\=\+{\rm{program}}\,({\it{index\/}}, {\it{size\/}})\index{program} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{index\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{cons}}\,({\rm{list}}\,({\tt{'}}{\tt{me}}, {\it{index\/}} $-\;1$, {\it{size\/}}), {\rm{program}}\,({\it{index\/}} $-\;1$, {\it{size\/}})\index{program})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{me-prg}$\;\;$
{\rm{me-prg}}\,({\it{size\/}})\index{me-prg} $=$ {\rm{program}}\,({\it{size\/}}, {\it{size\/}})\index{program}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member-program \\ \index{member-program}
\=\+({\it{statement\/}} $\in$ {\rm{program}}\,({\it{index\/}}, {\it{size\/}})\index{program}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{index\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{f}} \\ 
{\bf else }\=\+({\rm{car}}\,({\it{statement\/}}) $=$ {\tt{'}}{\tt{me}}) \\ 
$\wedge$$\;\;\;\;$({\rm{cadr}}\,({\it{statement\/}}) $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\rm{cadr}}\,({\it{statement\/}}) $<$ {\it{index\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{caddr}}\,({\it{statement\/}}) $=$ {\it{size\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{cdddr}}\,({\it{statement\/}}) $=$ {\bf{nil}})\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member-me-prg \\ \index{member-me-prg}
\=\+({\it{statement\/}} $\in$ {\rm{me-prg}}\,({\it{size\/}})\index{me-prg}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{size\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{f}} \\ 
{\bf else }\=\+({\rm{car}}\,({\it{statement\/}}) $=$ {\tt{'}}{\tt{me}}) \\ 
$\wedge$$\;\;\;\;$({\rm{cadr}}\,({\it{statement\/}}) $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\rm{cadr}}\,({\it{statement\/}}) $<$ {\it{size\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{caddr}}\,({\it{statement\/}}) $=$ {\it{size\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{cdddr}}\,({\it{statement\/}}) $=$ {\bf{nil}})\-$\;${\bf  endif}\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable me-prg.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  total-prg \\ \index{total-prg}
{\rm{total}}\,({\rm{me-prg}}\,({\it{size\/}})\index{me-prg})\index{total}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{weight-of-triple} \\  
\=\+{\rm{weight-of-triple}}\,({\it{state\/}}, {\it{index\/}}, {\it{size\/}})\index{weight-of-triple} \\ 
$=$$\;\;\;\;$(\=\+\=\+{\bf if }{\rm{critical}}\,({\it{state\/}}, {\it{index\/}})\index{critical}$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\- \\ 
$+$$\;\;\;\;${\rm{length}}\,({\rm{channel}}\,({\it{state\/}}, {\it{index\/}})\index{channel})\index{length} \\ 
$+$$\;\;\;\;${\rm{length}}\,({\rm{channel}}\,({\it{state\/}}, {\rm{add1-mod}}\,({\it{size\/}}, {\it{index\/}})\index{add1-mod})\index{channel})\index{length})\-\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  weight-of-triple-preserved \\ \index{weight-of-triple-preserved}
\=\+(\=\+({\it{index\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{size\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $<$ {\it{size\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{me}}\,({\it{old\/}}, {\it{new\/}}, {\it{index\/}}, {\it{size\/}})\index{me})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{weight-of-triple}}\,({\it{new\/}}, {\it{index\/}}, {\it{size\/}})\index{weight-of-triple} \\ 
$=$$\;\;\;\;${\rm{weight-of-triple}}\,({\it{old\/}}, {\it{index\/}}, {\it{size\/}})\index{weight-of-triple})\-\-
\end{tabbing}


\begin{tabbing}{\sc Definition}:\index{weight-but-triple} \\  
\=\+{\rm{weight-but-triple}}\,({\it{state\/}}, {\it{index\/}}, {\it{size\/}}, {\it{n\/}})\index{weight-but-triple} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }({\it{n\/}} $-\;1$) $=$ {\it{index\/}} \\ 
{\bf then }{\rm{weight-but-triple}}\,({\it{state\/}}, {\it{index\/}}, {\it{size\/}}, {\it{n\/}} $-\;1$)\index{weight-but-triple} \\ 
{\bf else }\=\+\=\+{\bf if }{\rm{critical}}\,({\it{state\/}}, {\it{n\/}} $-\;1$)\index{critical}$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\- \\ 
$+$$\;\;\;\;$\=\+{\bf if }({\it{n\/}} $-\;1$) $=$ {\rm{add1-mod}}\,({\it{size\/}}, {\it{index\/}})\index{add1-mod}$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\rm{length}}\,({\rm{channel}}\,({\it{state\/}}, {\it{n\/}} $-\;1$)\index{channel})\index{length}$\;${\bf  endif}\- \\ 
$+$$\;\;\;\;${\rm{weight-but-triple}}\,({\it{state\/}}, {\it{index\/}}, {\it{size\/}}, {\it{n\/}} $-\;1$)\index{weight-but-triple}\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  weight-but-triple-preserved \\ \index{weight-but-triple-preserved}
\=\+(({\it{index\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{index\/}} $<$ {\it{size\/}}) $\wedge$ {\rm{me}}\,({\it{old\/}}, {\it{new\/}}, {\it{index\/}}, {\it{size\/}})\index{me}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{weight-but-triple}}\,({\it{new\/}}, {\it{index\/}}, {\it{size\/}}, {\it{n\/}})\index{weight-but-triple} \\ 
$=$$\;\;\;\;${\rm{weight-but-triple}}\,({\it{old\/}}, {\it{index\/}}, {\it{size\/}}, {\it{n\/}})\index{weight-but-triple})\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{weight} \\  
\=\+{\rm{weight}}\,({\it{state\/}}, {\it{size\/}})\index{weight} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{size\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }\=\+\=\+{\bf if }{\rm{critical}}\,({\it{state\/}}, {\it{size\/}} $-\;1$)\index{critical}$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\- \\ 
$+$$\;\;\;\;${\rm{length}}\,({\rm{channel}}\,({\it{state\/}}, {\it{size\/}} $-\;1$)\index{channel})\index{length} \\ 
$+$$\;\;\;\;${\rm{weight}}\,({\it{state\/}}, {\it{size\/}} $-\;1$)\index{weight}\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  weight-is-sum \\ \index{weight-is-sum}
\=\+(({\it{index\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{index\/}} $<$ {\it{size\/}}) $\wedge$ ({\tt{1}} $<$ {\it{size\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{weight}}\,({\it{state\/}}, {\it{n\/}})\index{weight} \\ 
$=$$\;\;\;\;$(\=\+\=\+{\bf if }{\it{index\/}} $<$ {\it{n\/}} \\ 
{\bf then }\=\+\=\+{\bf if }{\rm{critical}}\,({\it{state\/}}, {\it{index\/}})\index{critical}$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\- \\ 
$+$$\;\;\;\;${\rm{length}}\,({\rm{channel}}\,({\it{state\/}}, {\it{index\/}})\index{channel})\index{length}\- \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\- \\ 
$+$$\;\;\;\;$\=\+{\bf if }{\rm{add1-mod}}\,({\it{size\/}}, {\it{index\/}})\index{add1-mod} $<$ {\it{n\/}} \\ 
{\bf then }{\rm{length}}\,({\rm{channel}}\,({\it{state\/}}, {\rm{add1-mod}}\,({\it{size\/}}, {\it{index\/}})\index{add1-mod})\index{channel})\index{length} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\- \\ 
$+$$\;\;\;\;${\rm{weight-but-triple}}\,({\it{state\/}}, {\it{index\/}}, {\it{size\/}}, {\it{n\/}})\index{weight-but-triple})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  weight-preserved-1 \\ \index{weight-preserved-1}
\=\+(\=\+({\it{index\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $<$ {\it{size\/}}) \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{size\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{me}}\,({\it{old\/}}, {\it{new\/}}, {\it{index\/}}, {\it{size\/}})\index{me})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{weight}}\,({\it{new\/}}, {\it{size\/}})\index{weight} $=$ {\rm{weight}}\,({\it{old\/}}, {\it{size\/}})\index{weight})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  weight-preserved-2 \\ \index{weight-preserved-2}
{\rm{me}}\,({\it{old\/}}, {\it{new\/}}, {\tt{0}}, {\tt{1}})\index{me} $\rightarrow$ ({\rm{weight}}\,({\it{new\/}}, {\tt{1}})\index{weight} $=$ {\rm{weight}}\,({\it{old\/}}, {\tt{1}})\index{weight})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  about-size-index \\ \index{about-size-index}
\=\+(({\it{index\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{index\/}} $<$ {\it{size\/}})) \\ 
$\rightarrow$$\;\;\;\;$((({\it{index\/}} $=$ {\tt{0}}) $\wedge$ ({\it{size\/}} $=$ {\tt{1}})) $\vee$ ({\tt{1}} $<$ {\it{size\/}}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  weight-preserved \\ \index{weight-preserved}
\=\+(({\it{index\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{index\/}} $<$ {\it{size\/}}) $\wedge$ {\rm{me}}\,({\it{old\/}}, {\it{new\/}}, {\it{index\/}}, {\it{size\/}})\index{me}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{weight}}\,({\it{new\/}}, {\it{size\/}})\index{weight} $=$ {\rm{weight}}\,({\it{old\/}}, {\it{size\/}})\index{weight})\-
\end{tabbing}


\noindent{\sc Event}:   Disable weight-is-sum.

\addvspace{18pt}

\noindent{\sc Event}:   Disable weight-preserved-1.

\addvspace{18pt}

\noindent{\sc Event}:   Disable weight-preserved-2.

\addvspace{18pt}

\noindent{\sc Event}:   Disable weight-of-triple-preserved.

\addvspace{18pt}

\noindent{\sc Event}:   Disable weight-but-triple-preserved.

\addvspace{18pt}

\noindent{\sc Event}:   Disable total-me.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{mutual-exclusionp} \\  
{\rm{mutual-exclusionp}}\,({\it{state\/}}, {\it{size\/}})\index{mutual-exclusionp} $=$ ({\rm{weight}}\,({\it{state\/}}, {\it{size\/}})\index{weight} $=$ {\tt{1}})
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  mutual-exclusionp-unless-sufficient \\ \index{mutual-exclusionp-unless-sufficie!nt}
{\rm{unless-sufficient}}\,(\=\+{\it{statement\/}}, \\ 
{\rm{me-prg}}\,({\it{size\/}})\index{me-prg}, \\ 
{\it{old\/}}, \\ 
{\it{new\/}}, \\ 
{\tt{`}}{\tt{(}}{\tt{mutual-exclusionp}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{size}}{\tt{)}}, \\ 
{\tt{'}}{\tt{(}}{\tt{false}}{\tt{)}})\-\index{unless-sufficient}
\end{tabbing}


\noindent{\sc Event}:   Disable weight-preserved.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  mutual-exclusionp-prg \\ \index{mutual-exclusionp-prg}
{\rm{unless}}\,({\tt{`}}{\tt{(}}{\tt{mutual-exclusionp}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{size}}{\tt{)}}, {\tt{'}}{\tt{(}}{\tt{false}}{\tt{)}}, {\rm{me-prg}}\,({\it{size\/}})\index{me-prg})\index{unless}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  wait-unless-critical-1 \\ \index{wait-unless-critical-1}
\=\+(\=\+({\it{index\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $<$ {\it{size\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{me}}\,({\it{old\/}}, {\it{new\/}}, {\it{index\/}}, {\it{size\/}})\index{me} \\ 
$\wedge$$\;\;\;\;${\rm{wait}}\,({\it{old\/}}, {\it{index\/}})\index{wait})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{wait}}\,({\it{new\/}}, {\it{index\/}})\index{wait} $\vee$ {\rm{critical}}\,({\it{new\/}}, {\it{index\/}})\index{critical})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  wait-unless-critical-2 \\ \index{wait-unless-critical-2}
\=\+(\=\+({\it{index\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $<$ {\it{size\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{index1\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{index1\/}} $<$ {\it{size\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $\not=$ {\it{index1\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{me}}\,({\it{old\/}}, {\it{new\/}}, {\it{index1\/}}, {\it{size\/}})\index{me} \\ 
$\wedge$$\;\;\;\;${\rm{wait}}\,({\it{old\/}}, {\it{index\/}})\index{wait})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{wait}}\,({\it{new\/}}, {\it{index\/}})\index{wait} $\vee$ {\rm{critical}}\,({\it{new\/}}, {\it{index\/}})\index{critical})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  wait-unless-critical-unless-sufficient \\ \index{wait-unless-critical-unless-suf!ficient}
\=\+(({\it{index\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{index\/}} $<$ {\it{size\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{unless-sufficient}}\,(\=\+{\it{statement\/}}, \\ 
{\rm{me-prg}}\,({\it{size\/}})\index{me-prg}, \\ 
{\it{old\/}}, \\ 
{\it{new\/}}, \\ 
{\tt{`}}{\tt{(}}{\tt{wait}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}, \\ 
{\tt{`}}{\tt{(}}{\tt{critical}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}})\-\index{unless-sufficient}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  wait-unless-critical \\ \index{wait-unless-critical}
\=\+(({\it{index\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{index\/}} $<$ {\it{size\/}}) $\wedge$ ({\it{size\/}} $\not\simeq {\tt{0}}$)) \\ 
$\rightarrow$$\;\;\;\;${\rm{unless}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{wait}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}, \\ 
{\tt{`}}{\tt{(}}{\tt{critical}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}, \\ 
{\rm{me-prg}}\,({\it{size\/}})\index{me-prg})\-\index{unless}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  celcor-ensures-key \\ \index{celcor-ensures-key}
\=\+(({\it{index\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{index\/}} $<$ {\it{size\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{ensures-key}}\,(\=\+{\rm{list}}\,({\tt{'}}{\tt{me}}, {\it{index\/}}, {\it{size\/}}), \\ 
{\rm{me-prg}}\,({\it{size\/}})\index{me-prg}, \\ 
{\it{old\/}}, \\ 
{\it{new\/}}, \\ 
{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{critical}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{lessp}} \\ 
{\tt{(}}{\tt{ticks}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{ticks}}{\tt{)}}{\tt{)}}\-{\tt{)}}\-, \\ 
{\tt{`}}{\tt{(}}\=\+{\tt{or}} \\ 
{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{critical}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}{\tt{lessp}}{\tt{ }}{\tt{(}}{\tt{ticks}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{ticks}}{\tt{)}}{\tt{)}}\- \\ 
{\tt{(}}{\tt{token}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1-mod}}{\tt{ }}{\tt{size}}{\tt{ }}{\tt{index}}{\tt{)}}{\tt{)}}{\tt{)}}\-)\-\index{ensures-key}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  celcor-ensures-rest \\ \index{celcor-ensures-rest}
\=\+(({\it{index\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{index\/}} $<$ {\it{size\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{ensures-rest}}\,(\=\+{\it{statement\/}}, \\ 
{\rm{list}}\,({\tt{'}}{\tt{me}}, {\it{index\/}}, {\it{size\/}}), \\ 
{\rm{me-prg}}\,({\it{size\/}})\index{me-prg}, \\ 
{\it{old\/}}, \\ 
{\it{new\/}}, \\ 
{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{critical}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{lessp}} \\ 
{\tt{(}}{\tt{ticks}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{ticks}}{\tt{)}}{\tt{)}}\-{\tt{)}}\-, \\ 
{\it{q\/}})\-\index{ensures-rest}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  critical-ensures-less-critical-or-right \\ \index{critical-ensures-less-critical-!or-right}
\=\+(({\it{index\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{index\/}} $<$ {\it{size\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{ensures}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{critical}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}{\tt{lessp}}{\tt{ }}{\tt{(}}{\tt{ticks}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{ticks}}{\tt{)}}{\tt{)}}{\tt{)}}\-, \\ 
{\tt{`}}{\tt{(}}\=\+{\tt{or}} \\ 
{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{critical}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}{\tt{lessp}}{\tt{ }}{\tt{(}}{\tt{ticks}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{ticks}}{\tt{)}}{\tt{)}}\- \\ 
{\tt{(}}{\tt{token}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1-mod}}{\tt{ }}{\tt{size}}{\tt{ }}{\tt{index}}{\tt{)}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{me-prg}}\,({\it{size\/}})\index{me-prg})\-\index{ensures}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  critical-unless-less-critical-or-right \\ \index{critical-unless-less-critical-o!r-right}
\=\+(({\it{index\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{index\/}} $<$ {\it{size\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{unless}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{critical}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}{\tt{lessp}}{\tt{ }}{\tt{(}}{\tt{ticks}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{ticks}}{\tt{)}}{\tt{)}}{\tt{)}}\-, \\ 
{\tt{`}}{\tt{(}}\=\+{\tt{or}} \\ 
{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{critical}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}{\tt{lessp}}{\tt{ }}{\tt{(}}{\tt{ticks}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{ticks}}{\tt{)}}{\tt{)}}\- \\ 
{\tt{(}}{\tt{token}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1-mod}}{\tt{ }}{\tt{size}}{\tt{ }}{\tt{index}}{\tt{)}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{me-prg}}\,({\it{size\/}})\index{me-prg})\-\index{unless}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  wlcec-ensures-key \\ \index{wlcec-ensures-key}
\=\+(({\it{index\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{index\/}} $<$ {\it{size\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{ensures-key}}\,(\=\+{\rm{list}}\,({\tt{'}}{\tt{me}}, {\it{index\/}}, {\it{size\/}}), \\ 
{\rm{me-prg}}\,({\it{size\/}})\index{me-prg}, \\ 
{\it{old\/}}, \\ 
{\it{new\/}}, \\ 
{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{wait}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}{\tt{token}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}{\tt{)}}\-, \\ 
{\tt{`}}{\tt{(}}{\tt{critical}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}})\-\index{ensures-key}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  wlcec-ensures-rest \\ \index{wlcec-ensures-rest}
\=\+(({\it{index\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{index\/}} $<$ {\it{size\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{ensures-rest}}\,(\=\+{\it{statement\/}}, \\ 
{\rm{list}}\,({\tt{'}}{\tt{me}}, {\it{index\/}}, {\it{size\/}}), \\ 
{\rm{me-prg}}\,({\it{size\/}})\index{me-prg}, \\ 
{\it{old\/}}, \\ 
{\it{new\/}}, \\ 
{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{wait}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}{\tt{token}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}{\tt{)}}\-, \\ 
{\it{q\/}})\-\index{ensures-rest}\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  wait-and-left-channel-ensures-critial \\ \index{wait-and-left-channel-ensures-c!ritial}
\=\+(({\it{index\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{index\/}} $<$ {\it{size\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{ensures}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{wait}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}{\tt{token}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}{\tt{)}}\-, \\ 
{\tt{`}}{\tt{(}}{\tt{critical}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}, \\ 
{\rm{me-prg}}\,({\it{size\/}})\index{me-prg})\-\index{ensures}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  wait-and-left-channel-unless-critial \\ \index{wait-and-left-channel-unless-criti!al}
\=\+(({\it{index\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{index\/}} $<$ {\it{size\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{unless}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{wait}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}{\tt{token}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}{\tt{)}}\-, \\ 
{\tt{`}}{\tt{(}}{\tt{critical}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}, \\ 
{\rm{me-prg}}\,({\it{size\/}})\index{me-prg})\-\index{unless}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  nclcewlcorc-ensures-key \\ \index{nclcewlcorc-ensures-key}
\=\+(({\it{index\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{index\/}} $<$ {\it{size\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{ensures-key}}\,(\=\+{\rm{list}}\,({\tt{'}}{\tt{me}}, {\it{index\/}}, {\it{size\/}}), \\ 
{\rm{me-prg}}\,({\it{size\/}})\index{me-prg}, \\ 
{\it{old\/}}, \\ 
{\it{new\/}}, \\ 
{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{non-critical}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}{\tt{token}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}{\tt{)}}\-, \\ 
{\tt{`}}{\tt{(}}\=\+{\tt{or}} \\ 
{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{wait}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}{\tt{token}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}{\tt{)}}\- \\ 
{\tt{(}}{\tt{token}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1-mod}}{\tt{ }}{\tt{size}}{\tt{ }}{\tt{index}}{\tt{)}}{\tt{)}}{\tt{)}}\-)\-\index{ensures-key}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  nclcewlcorc-ensures-rest \\ \index{nclcewlcorc-ensures-rest}
\=\+(({\it{index\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{index\/}} $<$ {\it{size\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{ensures-rest}}\,(\=\+{\it{statement\/}}, \\ 
{\rm{list}}\,({\tt{'}}{\tt{me}}, {\it{index\/}}, {\it{size\/}}), \\ 
{\rm{me-prg}}\,({\it{size\/}})\index{me-prg}, \\ 
{\it{old\/}}, \\ 
{\it{new\/}}, \\ 
{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{non-critical}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}{\tt{token}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}{\tt{)}}\-, \\ 
{\it{q\/}})\-\index{ensures-rest}\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  non-critical-left-ensures-wait-left-or-right \\ \index{non-critical-left-ensures-wait-!left-or-right}
\=\+(({\it{index\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{index\/}} $<$ {\it{size\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{ensures}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{non-critical}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}{\tt{token}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}{\tt{)}}\-, \\ 
{\tt{`}}{\tt{(}}\=\+{\tt{or}} \\ 
{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{wait}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}{\tt{token}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}{\tt{)}}\- \\ 
{\tt{(}}{\tt{token}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1-mod}}{\tt{ }}{\tt{size}}{\tt{ }}{\tt{index}}{\tt{)}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{me-prg}}\,({\it{size\/}})\index{me-prg})\-\index{ensures}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  non-critical-left-unless-wait-left-or-right \\ \index{non-critical-left-unless-wait-le!ft-or-right}
\=\+(({\it{index\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{index\/}} $<$ {\it{size\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{unless}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{non-critical}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}{\tt{token}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}{\tt{)}}\-, \\ 
{\tt{`}}{\tt{(}}\=\+{\tt{or}} \\ 
{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{wait}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}{\tt{token}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}{\tt{)}}\- \\ 
{\tt{(}}{\tt{token}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1-mod}}{\tt{ }}{\tt{size}}{\tt{ }}{\tt{index}}{\tt{)}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{me-prg}}\,({\it{size\/}})\index{me-prg})\-\index{unless}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  listp-me-prg \\ \index{listp-me-prg}
({\it{size\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ {\rm{listp}}\,({\rm{me-prg}}\,({\it{size\/}})\index{me-prg})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mutual-exclusionp-is-invariant \\ \index{mutual-exclusionp-is-invariant}
\=\+(\=\+{\rm{initial-condition}}\,({\tt{`}}{\tt{(}}{\tt{mutual-exclusionp}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{size}}{\tt{)}}, {\rm{me-prg}}\,({\it{size\/}})\index{me-prg})\index{initial-condition} \\ 
$\wedge$$\;\;\;\;$({\it{size\/}} $\not\simeq {\tt{0}}$))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{invariant}}\,({\tt{`}}{\tt{(}}{\tt{mutual-exclusionp}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{size}}{\tt{)}}, {\rm{me-prg}}\,({\it{size\/}})\index{me-prg})\index{invariant}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  critical-leads-to-less-critical-or-right \\ \index{critical-leads-to-less-critical!-or-right}
\=\+(({\it{index\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{index\/}} $<$ {\it{size\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{critical}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{lessp}} \\ 
{\tt{(}}{\tt{ticks}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{ticks}}{\tt{)}}{\tt{)}}\-{\tt{)}}\-, \\ 
{\tt{`}}{\tt{(}}\=\+{\tt{or}} \\ 
{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{critical}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}{\tt{lessp}}{\tt{ }}{\tt{(}}{\tt{ticks}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{ticks}}{\tt{)}}{\tt{)}}\- \\ 
{\tt{(}}{\tt{token}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1-mod}}{\tt{ }}{\tt{size}}{\tt{ }}{\tt{index}}{\tt{)}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{me-prg}}\,({\it{size\/}})\index{me-prg})\-\index{leads-to}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  critical-ticks-leads-to-right \\ \index{critical-ticks-leads-to-right}
\=\+(({\it{index\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{index\/}} $<$ {\it{size\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{critical}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{lessp}} \\ 
{\tt{(}}{\tt{ticks}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{ticks}}{\tt{)}}{\tt{)}}\-{\tt{)}}\-, \\ 
{\tt{`}}{\tt{(}}{\tt{token}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1-mod}}{\tt{ }}{\tt{size}}{\tt{ }}{\tt{index}}{\tt{)}}{\tt{)}}, \\ 
{\rm{me-prg}}\,({\it{size\/}})\index{me-prg})\-\index{leads-to}\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  critical-leads-to-right \\ \index{critical-leads-to-right}
\=\+(({\it{index\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{index\/}} $<$ {\it{size\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{critical}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}, \\ 
{\tt{`}}{\tt{(}}{\tt{token}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1-mod}}{\tt{ }}{\tt{size}}{\tt{ }}{\tt{index}}{\tt{)}}{\tt{)}}, \\ 
{\rm{me-prg}}\,({\it{size\/}})\index{me-prg})\-\index{leads-to}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  wait-left-leads-to-critical \\ \index{wait-left-leads-to-critical}
\=\+(({\it{index\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{index\/}} $<$ {\it{size\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{wait}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}{\tt{token}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}{\tt{)}}\-, \\ 
{\tt{`}}{\tt{(}}{\tt{critical}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}, \\ 
{\rm{me-prg}}\,({\it{size\/}})\index{me-prg})\-\index{leads-to}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  non-critical-left-leads-to-wait-left-or-right \\ \index{non-critical-left-leads-to-wait!-left-or-right}
\=\+(({\it{index\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{index\/}} $<$ {\it{size\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{non-critical}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}{\tt{token}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}{\tt{)}}\-, \\ 
{\tt{`}}{\tt{(}}\=\+{\tt{or}} \\ 
{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{wait}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}{\tt{token}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}{\tt{)}}\- \\ 
{\tt{(}}{\tt{token}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1-mod}}{\tt{ }}{\tt{size}}{\tt{ }}{\tt{index}}{\tt{)}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{me-prg}}\,({\it{size\/}})\index{me-prg})\-\index{leads-to}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  wait-left-leads-to-right \\ \index{wait-left-leads-to-right}
\=\+(({\it{index\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{index\/}} $<$ {\it{size\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{wait}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}{\tt{token}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}{\tt{)}}\-, \\ 
{\tt{`}}{\tt{(}}{\tt{token}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1-mod}}{\tt{ }}{\tt{size}}{\tt{ }}{\tt{index}}{\tt{)}}{\tt{)}}, \\ 
{\rm{me-prg}}\,({\it{size\/}})\index{me-prg})\-\index{leads-to}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  non-critical-left-leads-to-right \\ \index{non-critical-left-leads-to-right}
\=\+(({\it{index\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{index\/}} $<$ {\it{size\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{non-critical}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}{\tt{token}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}{\tt{)}}\-, \\ 
{\tt{`}}{\tt{(}}{\tt{token}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1-mod}}{\tt{ }}{\tt{size}}{\tt{ }}{\tt{index}}{\tt{)}}{\tt{)}}, \\ 
{\rm{me-prg}}\,({\it{size\/}})\index{me-prg})\-\index{leads-to}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  critical-wait-non-critical \\ \index{critical-wait-non-critical}
{\rm{critical}}\,({\it{state\/}}, {\it{index\/}})\index{critical} $\vee$ {\rm{wait}}\,({\it{state\/}}, {\it{index\/}})\index{wait} $\vee$ {\rm{non-critical}}\,({\it{state\/}}, {\it{index\/}})\index{non-critical}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{tokens} \\  
\=\+{\rm{tokens}}\,({\it{state\/}}, {\it{size\/}})\index{tokens} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{size\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf elseif }{\rm{token}}\,({\it{state\/}}, {\it{size\/}} $-\;1$)\index{token} \\ 
{\bf then }{\rm{cons}}\,({\it{size\/}} $-\;1$, {\rm{tokens}}\,({\it{state\/}}, {\it{size\/}} $-\;1$)\index{tokens}) \\ 
{\bf else }{\rm{tokens}}\,({\it{state\/}}, {\it{size\/}} $-\;1$)\index{tokens}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{criticals} \\  
\=\+{\rm{criticals}}\,({\it{state\/}}, {\it{size\/}})\index{criticals} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{size\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf elseif }{\rm{critical}}\,({\it{state\/}}, {\it{size\/}} $-\;1$)\index{critical} \\ 
{\bf then }{\rm{cons}}\,({\it{size\/}} $-\;1$, {\rm{criticals}}\,({\it{state\/}}, {\it{size\/}} $-\;1$)\index{criticals}) \\ 
{\bf else }{\rm{criticals}}\,({\it{state\/}}, {\it{size\/}} $-\;1$)\index{criticals}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  equal-plus-1 \\ \index{equal-plus-1}
\=\+(({\it{a\/}} $+$ {\it{b\/}}) $=$ {\tt{1}}) \\ 
$=$$\;\;\;\;$((({\it{a\/}} $=$ {\tt{1}}) $\wedge$ ({\it{b\/}} $\simeq {\tt{0}}$)) $\vee$ (({\it{b\/}} $=$ {\tt{1}}) $\wedge$ ({\it{a\/}} $\simeq {\tt{0}}$)))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  about-mutual-exclusionp \\ \index{about-mutual-exclusionp}
\=\+{\bf if }{\rm{weight}}\,({\it{state\/}}, {\it{size\/}})\index{weight} $\simeq {\tt{0}}$ \\ 
{\bf then }({\rm{tokens}}\,({\it{state\/}}, {\it{size\/}})\index{tokens} $=$ {\bf{nil}}) $\wedge$ ({\rm{criticals}}\,({\it{state\/}}, {\it{size\/}})\index{criticals} $=$ {\bf{nil}}) \\ 
{\bf elseif }{\rm{weight}}\,({\it{state\/}}, {\it{size\/}})\index{weight} $=$ {\tt{1}} \\ 
{\bf then }\=\+(\=\+({\rm{length}}\,({\rm{tokens}}\,({\it{state\/}}, {\it{size\/}})\index{tokens})\index{length} $=$ {\tt{1}}) \\ 
$\wedge$$\;\;\;\;$({\rm{criticals}}\,({\it{state\/}}, {\it{size\/}})\index{criticals} $=$ {\bf{nil}}))\- \\ 
$\vee$$\;\;\;\;$(\=\+({\rm{length}}\,({\rm{criticals}}\,({\it{state\/}}, {\it{size\/}})\index{criticals})\index{length} $=$ {\tt{1}}) \\ 
$\wedge$$\;\;\;\;$({\rm{tokens}}\,({\it{state\/}}, {\it{size\/}})\index{tokens} $=$ {\bf{nil}}))\-\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-
\end{tabbing}


\noindent{\sc Event}:   Disable equal-plus-1.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  numberp-car-tokens \\ \index{numberp-car-tokens}
{\rm{car}}\,({\rm{tokens}}\,({\it{state\/}}, {\it{size\/}})\index{tokens}) $\in\;${\bf{N}}${}$
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  numberp-car-criticals \\ \index{numberp-car-criticals}
{\rm{car}}\,({\rm{criticals}}\,({\it{state\/}}, {\it{size\/}})\index{criticals}) $\in\;${\bf{N}}${}$
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-car-tokens \\ \index{lessp-car-tokens}
({\rm{car}}\,({\rm{tokens}}\,({\it{state\/}}, {\it{size\/}})\index{tokens}) $<$ {\it{size\/}}) $=$ ({\it{size\/}} $\not\simeq {\tt{0}}$)
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-car-criticals \\ \index{lessp-car-criticals}
({\rm{car}}\,({\rm{criticals}}\,({\it{state\/}}, {\it{size\/}})\index{criticals}) $<$ {\it{size\/}}) $=$ ({\it{size\/}} $\not\simeq {\tt{0}}$)
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mutual-exclusionp-requires-state \\ \index{mutual-exclusionp-requires-state}
{\rm{mutual-exclusionp}}\,({\it{state\/}}, {\it{size\/}})\index{mutual-exclusionp} $\rightarrow$ ({\it{size\/}} $\not\simeq {\tt{0}}$)
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-car-tokens-and-criticals \\ \index{lessp-car-tokens-and-criticals}
\=\+{\rm{mutual-exclusionp}}\,({\it{state\/}}, {\it{size\/}})\index{mutual-exclusionp} \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{car}}\,({\rm{tokens}}\,({\it{state\/}}, {\it{size\/}})\index{tokens}) $<$ {\it{size\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\rm{criticals}}\,({\it{state\/}}, {\it{size\/}})\index{criticals}) $<$ {\it{size\/}}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  about-member-list-length-one \\ \index{about-member-list-length-one}
({\rm{length}}\,({\it{list\/}})\index{length} $=$ {\tt{1}}) $\rightarrow$ (({\it{x\/}} $\in$ {\it{list\/}}) $=$ ({\it{x\/}} $=$ {\rm{car}}\,({\it{list\/}})))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  about-member-car-tokens-criticals \\ \index{about-member-car-tokens-critica!ls}
\=\+{\rm{mutual-exclusionp}}\,({\it{state\/}}, {\it{size\/}})\index{mutual-exclusionp} \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+({\it{index\/}} $\in$ {\rm{tokens}}\,({\it{state\/}}, {\it{size\/}})\index{tokens}) \\ 
$=$$\;\;\;\;$(\=\+{\rm{listp}}\,({\rm{tokens}}\,({\it{state\/}}, {\it{size\/}})\index{tokens}) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $=$ {\rm{car}}\,({\rm{tokens}}\,({\it{state\/}}, {\it{size\/}})\index{tokens})))\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+({\it{index\/}} $\in$ {\rm{criticals}}\,({\it{state\/}}, {\it{size\/}})\index{criticals}) \\ 
$=$$\;\;\;\;$(\=\+{\rm{listp}}\,({\rm{criticals}}\,({\it{state\/}}, {\it{size\/}})\index{criticals}) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $=$ {\rm{car}}\,({\rm{criticals}}\,({\it{state\/}}, {\it{size\/}})\index{criticals})))\-)\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  not-member-tokens \\ \index{not-member-tokens}
({\it{index\/}} $\not<$ {\it{size\/}}) $\rightarrow$ ({\it{index\/}} $\not\in$ {\rm{tokens}}\,({\it{state\/}}, {\it{size\/}})\index{tokens})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  not-member-criticals \\ \index{not-member-criticals}
({\it{index\/}} $\not<$ {\it{size\/}}) $\rightarrow$ ({\it{index\/}} $\not\in$ {\rm{criticals}}\,({\it{state\/}}, {\it{size\/}})\index{criticals})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  token-equals \\ \index{token-equals}
\=\+(({\it{index\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{index\/}} $<$ {\it{size\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{token}}\,({\it{state\/}}, {\it{index\/}})\index{token} $=$ ({\it{index\/}} $\in$ {\rm{tokens}}\,({\it{state\/}}, {\it{size\/}})\index{tokens}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  critical-equals \\ \index{critical-equals}
\=\+(({\it{index\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{index\/}} $<$ {\it{size\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{critical}}\,({\it{state\/}}, {\it{index\/}})\index{critical} $=$ ({\it{index\/}} $\in$ {\rm{criticals}}\,({\it{state\/}}, {\it{size\/}})\index{criticals}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mtoken-equals \\ \index{mtoken-equals}
\=\+({\rm{mutual-exclusionp}}\,({\it{state\/}}, {\it{size\/}})\index{mutual-exclusionp} $\wedge$ ({\it{index\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{index\/}} $<$ {\it{size\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{token}}\,({\it{state\/}}, {\it{index\/}})\index{token} \\ 
$=$$\;\;\;\;$(\=\+{\rm{listp}}\,({\rm{tokens}}\,({\it{state\/}}, {\it{size\/}})\index{tokens}) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $=$ {\rm{car}}\,({\rm{tokens}}\,({\it{state\/}}, {\it{size\/}})\index{tokens})))\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mcritical-equals \\ \index{mcritical-equals}
\=\+({\rm{mutual-exclusionp}}\,({\it{state\/}}, {\it{size\/}})\index{mutual-exclusionp} $\wedge$ ({\it{index\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{index\/}} $<$ {\it{size\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{critical}}\,({\it{state\/}}, {\it{index\/}})\index{critical} \\ 
$=$$\;\;\;\;$(\=\+{\rm{listp}}\,({\rm{criticals}}\,({\it{state\/}}, {\it{size\/}})\index{criticals}) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $=$ {\rm{car}}\,({\rm{criticals}}\,({\it{state\/}}, {\it{size\/}})\index{criticals})))\-)\-\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  mutual-exclusionp-implies \\ \index{mutual-exclusionp-implies}
\=\+{\rm{mutual-exclusionp}}\,({\it{state\/}}, {\it{size\/}})\index{mutual-exclusionp} \\ 
$\rightarrow$$\;\;\;\;$({\rm{listp}}\,({\rm{tokens}}\,({\it{state\/}}, {\it{size\/}})\index{tokens}) $\leftrightarrow$ ($\neg$ {\rm{listp}}\,({\rm{criticals}}\,({\it{state\/}}, {\it{size\/}})\index{criticals})))\-
\end{tabbing}


\noindent{\sc Event}:   Disable lessp-car-criticals.

\addvspace{18pt}

\noindent{\sc Event}:   Disable lessp-car-tokens.

\addvspace{18pt}

\noindent{\sc Event}:   Disable about-member-list-length-one.

\addvspace{18pt}

\noindent{\sc Event}:   Disable not-member-tokens.

\addvspace{18pt}

\noindent{\sc Event}:   Disable not-member-criticals.

\addvspace{18pt}


\noindent{\sc Event}:   Disable token.

\addvspace{18pt}

\noindent{\sc Event}:   Disable critical.

\addvspace{18pt}

\noindent{\sc Event}:   Disable non-critical.

\addvspace{18pt}

\noindent{\sc Event}:   Disable wait.

\addvspace{18pt}

\noindent{\sc Event}:   Disable mutual-exclusionp.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  mutual-exclusionp-implies-prg \\ \index{mutual-exclusionp-implies-prg}
{\rm{mutual-exclusionp}}\,({\it{state\/}}, {\it{size\/}})\index{mutual-exclusionp} $\rightarrow$ {\rm{listp}}\,({\rm{me-prg}}\,({\it{size\/}})\index{me-prg})
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  left-leads-to-right \\ \index{left-leads-to-right}
\=\+(\=\+({\it{index\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $<$ {\it{size\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{initial-condition}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{mutual-exclusionp}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{size}}{\tt{)}}, \\ 
{\rm{me-prg}}\,({\it{size\/}})\index{me-prg})\-\index{initial-condition})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{token}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}, \\ 
{\tt{`}}{\tt{(}}{\tt{token}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1-mod}}{\tt{ }}{\tt{size}}{\tt{ }}{\tt{index}}{\tt{)}}{\tt{)}}, \\ 
{\rm{me-prg}}\,({\it{size\/}})\index{me-prg})\-\index{leads-to}\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{walk-ring} \\  
\=\+{\rm{walk-ring}}\,({\it{a\/}}, {\it{b\/}}, {\it{size\/}})\index{walk-ring} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{a\/}} $\in\;${\bf{N}}${}$ \\ 
{\bf then }\=\+{\bf if }{\it{b\/}} $\in\;${\bf{N}}${}$ \\ 
{\bf then }\=\+{\bf if }{\it{a\/}} $<$ {\it{size\/}} \\ 
{\bf then }\=\+{\bf if }{\it{b\/}} $<$ {\it{size\/}} \\ 
{\bf then }\=\+{\bf if }{\it{a\/}} $=$ {\it{b\/}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{walk-ring}}\,({\rm{add1-mod}}\,({\it{size\/}}, {\it{a\/}})\index{add1-mod}, {\it{b\/}}, {\it{size\/}})\index{walk-ring}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  any-left-leads-to-right \\ \index{any-left-leads-to-right}
\=\+(\=\+({\it{left\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{left\/}} $<$ {\it{size\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{right\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{right\/}} $<$ {\it{size\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{initial-condition}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{mutual-exclusionp}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{size}}{\tt{)}}, \\ 
{\rm{me-prg}}\,({\it{size\/}})\index{me-prg})\-\index{initial-condition})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{token}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{left}}{\tt{)}}, \\ 
{\tt{`}}{\tt{(}}{\tt{token}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{right}}{\tt{)}}, \\ 
{\rm{me-prg}}\,({\it{size\/}})\index{me-prg})\-\index{leads-to}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-add1-mod-size \\ \index{lessp-add1-mod-size}
{\rm{mutual-exclusionp}}\,({\it{state\/}}, {\it{size\/}})\index{mutual-exclusionp} $\rightarrow$ ({\rm{add1-mod}}\,({\it{size\/}}, {\it{n\/}})\index{add1-mod} $<$ {\it{size\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  any-critical-leads-to-right \\ \index{any-critical-leads-to-right}
\=\+(\=\+({\it{left\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{left\/}} $<$ {\it{size\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{right\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{right\/}} $<$ {\it{size\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{initial-condition}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{mutual-exclusionp}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{size}}{\tt{)}}, \\ 
{\rm{me-prg}}\,({\it{size\/}})\index{me-prg})\-\index{initial-condition})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{critical}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{left}}{\tt{)}}, \\ 
{\tt{`}}{\tt{(}}{\tt{token}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{right}}{\tt{)}}, \\ 
{\rm{me-prg}}\,({\it{size\/}})\index{me-prg})\-\index{leads-to}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  any-leads-to-right \\ \index{any-leads-to-right}
\=\+(\=\+({\it{index\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $<$ {\it{size\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{initial-condition}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{mutual-exclusionp}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{size}}{\tt{)}}, \\ 
{\rm{me-prg}}\,({\it{size\/}})\index{me-prg})\-\index{initial-condition})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,({\tt{'}}{\tt{(}}{\tt{true}}{\tt{)}}, {\tt{`}}{\tt{(}}{\tt{token}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}, {\rm{me-prg}}\,({\it{size\/}})\index{me-prg})\index{leads-to}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  me-prg-non-zero-size \\ \index{me-prg-non-zero-size}
{\rm{listp}}\,({\rm{me-prg}}\,({\it{size\/}})\index{me-prg}) $=$ ({\it{size\/}} $\not\simeq {\tt{0}}$)
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  wait-leads-to-left-wait-or-critical \\ \index{wait-leads-to-left-wait-or-criti!cal}
\=\+(\=\+({\it{index\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $<$ {\it{size\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{initial-condition}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{mutual-exclusionp}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{size}}{\tt{)}}, \\ 
{\rm{me-prg}}\,({\it{size\/}})\index{me-prg})\-\index{initial-condition})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{and}}{\tt{ }}{\tt{(}}{\tt{true}}{\tt{)}}{\tt{ }}{\tt{(}}{\tt{wait}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}{\tt{)}}, \\ 
{\tt{`}}{\tt{(}}\=\+{\tt{or}} \\ 
{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{token}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}{\tt{wait}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}{\tt{)}}\- \\ 
{\tt{(}}{\tt{critical}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{me-prg}}\,({\it{size\/}})\index{me-prg})\-\index{leads-to}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  wait-leads-to-critical \\ \index{wait-leads-to-critical}
\=\+(\=\+({\it{index\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $<$ {\it{size\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{initial-condition}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{mutual-exclusionp}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{size}}{\tt{)}}, \\ 
{\rm{me-prg}}\,({\it{size\/}})\index{me-prg})\-\index{initial-condition})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{wait}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}, \\ 
{\tt{`}}{\tt{(}}{\tt{critical}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}, \\ 
{\rm{me-prg}}\,({\it{size\/}})\index{me-prg})\-\index{leads-to}\-
\end{tabbing}

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