\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};;; The Program

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

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

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

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

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

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

\begin{tabbing}{\sc Definition}:\index{owns-left} \\  
{\rm{owns-left}}\,({\it{state\/}}, {\it{index\/}})\index{owns-left} $=$ ({\rm{fork}}\,({\it{state\/}}, {\it{index\/}})\index{fork} $=$ {\it{index\/}})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{owns-right} \\  
{\rm{owns-right}}\,({\it{state\/}}, {\it{index\/}}, {\it{n\/}})\index{owns-right} $=$ ({\rm{fork}}\,({\it{state\/}}, {\rm{add1-mod}}\,({\it{n\/}}, {\it{index\/}})\index{add1-mod})\index{fork} $=$ {\it{index\/}})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{thinking-to} \\  
\=\+{\rm{thinking-to}}\,({\it{old\/}}, {\it{new\/}}, {\it{index\/}})\index{thinking-to} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{thinking}}\,({\it{old\/}}, {\it{index\/}})\index{thinking} \\ 
{\bf then }\=\+({\rm{thinking}}\,({\it{new\/}}, {\it{index\/}})\index{thinking} $\vee$ {\rm{hungry}}\,({\it{new\/}}, {\it{index\/}})\index{hungry}) \\ 
$\wedge$$\;\;\;\;${\rm{changed}}\,({\it{old\/}}, {\it{new\/}}, {\rm{list}}\,({\rm{cons}}\,({\tt{'}}{\tt{s}}, {\it{index\/}})))\index{changed}\- \\ 
{\bf else }{\rm{changed}}\,({\it{old\/}}, {\it{new\/}}, {\bf{nil}})\index{changed}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{hungry-left} \\  
\=\+{\rm{hungry-left}}\,({\it{old\/}}, {\it{new\/}}, {\it{index\/}})\index{hungry-left} \\ 
$=$$\;\;\;\;$(\=\+{\rm{hungry}}\,({\it{old\/}}, {\it{index\/}})\index{hungry} \\ 
$\wedge$$\;\;\;\;${\rm{free}}\,({\it{old\/}}, {\it{index\/}})\index{free} \\ 
$\wedge$$\;\;\;\;${\rm{owns-left}}\,({\it{new\/}}, {\it{index\/}})\index{owns-left} \\ 
$\wedge$$\;\;\;\;${\rm{changed}}\,({\it{old\/}}, {\it{new\/}}, {\rm{list}}\,({\rm{cons}}\,({\tt{'}}{\tt{f}}, {\it{index\/}})))\index{changed})\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{hungry-right} \\  
\=\+{\rm{hungry-right}}\,({\it{old\/}}, {\it{new\/}}, {\it{index\/}}, {\it{n\/}})\index{hungry-right} \\ 
$=$$\;\;\;\;$(\=\+{\rm{hungry}}\,({\it{old\/}}, {\it{index\/}})\index{hungry} \\ 
$\wedge$$\;\;\;\;${\rm{free}}\,({\it{old\/}}, {\rm{add1-mod}}\,({\it{n\/}}, {\it{index\/}})\index{add1-mod})\index{free} \\ 
$\wedge$$\;\;\;\;${\rm{owns-right}}\,({\it{new\/}}, {\it{index\/}}, {\it{n\/}})\index{owns-right} \\ 
$\wedge$$\;\;\;\;${\rm{changed}}\,({\it{old\/}}, {\it{new\/}}, {\rm{list}}\,({\rm{cons}}\,({\tt{'}}{\tt{f}}, {\rm{add1-mod}}\,({\it{n\/}}, {\it{index\/}})\index{add1-mod})))\index{changed})\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{hungry-both} \\  
\=\+{\rm{hungry-both}}\,({\it{old\/}}, {\it{new\/}}, {\it{index\/}}, {\it{n\/}})\index{hungry-both} \\ 
$=$$\;\;\;\;$\=\+{\bf if }\=\+{\rm{hungry}}\,({\it{old\/}}, {\it{index\/}})\index{hungry} \\ 
$\wedge$$\;\;\;\;${\rm{owns-left}}\,({\it{old\/}}, {\it{index\/}})\index{owns-left} \\ 
$\wedge$$\;\;\;\;${\rm{owns-right}}\,({\it{old\/}}, {\it{index\/}}, {\it{n\/}})\index{owns-right}\- \\ 
{\bf then }{\rm{eating}}\,({\it{new\/}}, {\it{index\/}})\index{eating} $\wedge$ {\rm{changed}}\,({\it{old\/}}, {\it{new\/}}, {\rm{list}}\,({\rm{cons}}\,({\tt{'}}{\tt{s}}, {\it{index\/}})))\index{changed} \\ 
{\bf else }{\rm{changed}}\,({\it{old\/}}, {\it{new\/}}, {\bf{nil}})\index{changed}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{eating-to} \\  
\=\+{\rm{eating-to}}\,({\it{old\/}}, {\it{new\/}}, {\it{index\/}}, {\it{n\/}})\index{eating-to} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{eating}}\,({\it{old\/}}, {\it{index\/}})\index{eating} \\ 
{\bf then }\=\+{\rm{thinking}}\,({\it{new\/}}, {\it{index\/}})\index{thinking} \\ 
$\wedge$$\;\;\;\;${\rm{free}}\,({\it{new\/}}, {\it{index\/}})\index{free} \\ 
$\wedge$$\;\;\;\;${\rm{free}}\,({\it{new\/}}, {\rm{add1-mod}}\,({\it{n\/}}, {\it{index\/}})\index{add1-mod})\index{free} \\ 
$\wedge$$\;\;\;\;${\rm{changed}}\,(\=\+{\it{old\/}}, \\ 
{\it{new\/}}, \\ 
{\rm{list}}\,(\=\+{\rm{cons}}\,({\tt{'}}{\tt{s}}, {\it{index\/}}), \\ 
{\rm{cons}}\,({\tt{'}}{\tt{f}}, {\it{index\/}}), \\ 
{\rm{cons}}\,({\tt{'}}{\tt{f}}, {\rm{add1-mod}}\,({\it{n\/}}, {\it{index\/}})\index{add1-mod}))\-)\-\index{changed}\- \\ 
{\bf else }{\rm{changed}}\,({\it{old\/}}, {\it{new\/}}, {\bf{nil}})\index{changed}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{phil} \\  
\=\+{\rm{phil}}\,({\it{index\/}}, {\it{n\/}})\index{phil} \\ 
$=$$\;\;\;\;${\rm{list}}\,(\=\+{\rm{list}}\,({\tt{'}}{\tt{thinking-to}}, {\it{index\/}}), \\ 
{\rm{list}}\,({\tt{'}}{\tt{hungry-left}}, {\it{index\/}}), \\ 
{\rm{list}}\,({\tt{'}}{\tt{hungry-right}}, {\it{index\/}}, {\it{n\/}}), \\ 
{\rm{list}}\,({\tt{'}}{\tt{hungry-both}}, {\it{index\/}}, {\it{n\/}}), \\ 
{\rm{list}}\,({\tt{'}}{\tt{eating-to}}, {\it{index\/}}, {\it{n\/}}))\-\-
\end{tabbing}

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

\begin{tabbing}{\sc Definition}:\index{phil-prg}$\;\;$
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg} $=$ {\rm{ring}}\,({\it{n\/}}, {\it{n\/}})\index{ring}
\end{tabbing}


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

\addvspace{18pt}

\noindent{\sc Event}:   Disable *1*phil-prg.

\addvspace{18pt}


\begin{verbatim};;; Correctness


\end{verbatim}\begin{tabbing}{\sc Theorem}:  member-ring \\ \index{member-ring}
\=\+({\it{statement\/}} $\in$ {\rm{ring}}\,({\it{index\/}}, {\it{n\/}})\index{ring}) \\ 
$=$$\;\;\;\;$(\=\+({\it{statement\/}} $\in$ {\rm{phil}}\,({\rm{cadr}}\,({\it{statement\/}}), {\it{n\/}})\index{phil}) \\ 
$\wedge$$\;\;\;\;$({\rm{cadr}}\,({\it{statement\/}}) $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\rm{cadr}}\,({\it{statement\/}}) $<$ {\it{index\/}}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member-phil-prg \\ \index{member-phil-prg}
\=\+({\it{statement\/}} $\in$ {\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg}) \\ 
$=$$\;\;\;\;$(\=\+({\it{statement\/}} $\in$ {\rm{phil}}\,({\rm{cadr}}\,({\it{statement\/}}), {\it{n\/}})\index{phil}) \\ 
$\wedge$$\;\;\;\;$({\rm{cadr}}\,({\it{statement\/}}) $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\rm{cadr}}\,({\it{statement\/}}) $<$ {\it{n\/}}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{proper-forks-rec} \\  
\=\+{\rm{proper-forks-rec}}\,({\it{state\/}}, {\it{index\/}}, {\it{n\/}})\index{proper-forks-rec} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{index\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }\=\+(\=\+{\rm{free}}\,({\it{state\/}}, {\it{index\/}} $-\;1$)\index{free} \\ 
$\vee$$\;\;\;\;$({\rm{fork}}\,({\it{state\/}}, {\it{index\/}} $-\;1$)\index{fork} $=$ ({\it{index\/}} $-\;1$)) \\ 
$\vee$$\;\;\;\;$({\rm{fork}}\,({\it{state\/}}, {\it{index\/}} $-\;1$)\index{fork} $=$ {\rm{sub1-mod}}\,({\it{n\/}}, {\it{index\/}} $-\;1$)\index{sub1-mod}))\- \\ 
$\wedge$$\;\;\;\;${\rm{proper-forks-rec}}\,({\it{state\/}}, {\it{index\/}} $-\;1$, {\it{n\/}})\index{proper-forks-rec}\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  proper-forks-rec-implies \\ \index{proper-forks-rec-implies}
\=\+(\=\+{\rm{proper-forks-rec}}\,({\it{state\/}}, {\it{index\/}}, {\it{n\/}})\index{proper-forks-rec} \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not<$ {\it{index\/}}) \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\it{index\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\in\;${\bf{N}}${}$))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{free}}\,({\it{state\/}}, {\it{i\/}})\index{free} \\ 
$\vee$$\;\;\;\;$({\rm{fork}}\,({\it{state\/}}, {\it{i\/}})\index{fork} $=$ {\it{i\/}}) \\ 
$\vee$$\;\;\;\;$({\rm{fork}}\,({\it{state\/}}, {\it{i\/}})\index{fork} $=$ {\rm{sub1-mod}}\,({\it{n\/}}, {\it{i\/}})\index{sub1-mod}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{proper-forks}$\;\;$
{\rm{proper-forks}}\,({\it{state\/}}, {\it{n\/}})\index{proper-forks} $=$ {\rm{proper-forks-rec}}\,({\it{state\/}}, {\it{n\/}}, {\it{n\/}})\index{proper-forks-rec}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  proper-forks-implies \\ \index{proper-forks-implies}
\=\+({\rm{proper-forks}}\,({\it{state\/}}, {\it{n\/}})\index{proper-forks} $\wedge$ ({\tt{1}} $<$ {\it{n\/}}) $\wedge$ ({\it{i\/}} $<$ {\it{n\/}}) $\wedge$ ({\it{i\/}} $\in\;${\bf{N}}${}$)) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{free}}\,({\it{state\/}}, {\it{i\/}})\index{free} \\ 
$\vee$$\;\;\;\;$({\rm{fork}}\,({\it{state\/}}, {\it{i\/}})\index{fork} $=$ {\it{i\/}}) \\ 
$\vee$$\;\;\;\;$({\rm{fork}}\,({\it{state\/}}, {\it{i\/}})\index{fork} $=$ {\rm{sub1-mod}}\,({\it{n\/}}, {\it{i\/}})\index{sub1-mod}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{proper-phil} \\  
\=\+{\rm{proper-phil}}\,({\it{state\/}}, {\it{phil\/}}, {\it{right\/}})\index{proper-phil} \\ 
$=$$\;\;\;\;$(\=\+(\=\+{\rm{thinking}}\,({\it{state\/}}, {\it{phil\/}})\index{thinking} \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{fork}}\,({\it{state\/}}, {\it{phil\/}})\index{fork} $\not=$ {\it{phil\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{fork}}\,({\it{state\/}}, {\it{right\/}})\index{fork} $\not=$ {\it{phil\/}}))\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{eating}}\,({\it{state\/}}, {\it{phil\/}})\index{eating} \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{fork}}\,({\it{state\/}}, {\it{phil\/}})\index{fork} $=$ {\it{phil\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{fork}}\,({\it{state\/}}, {\it{right\/}})\index{fork} $=$ {\it{phil\/}}))\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{thinking}}\,({\it{state\/}}, {\it{phil\/}})\index{thinking} \\ 
$\vee$$\;\;\;\;${\rm{hungry}}\,({\it{state\/}}, {\it{phil\/}})\index{hungry} \\ 
$\vee$$\;\;\;\;${\rm{eating}}\,({\it{state\/}}, {\it{phil\/}})\index{eating})\-)\-\-
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  proper-phils-rec-implies-proper-phil \\ \index{proper-phils-rec-implies-proper!-phil}
\=\+(\=\+{\rm{proper-phils-rec}}\,({\it{state\/}}, {\it{index\/}}, {\it{n\/}})\index{proper-phils-rec} \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not<$ {\it{index\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{phil\/}} $<$ {\it{index\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{phil\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{right\/}} $=$ {\rm{add1-mod}}\,({\it{n\/}}, {\it{phil\/}})\index{add1-mod}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{proper-phil}}\,({\it{state\/}}, {\it{phil\/}}, {\it{right\/}})\index{proper-phil}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  proper-phils-rec-implies \\ \index{proper-phils-rec-implies}
\=\+(\=\+{\rm{proper-phils-rec}}\,({\it{state\/}}, {\it{index\/}}, {\it{n\/}})\index{proper-phils-rec} \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not<$ {\it{index\/}}) \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{phil\/}} $<$ {\it{index\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{phil\/}} $\in\;${\bf{N}}${}$))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+{\rm{thinking}}\,({\it{state\/}}, {\it{phil\/}})\index{thinking} \\ 
$\rightarrow$$\;\;\;\;$(\=\+($\neg$ {\rm{owns-left}}\,({\it{state\/}}, {\it{phil\/}})\index{owns-left}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{owns-right}}\,({\it{state\/}}, {\it{phil\/}}, {\it{n\/}})\index{owns-right}))\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{eating}}\,({\it{state\/}}, {\it{phil\/}})\index{eating} \\ 
$\rightarrow$$\;\;\;\;$({\rm{owns-left}}\,({\it{state\/}}, {\it{phil\/}})\index{owns-left} $\wedge$ {\rm{owns-right}}\,({\it{state\/}}, {\it{phil\/}}, {\it{n\/}})\index{owns-right}))\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{thinking}}\,({\it{state\/}}, {\it{phil\/}})\index{thinking} \\ 
$\vee$$\;\;\;\;${\rm{hungry}}\,({\it{state\/}}, {\it{phil\/}})\index{hungry} \\ 
$\vee$$\;\;\;\;${\rm{eating}}\,({\it{state\/}}, {\it{phil\/}})\index{eating})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{proper-phils}$\;\;$
{\rm{proper-phils}}\,({\it{state\/}}, {\it{n\/}})\index{proper-phils} $=$ {\rm{proper-phils-rec}}\,({\it{state\/}}, {\it{n\/}}, {\it{n\/}})\index{proper-phils-rec}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  proper-phils-implies-proper-phil \\ \index{proper-phils-implies-proper-phi!l}
\=\+(\=\+{\rm{proper-phils}}\,({\it{state\/}}, {\it{n\/}})\index{proper-phils} \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{phil\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{phil\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{right\/}} $=$ {\rm{add1-mod}}\,({\it{n\/}}, {\it{phil\/}})\index{add1-mod}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{proper-phil}}\,({\it{state\/}}, {\it{phil\/}}, {\it{right\/}})\index{proper-phil}\-
\end{tabbing}



\begin{tabbing}{\sc Definition}:\index{all-lefts} \\  
\=\+{\rm{all-lefts}}\,({\it{state\/}}, {\it{index\/}})\index{all-lefts} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{index\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }\=\+{\rm{owns-left}}\,({\it{state\/}}, {\it{index\/}} $-\;1$)\index{owns-left} \\ 
$\wedge$$\;\;\;\;${\rm{hungry}}\,({\it{state\/}}, {\it{index\/}} $-\;1$)\index{hungry} \\ 
$\wedge$$\;\;\;\;${\rm{all-lefts}}\,({\it{state\/}}, {\it{index\/}} $-\;1$)\index{all-lefts}\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-lefts-implies \\ \index{all-lefts-implies}
\=\+(({\it{i\/}} $<$ {\it{n\/}}) $\wedge$ ({\it{i\/}} $\in\;${\bf{N}}${}$) $\wedge$ {\rm{all-lefts}}\,({\it{state\/}}, {\it{n\/}})\index{all-lefts}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{hungry}}\,({\it{state\/}}, {\it{i\/}})\index{hungry} $\wedge$ {\rm{owns-left}}\,({\it{state\/}}, {\it{i\/}})\index{owns-left})\-
\end{tabbing}


\begin{tabbing}{\sc Definition}:\index{all-rights-rec} \\  
\=\+{\rm{all-rights-rec}}\,({\it{state\/}}, {\it{index\/}}, {\it{n\/}})\index{all-rights-rec} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{index\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }\=\+{\rm{owns-right}}\,({\it{state\/}}, {\it{index\/}} $-\;1$, {\it{n\/}})\index{owns-right} \\ 
$\wedge$$\;\;\;\;${\rm{hungry}}\,({\it{state\/}}, {\it{index\/}} $-\;1$)\index{hungry} \\ 
$\wedge$$\;\;\;\;${\rm{all-rights-rec}}\,({\it{state\/}}, {\it{index\/}} $-\;1$, {\it{n\/}})\index{all-rights-rec}\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-rights-rec-implies \\ \index{all-rights-rec-implies}
\=\+(\=\+({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not<$ {\it{index\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\it{index\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{all-rights-rec}}\,({\it{state\/}}, {\it{index\/}}, {\it{n\/}})\index{all-rights-rec})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{hungry}}\,({\it{state\/}}, {\it{i\/}})\index{hungry} $\wedge$ {\rm{owns-right}}\,({\it{state\/}}, {\it{i\/}}, {\it{n\/}})\index{owns-right})\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{all-rights}$\;\;$
{\rm{all-rights}}\,({\it{state\/}}, {\it{n\/}})\index{all-rights} $=$ {\rm{all-rights-rec}}\,({\it{state\/}}, {\it{n\/}}, {\it{n\/}})\index{all-rights-rec}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-rights-implies \\ \index{all-rights-implies}
\=\+(({\tt{1}} $<$ {\it{n\/}}) $\wedge$ ({\it{i\/}} $<$ {\it{n\/}}) $\wedge$ ({\it{i\/}} $\in\;${\bf{N}}${}$) $\wedge$ {\rm{all-rights}}\,({\it{state\/}}, {\it{n\/}})\index{all-rights}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{hungry}}\,({\it{state\/}}, {\it{i\/}})\index{hungry} $\wedge$ {\rm{owns-right}}\,({\it{state\/}}, {\it{i\/}}, {\it{n\/}})\index{owns-right})\-
\end{tabbing}


\begin{verbatim};(defn initial (state n)
;  (and (proper-forks state n)
;       (proper-phils state n)))

\end{verbatim}\begin{tabbing}{\sc Theorem}:  listp-phil-prg \\ \index{listp-phil-prg}
{\rm{listp}}\,({\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg}) $=$ ({\it{n\/}} $\not\simeq {\tt{0}}$)
\end{tabbing}


\begin{tabbing}{\sc Definition}:\index{pfusi} \\  
\=\+{\rm{pfusi}}\,({\it{index\/}}, {\it{n\/}}, {\it{statement\/}})\index{pfusi} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{index\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }({\it{index\/}} $-\;1$) $=$ {\rm{cadr}}\,({\it{statement\/}}) \\ 
{\bf then }{\rm{pfusi}}\,({\it{index\/}} $-\;1$, {\it{n\/}}, {\it{statement\/}})\index{pfusi} \\ 
{\bf elseif }({\it{index\/}} $-\;1$) $=$ {\rm{add1-mod}}\,({\it{n\/}}, {\rm{cadr}}\,({\it{statement\/}}))\index{add1-mod} \\ 
{\bf then }{\rm{pfusi}}\,({\it{index\/}} $-\;1$, {\it{n\/}}, {\it{statement\/}})\index{pfusi} \\ 
{\bf else }{\rm{pfusi}}\,({\it{index\/}} $-\;1$, {\it{n\/}}, {\it{statement\/}})\index{pfusi}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  proper-forks-rec-unless-sufficient \\ \index{proper-forks-rec-unless-sufficie!nt}
\=\+(({\it{n\/}} $\not<$ {\it{index\/}}) $\wedge$ ({\tt{1}} $<$ {\it{n\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{unless-sufficient}}\,(\=\+{\it{statement\/}}, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg}, \\ 
{\it{old\/}}, \\ 
{\it{new\/}}, \\ 
{\tt{`}}{\tt{(}}{\tt{proper-forks-rec}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}, \\ 
{\tt{'}}{\tt{(}}{\tt{false}}{\tt{)}})\-\index{unless-sufficient}\-
\end{tabbing}


\begin{tabbing}{\sc Definition}:\index{proper-triple} \\  
\=\+{\rm{proper-triple}}\,({\it{state\/}}, {\it{phil\/}}, {\it{n\/}})\index{proper-triple} \\ 
$=$$\;\;\;\;$(\=\+{\rm{proper-phil}}\,({\it{state\/}}, {\rm{sub1-mod}}\,({\it{n\/}}, {\it{phil\/}})\index{sub1-mod}, {\rm{add1-mod}}\,({\it{n\/}}, {\rm{sub1-mod}}\,({\it{n\/}}, {\it{phil\/}})\index{sub1-mod})\index{add1-mod})\index{proper-phil} \\ 
$\wedge$$\;\;\;\;${\rm{proper-phil}}\,({\it{state\/}}, {\it{phil\/}}, {\rm{add1-mod}}\,({\it{n\/}}, {\it{phil\/}})\index{add1-mod})\index{proper-phil} \\ 
$\wedge$$\;\;\;\;${\rm{proper-phil}}\,(\=\+{\it{state\/}}, \\ 
{\rm{add1-mod}}\,({\it{n\/}}, {\it{phil\/}})\index{add1-mod}, \\ 
{\rm{add1-mod}}\,({\it{n\/}}, {\rm{add1-mod}}\,({\it{n\/}}, {\it{phil\/}})\index{add1-mod})\index{add1-mod})\-\index{proper-phil})\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{but-triple} \\  
\=\+{\rm{but-triple}}\,({\it{state\/}}, {\it{index\/}}, {\it{phil\/}}, {\it{n\/}})\index{but-triple} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{index\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }\=\+(({\it{index\/}} $-\;1$) $=$ {\rm{sub1-mod}}\,({\it{n\/}}, {\it{phil\/}})\index{sub1-mod}) \\ 
$\vee$$\;\;\;\;$(({\it{index\/}} $-\;1$) $=$ {\it{phil\/}}) \\ 
$\vee$$\;\;\;\;$(({\it{index\/}} $-\;1$) $=$ {\rm{add1-mod}}\,({\it{n\/}}, {\it{phil\/}})\index{add1-mod})\- \\ 
{\bf then }{\rm{but-triple}}\,({\it{state\/}}, {\it{index\/}} $-\;1$, {\it{phil\/}}, {\it{n\/}})\index{but-triple} \\ 
{\bf else }\=\+{\rm{proper-phil}}\,({\it{state\/}}, {\it{index\/}} $-\;1$, {\rm{add1-mod}}\,({\it{n\/}}, {\it{index\/}} $-\;1$)\index{add1-mod})\index{proper-phil} \\ 
$\wedge$$\;\;\;\;${\rm{but-triple}}\,({\it{state\/}}, {\it{index\/}} $-\;1$, {\it{phil\/}}, {\it{n\/}})\index{but-triple}\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-1 \\ \index{lessp-1}
({\tt{1}} $<$ {\it{n\/}}) $=$ (({\it{n\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{n\/}} $\not=$ {\tt{1}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-2 \\ \index{lessp-2}
({\it{x\/}} $<$ {\tt{2}}) $=$ (({\it{x\/}} $=$ {\tt{1}}) $\vee$ ({\it{x\/}} $\simeq {\tt{0}}$))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-2-2 \\ \index{lessp-2-2}
({\tt{2}} $<$ {\it{x\/}}) $=$ (({\it{x\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{x\/}} $\not=$ {\tt{1}}) $\wedge$ ({\it{x\/}} $\not=$ {\tt{2}}))
\end{tabbing}

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

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

\begin{tabbing}{\sc Theorem}:  but-triple-and-triple-all \\ \index{but-triple-and-triple-all}
\=\+(({\it{phil\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{n\/}} $\not<$ {\it{index\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{proper-phils-rec}}\,({\it{state\/}}, {\it{index\/}}, {\it{n\/}})\index{proper-phils-rec} \\ 
$=$$\;\;\;\;$(\=\+{\rm{but-triple}}\,({\it{state\/}}, {\it{index\/}}, {\it{phil\/}}, {\it{n\/}})\index{but-triple} \\ 
$\wedge$$\;\;\;\;$\=\+{\bf if }{\rm{add1-mod}}\,({\it{n\/}}, {\it{phil\/}})\index{add1-mod} $<$ {\it{index\/}} \\ 
{\bf then }\=\+{\bf if }{\it{phil\/}} $<$ {\it{index\/}} \\ 
{\bf then }\=\+{\bf if }{\rm{sub1-mod}}\,({\it{n\/}}, {\it{phil\/}})\index{sub1-mod} $<$ {\it{index\/}} \\ 
{\bf then }{\rm{proper-triple}}\,({\it{state\/}}, {\it{phil\/}}, {\it{n\/}})\index{proper-triple} \\ 
{\bf else }\=\+{\rm{proper-phil}}\,(\=\+{\it{state\/}}, \\ 
{\it{phil\/}}, \\ 
{\rm{add1-mod}}\,({\it{n\/}}, {\it{phil\/}})\index{add1-mod})\-\index{proper-phil} \\ 
$\wedge$$\;\;\;\;${\rm{proper-phil}}\,(\=\+{\it{state\/}}, \\ 
{\rm{add1-mod}}\,(\=\+{\it{n\/}}, \\ 
{\it{phil\/}})\-\index{add1-mod}, \\ 
{\rm{add1-mod}}\,(\=\+{\it{n\/}}, \\ 
{\rm{add1-mod}}\,(\=\+{\it{n\/}}, \\ 
{\it{phil\/}})\-\index{add1-mod})\-\index{add1-mod})\-\index{proper-phil}\-$\;${\bf  endif}\- \\ 
{\bf elseif }{\rm{sub1-mod}}\,({\it{n\/}}, {\it{phil\/}})\index{sub1-mod} $<$ {\it{index\/}} \\ 
{\bf then }\=\+{\rm{proper-phil}}\,(\=\+{\it{state\/}}, \\ 
{\rm{sub1-mod}}\,({\it{n\/}}, {\it{phil\/}})\index{sub1-mod}, \\ 
{\rm{add1-mod}}\,({\it{n\/}}, {\rm{sub1-mod}}\,({\it{n\/}}, {\it{phil\/}})\index{sub1-mod})\index{add1-mod})\-\index{proper-phil} \\ 
$\wedge$$\;\;\;\;${\rm{proper-phil}}\,(\=\+{\it{state\/}}, \\ 
{\rm{add1-mod}}\,({\it{n\/}}, {\it{phil\/}})\index{add1-mod}, \\ 
{\rm{add1-mod}}\,(\=\+{\it{n\/}}, \\ 
{\rm{add1-mod}}\,({\it{n\/}}, {\it{phil\/}})\index{add1-mod})\-\index{add1-mod})\-\index{proper-phil}\- \\ 
{\bf else }{\rm{proper-phil}}\,(\=\+{\it{state\/}}, \\ 
{\rm{add1-mod}}\,({\it{n\/}}, {\it{phil\/}})\index{add1-mod}, \\ 
{\rm{add1-mod}}\,(\=\+{\it{n\/}}, \\ 
{\rm{add1-mod}}\,({\it{n\/}}, {\it{phil\/}})\index{add1-mod})\-\index{add1-mod})\-\index{proper-phil}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{phil\/}} $<$ {\it{index\/}} \\ 
{\bf then }\=\+{\bf if }{\rm{sub1-mod}}\,({\it{n\/}}, {\it{phil\/}})\index{sub1-mod} $<$ {\it{index\/}} \\ 
{\bf then }\=\+{\rm{proper-phil}}\,({\it{state\/}}, {\it{phil\/}}, {\rm{add1-mod}}\,({\it{n\/}}, {\it{phil\/}})\index{add1-mod})\index{proper-phil} \\ 
$\wedge$$\;\;\;\;${\rm{proper-phil}}\,(\=\+{\it{state\/}}, \\ 
{\rm{sub1-mod}}\,({\it{n\/}}, {\it{phil\/}})\index{sub1-mod}, \\ 
{\rm{add1-mod}}\,(\=\+{\it{n\/}}, \\ 
{\rm{sub1-mod}}\,({\it{n\/}}, {\it{phil\/}})\index{sub1-mod})\-\index{add1-mod})\-\index{proper-phil}\- \\ 
{\bf else }{\rm{proper-phil}}\,(\=\+{\it{state\/}}, \\ 
{\it{phil\/}}, \\ 
{\rm{add1-mod}}\,({\it{n\/}}, {\it{phil\/}})\index{add1-mod})\-\index{proper-phil}$\;${\bf  endif}\- \\ 
{\bf elseif }{\rm{sub1-mod}}\,({\it{n\/}}, {\it{phil\/}})\index{sub1-mod} $<$ {\it{index\/}} \\ 
{\bf then }{\rm{proper-phil}}\,(\=\+{\it{state\/}}, \\ 
{\rm{sub1-mod}}\,({\it{n\/}}, {\it{phil\/}})\index{sub1-mod}, \\ 
{\rm{add1-mod}}\,({\it{n\/}}, {\rm{sub1-mod}}\,({\it{n\/}}, {\it{phil\/}})\index{sub1-mod})\index{add1-mod})\-\index{proper-phil} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-)\-)\-\-
\end{tabbing}

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


\noindent{\sc Event}:   Disable but-triple-and-triple-all.

\addvspace{18pt}

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

\addvspace{18pt}

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

\addvspace{18pt}

\noindent{\sc Event}:   Disable proper-phils.

\addvspace{18pt}


\begin{tabbing}{\sc Theorem}:  proper-phils-unless-sufficient \\ \index{proper-phils-unless-sufficient}
\=\+({\tt{1}} $<$ {\it{n\/}}) \\ 
$\rightarrow$$\;\;\;\;${\rm{unless-sufficient}}\,(\=\+{\it{statement\/}}, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg}, \\ 
{\it{old\/}}, \\ 
{\it{new\/}}, \\ 
{\tt{`}}{\tt{(}}{\tt{proper-phils}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}, \\ 
{\tt{'}}{\tt{(}}{\tt{false}}{\tt{)}})\-\index{unless-sufficient}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-lefts-unchanged \\ \index{all-lefts-unchanged}
({\rm{all-lefts}}\,({\it{old\/}}, {\it{n\/}})\index{all-lefts} $\wedge$ {\rm{changed}}\,({\it{old\/}}, {\it{new\/}}, {\bf{nil}})\index{changed}) $\rightarrow$ {\rm{all-lefts}}\,({\it{new\/}}, {\it{n\/}})\index{all-lefts}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-lefts-unless-sufficient \\ \index{all-lefts-unless-sufficient}
\=\+({\tt{1}} $<$ {\it{n\/}}) \\ 
$\rightarrow$$\;\;\;\;${\rm{unless-sufficient}}\,(\=\+{\it{statement\/}}, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg}, \\ 
{\it{old\/}}, \\ 
{\it{new\/}}, \\ 
{\tt{`}}{\tt{(}}{\tt{all-lefts}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}, \\ 
{\tt{'}}{\tt{(}}{\tt{false}}{\tt{)}})\-\index{unless-sufficient}\-
\end{tabbing}


\noindent{\sc Event}:   Disable all-lefts-implies.

\addvspace{18pt}

\noindent{\sc Event}:   Disable all-lefts-unchanged.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  all-rights-rec-unchanged \\ \index{all-rights-rec-unchanged}
\=\+({\rm{all-rights-rec}}\,({\it{old\/}}, {\it{index\/}}, {\it{n\/}})\index{all-rights-rec} $\wedge$ {\rm{changed}}\,({\it{old\/}}, {\it{new\/}}, {\bf{nil}})\index{changed} $\wedge$ ({\it{n\/}} $\not<$ {\it{index\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{all-rights-rec}}\,({\it{new\/}}, {\it{index\/}}, {\it{n\/}})\index{all-rights-rec}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-rights-unless-sufficient \\ \index{all-rights-unless-sufficient}
\=\+({\tt{1}} $<$ {\it{n\/}}) \\ 
$\rightarrow$$\;\;\;\;${\rm{unless-sufficient}}\,(\=\+{\it{statement\/}}, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg}, \\ 
{\it{old\/}}, \\ 
{\it{new\/}}, \\ 
{\tt{`}}{\tt{(}}{\tt{all-rights}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}, \\ 
{\tt{'}}{\tt{(}}{\tt{false}}{\tt{)}})\-\index{unless-sufficient}\-
\end{tabbing}


\noindent{\sc Event}:   Disable all-rights-implies.

\addvspace{18pt}

\noindent{\sc Event}:   Disable all-rights-rec-unchanged.

\addvspace{18pt}

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

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

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


\begin{tabbing}{\sc Theorem}:  all-lefts-inv \\ \index{all-lefts-inv}
({\tt{1}} $<$ {\it{n\/}}) $\rightarrow$ {\rm{unless}}\,({\tt{`}}{\tt{(}}{\tt{all-lefts}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}, {\tt{'}}{\tt{(}}{\tt{false}}{\tt{)}}, {\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\index{unless}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-rights-inv \\ \index{all-rights-inv}
\=\+({\tt{1}} $<$ {\it{n\/}}) \\ 
$\rightarrow$$\;\;\;\;${\rm{unless}}\,({\tt{`}}{\tt{(}}{\tt{all-rights}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}, {\tt{'}}{\tt{(}}{\tt{false}}{\tt{)}}, {\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\index{unless}\-
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  proper-phil-invariant \\ \index{proper-phil-invariant}
\=\+(\=\+({\it{index\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{initial-condition}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{proper-phils}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}} \\ 
{\tt{(}}{\tt{proper-forks}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{initial-condition})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{invariant}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{proper-phil}}{\tt{ }}{\tt{state}} \\ 
{\tt{'}}{\tt{,}}{\tt{index}} \\ 
{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1-mod}}{\tt{ }}{\tt{n}}{\tt{ }}{\tt{index}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{invariant}\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{proper-fork} \\  
\=\+{\rm{proper-fork}}\,({\it{state\/}}, {\it{index\/}}, {\it{left\/}})\index{proper-fork} \\ 
$=$$\;\;\;\;$(\=\+{\rm{free}}\,({\it{state\/}}, {\it{index\/}})\index{free} \\ 
$\vee$$\;\;\;\;$({\rm{fork}}\,({\it{state\/}}, {\it{index\/}})\index{fork} $=$ {\it{index\/}}) \\ 
$\vee$$\;\;\;\;$({\rm{fork}}\,({\it{state\/}}, {\it{index\/}})\index{fork} $=$ {\it{left\/}}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  proper-fork-invariant \\ \index{proper-fork-invariant}
\=\+(\=\+({\it{index\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{initial-condition}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{proper-phils}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}} \\ 
{\tt{(}}{\tt{proper-forks}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{initial-condition})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{invariant}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{proper-fork}}{\tt{ }}{\tt{state}} \\ 
{\tt{'}}{\tt{,}}{\tt{index}} \\ 
{\tt{'}}{\tt{,}}{\tt{(}}{\tt{sub1-mod}}{\tt{ }}{\tt{n}}{\tt{ }}{\tt{index}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{invariant}\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  hungry-unless-owns-left \\ \index{hungry-unless-owns-left}
\=\+(({\tt{1}} $<$ {\it{n\/}}) $\wedge$ ({\it{index\/}} $<$ {\it{n\/}}) $\wedge$ ({\it{index\/}} $\in\;${\bf{N}}${}$)) \\ 
$\rightarrow$$\;\;\;\;${\rm{unless}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{hungry}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}, \\ 
{\tt{`}}{\tt{(}}{\tt{owns-left}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{unless}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  hungry-unless-owns-right \\ \index{hungry-unless-owns-right}
\=\+(({\tt{1}} $<$ {\it{n\/}}) $\wedge$ ({\it{index\/}} $<$ {\it{n\/}}) $\wedge$ ({\it{index\/}} $\in\;${\bf{N}}${}$)) \\ 
$\rightarrow$$\;\;\;\;${\rm{unless}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{hungry}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}, \\ 
{\tt{`}}{\tt{(}}{\tt{owns-right}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{unless}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  hungry-left-free-e-ensures-owns-left \\ \index{hungry-left-free-e-ensures-owns!-left}
\=\+(({\tt{1}} $<$ {\it{n\/}}) $\wedge$ ({\it{index\/}} $<$ {\it{n\/}}) $\wedge$ ({\it{index\/}} $\in\;${\bf{N}}${}$)) \\ 
$\rightarrow$$\;\;\;\;${\rm{e-ensures}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{hungry}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}, \\ 
{\tt{`}}{\tt{(}}{\tt{owns-left}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}, \\ 
{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{hungry}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}{\tt{free}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{e-ensures}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  hungry-right-free-e-ensures-owns-right \\ \index{hungry-right-free-e-ensures-own!s-right}
\=\+(({\tt{1}} $<$ {\it{n\/}}) $\wedge$ ({\it{index\/}} $<$ {\it{n\/}}) $\wedge$ ({\it{index\/}} $\in\;${\bf{N}}${}$)) \\ 
$\rightarrow$$\;\;\;\;${\rm{e-ensures}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{hungry}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}, \\ 
{\tt{`}}{\tt{(}}{\tt{owns-right}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}, \\ 
{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{hungry}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}{\tt{free}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1-mod}}{\tt{ }}{\tt{n}}{\tt{ }}{\tt{index}}{\tt{)}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{e-ensures}\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  hungry-unless-eating \\ \index{hungry-unless-eating}
\=\+(({\tt{1}} $<$ {\it{n\/}}) $\wedge$ ({\it{index\/}} $<$ {\it{n\/}}) $\wedge$ ({\it{index\/}} $\in\;${\bf{N}}${}$)) \\ 
$\rightarrow$$\;\;\;\;${\rm{unless}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{hungry}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}, \\ 
{\tt{`}}{\tt{(}}{\tt{eating}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{unless}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  owns-left-unless-sufficient \\ \index{owns-left-unless-sufficient}
\=\+(({\tt{1}} $<$ {\it{n\/}}) $\wedge$ ({\it{index\/}} $<$ {\it{n\/}}) $\wedge$ ({\it{index\/}} $\in\;${\bf{N}}${}$)) \\ 
$\rightarrow$$\;\;\;\;${\rm{unless-sufficient}}\,(\=\+{\it{statement\/}}, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg}, \\ 
{\it{old\/}}, \\ 
{\it{new\/}}, \\ 
{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{proper-phils}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}} \\ 
{\tt{(}}{\tt{owns-left}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}{\tt{)}}\-, \\ 
{\tt{`}}{\tt{(}}{\tt{eating}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}})\-\index{unless-sufficient}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  owns-right-unless-sufficient \\ \index{owns-right-unless-sufficient}
\=\+(({\tt{1}} $<$ {\it{n\/}}) $\wedge$ ({\it{index\/}} $<$ {\it{n\/}}) $\wedge$ ({\it{index\/}} $\in\;${\bf{N}}${}$)) \\ 
$\rightarrow$$\;\;\;\;${\rm{unless-sufficient}}\,(\=\+{\it{statement\/}}, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg}, \\ 
{\it{old\/}}, \\ 
{\it{new\/}}, \\ 
{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{proper-phils}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}} \\ 
{\tt{(}}{\tt{owns-right}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}{\tt{)}}\-, \\ 
{\tt{`}}{\tt{(}}{\tt{eating}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}})\-\index{unless-sufficient}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  owns-right-unless-eating \\ \index{owns-right-unless-eating}
\=\+(({\tt{1}} $<$ {\it{n\/}}) $\wedge$ ({\it{index\/}} $<$ {\it{n\/}}) $\wedge$ ({\it{index\/}} $\in\;${\bf{N}}${}$)) \\ 
$\rightarrow$$\;\;\;\;${\rm{unless}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{proper-phils}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}} \\ 
{\tt{(}}{\tt{owns-right}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}{\tt{)}}\-, \\ 
{\tt{`}}{\tt{(}}{\tt{eating}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{unless}\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  owns-left-unless-eating \\ \index{owns-left-unless-eating}
\=\+(({\tt{1}} $<$ {\it{n\/}}) $\wedge$ ({\it{index\/}} $<$ {\it{n\/}}) $\wedge$ ({\it{index\/}} $\in\;${\bf{N}}${}$)) \\ 
$\rightarrow$$\;\;\;\;${\rm{unless}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{proper-phils}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}} \\ 
{\tt{(}}{\tt{owns-left}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}{\tt{)}}\-, \\ 
{\tt{`}}{\tt{(}}{\tt{eating}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{unless}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  owns-both-unless-eating \\ \index{owns-both-unless-eating}
\=\+(({\tt{1}} $<$ {\it{n\/}}) $\wedge$ ({\it{index\/}} $<$ {\it{n\/}}) $\wedge$ ({\it{index\/}} $\in\;${\bf{N}}${}$)) \\ 
$\rightarrow$$\;\;\;\;${\rm{unless}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{owns-left}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{owns-right}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}} \\ 
{\tt{(}}{\tt{proper-phils}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}{\tt{)}}\-{\tt{)}}\-, \\ 
{\tt{`}}{\tt{(}}{\tt{eating}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{unless}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  owns-both-e-ensures-eating \\ \index{owns-both-e-ensures-eating}
\=\+(({\tt{1}} $<$ {\it{n\/}}) $\wedge$ ({\it{index\/}} $<$ {\it{n\/}}) $\wedge$ ({\it{index\/}} $\in\;${\bf{N}}${}$)) \\ 
$\rightarrow$$\;\;\;\;${\rm{e-ensures}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{owns-left}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{owns-right}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}} \\ 
{\tt{(}}{\tt{proper-phils}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}{\tt{)}}\-{\tt{)}}\-, \\ 
{\tt{`}}{\tt{(}}{\tt{eating}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}, \\ 
{\tt{`}}{\tt{(}}{\tt{true}}{\tt{)}}, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{e-ensures}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  owns-both-leads-to-eating \\ \index{owns-both-leads-to-eating}
\=\+(\=\+({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{initial-condition}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{proper-phils}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}} \\ 
{\tt{(}}{\tt{proper-forks}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{initial-condition})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{owns-left}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}{\tt{owns-right}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}{\tt{)}}\-, \\ 
{\tt{`}}{\tt{(}}{\tt{eating}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{leads-to}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  eating-unless-free \\ \index{eating-unless-free}
\=\+(({\tt{1}} $<$ {\it{n\/}}) $\wedge$ ({\it{index\/}} $<$ {\it{n\/}}) $\wedge$ ({\it{index\/}} $\in\;${\bf{N}}${}$)) \\ 
$\rightarrow$$\;\;\;\;${\rm{unless}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{eating}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}, \\ 
{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{free}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}{\tt{free}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1-mod}}{\tt{ }}{\tt{n}}{\tt{ }}{\tt{index}}{\tt{)}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{unless}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  eating-e-ensures-free \\ \index{eating-e-ensures-free}
\=\+(({\tt{1}} $<$ {\it{n\/}}) $\wedge$ ({\it{index\/}} $<$ {\it{n\/}}) $\wedge$ ({\it{index\/}} $\in\;${\bf{N}}${}$)) \\ 
$\rightarrow$$\;\;\;\;${\rm{e-ensures}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{eating}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}, \\ 
{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{free}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}{\tt{free}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1-mod}}{\tt{ }}{\tt{n}}{\tt{ }}{\tt{index}}{\tt{)}}{\tt{)}}{\tt{)}}\-, \\ 
{\tt{'}}{\tt{(}}{\tt{true}}{\tt{)}}, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{e-ensures}\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  eating-leads-to-free \\ \index{eating-leads-to-free}
\=\+(\=\+({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{initial-condition}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{proper-phils}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}} \\ 
{\tt{(}}{\tt{proper-forks}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{initial-condition})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{eating}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}, \\ 
{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{free}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}{\tt{free}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1-mod}}{\tt{ }}{\tt{n}}{\tt{ }}{\tt{index}}{\tt{)}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{leads-to}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  leads-to-expanded-right-implies \\ \index{leads-to-expanded-right-implies}
\=\+(\=\+({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{initial-condition}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{proper-phils}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}} \\ 
{\tt{(}}{\tt{proper-forks}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{initial-condition} \\ 
$\wedge$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{true}}{\tt{)}}, \\ 
{\tt{`}}{\tt{(}}\=\+{\tt{or}} \\ 
{\tt{(}}{\tt{owns-right}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{sub1-mod}}{\tt{ }}{\tt{n}}{\tt{ }}{\tt{index}}{\tt{)}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{or}} \\ 
{\tt{(}}{\tt{free}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{or}} \\ 
{\tt{(}}{\tt{eating}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}{\tt{thinking}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}{\tt{)}}\-{\tt{)}}\-{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{leads-to})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{true}}{\tt{)}}, \\ 
{\tt{`}}{\tt{(}}\=\+{\tt{or}} \\ 
{\tt{(}}{\tt{free}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}{\tt{owns-right}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{sub1-mod}}{\tt{ }}{\tt{n}}{\tt{ }}{\tt{index}}{\tt{)}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{leads-to}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  leads-to-expanded-left-implies \\ \index{leads-to-expanded-left-implies}
\=\+(\=\+({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{initial-condition}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{proper-phils}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}} \\ 
{\tt{(}}{\tt{proper-forks}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{initial-condition} \\ 
$\wedge$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{true}}{\tt{)}}, \\ 
{\tt{`}}{\tt{(}}\=\+{\tt{or}} \\ 
{\tt{(}}{\tt{owns-left}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1-mod}}{\tt{ }}{\tt{n}}{\tt{ }}{\tt{index}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{or}} \\ 
{\tt{(}}{\tt{free}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1-mod}}{\tt{ }}{\tt{n}}{\tt{ }}{\tt{index}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{or}} \\ 
{\tt{(}}{\tt{eating}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}{\tt{thinking}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}{\tt{)}}\-{\tt{)}}\-{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{leads-to})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{true}}{\tt{)}}, \\ 
{\tt{`}}{\tt{(}}\=\+{\tt{or}} \\ 
{\tt{(}}{\tt{free}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1-mod}}{\tt{ }}{\tt{n}}{\tt{ }}{\tt{index}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}{\tt{owns-left}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1-mod}}{\tt{ }}{\tt{n}}{\tt{ }}{\tt{index}}{\tt{)}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{leads-to}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  true-leads-to-left-free-implies \\ \index{true-leads-to-left-free-implies}
\=\+(\=\+({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{strongly-fair}}\,({\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\index{strongly-fair} \\ 
$\wedge$$\;\;\;\;${\rm{initial-condition}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{proper-phils}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}} \\ 
{\tt{(}}{\tt{proper-forks}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{initial-condition} \\ 
$\wedge$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{true}}{\tt{)}}, \\ 
{\tt{`}}{\tt{(}}\=\+{\tt{or}} \\ 
{\tt{(}}{\tt{free}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}{\tt{owns-left}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{leads-to})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{hungry}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}, \\ 
{\tt{`}}{\tt{(}}{\tt{owns-left}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{leads-to}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  true-leads-to-right-free-implies \\ \index{true-leads-to-right-free-implie!s}
\=\+(\=\+({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{strongly-fair}}\,({\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\index{strongly-fair} \\ 
$\wedge$$\;\;\;\;${\rm{initial-condition}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{proper-phils}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}} \\ 
{\tt{(}}{\tt{proper-forks}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{initial-condition} \\ 
$\wedge$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{true}}{\tt{)}}, \\ 
{\tt{`}}{\tt{(}}\=\+{\tt{or}} \\ 
{\tt{(}}{\tt{free}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1-mod}}{\tt{ }}{\tt{n}}{\tt{ }}{\tt{index}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}{\tt{owns-right}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{leads-to})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{hungry}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}, \\ 
{\tt{`}}{\tt{(}}{\tt{owns-right}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{leads-to}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  hungry-leads-to-owns-right-implies \\ \index{hungry-leads-to-owns-right-implie!s}
\=\+(\=\+({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{strongly-fair}}\,({\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\index{strongly-fair} \\ 
$\wedge$$\;\;\;\;${\rm{initial-condition}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{proper-phils}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}} \\ 
{\tt{(}}{\tt{proper-forks}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{initial-condition} \\ 
$\wedge$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{hungry}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}, \\ 
{\tt{`}}{\tt{(}}{\tt{owns-right}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{leads-to})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{hungry}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}{\tt{owns-left}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}{\tt{)}}\-, \\ 
{\tt{`}}{\tt{(}}{\tt{eating}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{leads-to}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  hungry-leads-to-owns-left-implies \\ \index{hungry-leads-to-owns-left-implie!s}
\=\+(\=\+({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{strongly-fair}}\,({\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\index{strongly-fair} \\ 
$\wedge$$\;\;\;\;${\rm{initial-condition}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{proper-phils}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}} \\ 
{\tt{(}}{\tt{proper-forks}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{initial-condition} \\ 
$\wedge$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{hungry}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}, \\ 
{\tt{`}}{\tt{(}}{\tt{owns-left}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{leads-to})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{hungry}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}{\tt{owns-right}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}{\tt{)}}\-, \\ 
{\tt{`}}{\tt{(}}{\tt{eating}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{leads-to}\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{left-chain} \\  
\=\+{\rm{left-chain}}\,({\it{i\/}}, {\it{j\/}}, {\it{n\/}}, {\it{state\/}})\index{left-chain} \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\it{i\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{j\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{i\/}} $<$ {\it{n\/}}) $\wedge$ ({\it{j\/}} $<$ {\it{n\/}}) \\ 
{\bf then }\=\+{\bf if }{\it{i\/}} $=$ {\it{j\/}}$\;\;${\bf then }{\rm{hungry}}\,({\it{state\/}}, {\it{i\/}})\index{hungry} $\wedge$ {\rm{owns-left}}\,({\it{state\/}}, {\it{i\/}})\index{owns-left} \\ 
{\bf else }\=\+{\rm{hungry}}\,({\it{state\/}}, {\it{i\/}})\index{hungry} \\ 
$\wedge$$\;\;\;\;${\rm{owns-left}}\,({\it{state\/}}, {\it{i\/}})\index{owns-left} \\ 
$\wedge$$\;\;\;\;${\rm{left-chain}}\,({\rm{sub1-mod}}\,({\it{n\/}}, {\it{i\/}})\index{sub1-mod}, {\it{j\/}}, {\it{n\/}}, {\it{state\/}})\index{left-chain}\-$\;${\bf  endif}\- \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{right-chain} \\  
\=\+{\rm{right-chain}}\,({\it{i\/}}, {\it{j\/}}, {\it{n\/}}, {\it{state\/}})\index{right-chain} \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\it{i\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{j\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{i\/}} $<$ {\it{n\/}}) $\wedge$ ({\it{j\/}} $<$ {\it{n\/}}) \\ 
{\bf then }\=\+{\bf if }{\it{i\/}} $=$ {\it{j\/}}$\;\;${\bf then }{\rm{hungry}}\,({\it{state\/}}, {\it{i\/}})\index{hungry} $\wedge$ {\rm{owns-right}}\,({\it{state\/}}, {\it{i\/}}, {\it{n\/}})\index{owns-right} \\ 
{\bf else }\=\+{\rm{hungry}}\,({\it{state\/}}, {\it{i\/}})\index{hungry} \\ 
$\wedge$$\;\;\;\;${\rm{owns-right}}\,({\it{state\/}}, {\it{i\/}}, {\it{n\/}})\index{owns-right} \\ 
$\wedge$$\;\;\;\;${\rm{right-chain}}\,({\rm{add1-mod}}\,({\it{n\/}}, {\it{i\/}})\index{add1-mod}, {\it{j\/}}, {\it{n\/}}, {\it{state\/}})\index{right-chain}\-$\;${\bf  endif}\- \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  break-left-chain \\ \index{break-left-chain}
\=\+(({\it{i\/}} $<$ {\it{n\/}}) $\wedge$ ({\it{j\/}} $<$ {\it{n\/}}) $\wedge$ ({\it{i\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{j\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{i\/}} $<$ {\it{j\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{left-chain}}\,({\it{i\/}}, {\it{j\/}}, {\it{n\/}}, {\it{state\/}})\index{left-chain} \\ 
$=$$\;\;\;\;$({\rm{left-chain}}\,({\it{i\/}}, {\tt{0}}, {\it{n\/}}, {\it{state\/}})\index{left-chain} $\wedge$ {\rm{left-chain}}\,({\it{n\/}} $-\;1$, {\it{j\/}}, {\it{n\/}}, {\it{state\/}})\index{left-chain}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{lcc} \\  
\=\+{\rm{lcc}}\,({\it{i\/}}, {\it{j\/}}, {\it{k\/}})\index{lcc} \\ 
$=$$\;\;\;\;$\=\+{\bf if }\=\+({\it{i\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{k\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\it{k\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $<$ {\it{k\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not=$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{k\/}} $\not\simeq {\tt{0}}$)\- \\ 
{\bf then }\=\+{\bf if }($1\;+$ {\it{i\/}}) $=$ {\it{k\/}}$\;\;${\bf then }{\rm{lcc}}\,({\it{i\/}} $-\;1$, {\it{j\/}}, {\it{k\/}} $-\;1$)\index{lcc} \\ 
{\bf elseif }($1\;+$ {\it{j\/}}) $=$ {\it{k\/}}$\;\;${\bf then }{\rm{lcc}}\,({\it{i\/}}, {\it{j\/}} $-\;1$, {\it{k\/}} $-\;1$)\index{lcc} \\ 
{\bf else }{\rm{lcc}}\,({\it{i\/}}, {\it{j\/}}, {\it{k\/}} $-\;1$)\index{lcc}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  left-chain-combine \\ \index{left-chain-combine}
\=\+(({\it{i\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{j\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{k\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{k\/}} $<$ {\it{n\/}}) $\wedge$ ({\it{i\/}} $<$ {\it{k\/}}) $\wedge$ ({\it{j\/}} $<$ {\it{k\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{left-chain}}\,({\it{i\/}}, {\tt{0}}, {\it{n\/}}, {\it{state\/}})\index{left-chain} $\wedge$ {\rm{left-chain}}\,({\it{k\/}}, $1\;+$ {\it{i\/}}, {\it{n\/}}, {\it{state\/}})\index{left-chain}) \\ 
$=$$\;\;\;\;$({\rm{left-chain}}\,({\it{j\/}}, {\tt{0}}, {\it{n\/}}, {\it{state\/}})\index{left-chain} $\wedge$ {\rm{left-chain}}\,({\it{k\/}}, $1\;+$ {\it{j\/}}, {\it{n\/}}, {\it{state\/}})\index{left-chain}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-1-1 \\ \index{lessp-1-1}
({\it{n\/}} $<$ {\tt{1}}) $=$ ({\it{n\/}} $\simeq {\tt{0}}$)
\end{tabbing}


\noindent{\sc Event}:   Disable lessp-1-1.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  left-chain-canonicalize \\ \index{left-chain-canonicalize}
\=\+(({\it{i\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{i\/}} $<$ {\it{n\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{left-chain}}\,({\it{i\/}}, {\rm{add1-mod}}\,({\it{n\/}}, {\it{i\/}})\index{add1-mod}, {\it{n\/}}, {\it{state\/}})\index{left-chain} $=$ {\rm{left-chain}}\,({\it{n\/}} $-\;1$, {\tt{0}}, {\it{n\/}}, {\it{state\/}})\index{left-chain})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  left-chain-canonicalize-all-lefts \\ \index{left-chain-canonicalize-all-left!s}
\=\+(({\it{index\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{n\/}} $\not<$ {\it{index\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{left-chain}}\,({\it{index\/}} $-\;1$, {\tt{0}}, {\it{n\/}}, {\it{state\/}})\index{left-chain} $=$ {\rm{all-lefts}}\,({\it{state\/}}, {\it{index\/}})\index{all-lefts})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  left-chain-complete \\ \index{left-chain-complete}
\=\+(({\it{i\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{i\/}} $<$ {\it{n\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{left-chain}}\,({\it{i\/}}, {\rm{add1-mod}}\,({\it{n\/}}, {\it{i\/}})\index{add1-mod}, {\it{n\/}}, {\it{state\/}})\index{left-chain} $=$ {\rm{all-lefts}}\,({\it{state\/}}, {\it{n\/}})\index{all-lefts})\-
\end{tabbing}


\noindent{\sc Event}:   Disable left-chain-canonicalize-all-lefts.

\addvspace{18pt}

\noindent{\sc Event}:   Disable left-chain-canonicalize.

\addvspace{18pt}

\noindent{\sc Event}:   Disable left-chain-combine.

\addvspace{18pt}

\noindent{\sc Event}:   Disable break-left-chain.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  break-right-chain \\ \index{break-right-chain}
\=\+(({\it{i\/}} $<$ {\it{n\/}}) $\wedge$ ({\it{j\/}} $<$ {\it{n\/}}) $\wedge$ ({\it{i\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{j\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{j\/}} $<$ {\it{i\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{right-chain}}\,({\it{i\/}}, {\it{j\/}}, {\it{n\/}}, {\it{state\/}})\index{right-chain} \\ 
$=$$\;\;\;\;$({\rm{right-chain}}\,({\it{i\/}}, {\it{n\/}} $-\;1$, {\it{n\/}}, {\it{state\/}})\index{right-chain} $\wedge$ {\rm{right-chain}}\,({\tt{0}}, {\it{j\/}}, {\it{n\/}}, {\it{state\/}})\index{right-chain}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{rcc} \\  
\=\+{\rm{rcc}}\,({\it{i\/}}, {\it{j\/}}, {\it{k\/}}, {\it{n\/}})\index{rcc} \\ 
$=$$\;\;\;\;$\=\+{\bf if }\=\+({\it{i\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{k\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{k\/}} $<$ {\it{i\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{k\/}} $<$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not=$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{k\/}} $\not=$ {\it{n\/}})\- \\ 
{\bf then }\=\+{\bf if }{\it{k\/}} $=$ ({\it{i\/}} $-\;1$)$\;\;${\bf then }{\rm{rcc}}\,($1\;+$ {\it{i\/}}, {\it{j\/}}, $1\;+$ {\it{k\/}}, {\it{n\/}})\index{rcc} \\ 
{\bf elseif }{\it{k\/}} $=$ ({\it{j\/}} $-\;1$)$\;\;${\bf then }{\rm{rcc}}\,({\it{i\/}}, $1\;+$ {\it{j\/}}, $1\;+$ {\it{k\/}}, {\it{n\/}})\index{rcc} \\ 
{\bf else }{\rm{rcc}}\,({\it{i\/}}, {\it{j\/}}, $1\;+$ {\it{k\/}}, {\it{n\/}})\index{rcc}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  right-chain-combine \\ \index{right-chain-combine}
\=\+(({\it{k\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{i\/}} $<$ {\it{n\/}}) $\wedge$ ({\it{j\/}} $<$ {\it{n\/}}) $\wedge$ ({\it{k\/}} $<$ {\it{i\/}}) $\wedge$ ({\it{k\/}} $<$ {\it{j\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{right-chain}}\,({\it{i\/}}, {\it{n\/}} $-\;1$, {\it{n\/}}, {\it{state\/}})\index{right-chain} $\wedge$ {\rm{right-chain}}\,({\it{k\/}}, {\it{i\/}} $-\;1$, {\it{n\/}}, {\it{state\/}})\index{right-chain}) \\ 
$=$$\;\;\;\;$(\=\+{\rm{right-chain}}\,({\it{j\/}}, {\it{n\/}} $-\;1$, {\it{n\/}}, {\it{state\/}})\index{right-chain} \\ 
$\wedge$$\;\;\;\;${\rm{right-chain}}\,({\it{k\/}}, {\it{j\/}} $-\;1$, {\it{n\/}}, {\it{state\/}})\index{right-chain})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  right-chain-canonicalize \\ \index{right-chain-canonicalize}
\=\+(({\it{i\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{i\/}} $<$ {\it{n\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{right-chain}}\,({\it{i\/}}, {\rm{sub1-mod}}\,({\it{n\/}}, {\it{i\/}})\index{sub1-mod}, {\it{n\/}}, {\it{state\/}})\index{right-chain} \\ 
$=$$\;\;\;\;${\rm{right-chain}}\,({\tt{0}}, {\it{n\/}} $-\;1$, {\it{n\/}}, {\it{state\/}})\index{right-chain})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  right-chain-extend-right \\ \index{right-chain-extend-right}
\=\+(({\it{i\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{j\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{i\/}} $<$ {\it{n\/}}) $\wedge$ ({\it{j\/}} $<$ {\it{n\/}}) $\wedge$ ({\it{i\/}} $\not=$ {\it{j\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{right-chain}}\,({\it{i\/}}, {\it{j\/}}, {\it{n\/}}, {\it{state\/}})\index{right-chain} \\ 
$=$$\;\;\;\;$(\=\+{\rm{right-chain}}\,({\it{i\/}}, {\rm{sub1-mod}}\,({\it{n\/}}, {\it{j\/}})\index{sub1-mod}, {\it{n\/}}, {\it{state\/}})\index{right-chain} \\ 
$\wedge$$\;\;\;\;${\rm{hungry}}\,({\it{state\/}}, {\it{j\/}})\index{hungry} \\ 
$\wedge$$\;\;\;\;${\rm{owns-right}}\,({\it{state\/}}, {\it{j\/}}, {\it{n\/}})\index{owns-right})\-)\-\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  right-chain-canonicalize-all-rights \\ \index{right-chain-canonicalize-all-ri!ghts}
\=\+(({\it{index\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{n\/}} $\not<$ {\it{index\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{right-chain}}\,({\tt{0}}, {\it{index\/}} $-\;1$, {\it{n\/}}, {\it{state\/}})\index{right-chain} $=$ {\rm{all-rights-rec}}\,({\it{state\/}}, {\it{index\/}}, {\it{n\/}})\index{all-rights-rec})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  right-chain-complete \\ \index{right-chain-complete}
\=\+(({\it{i\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{i\/}} $<$ {\it{n\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{right-chain}}\,({\it{i\/}}, {\rm{sub1-mod}}\,({\it{n\/}}, {\it{i\/}})\index{sub1-mod}, {\it{n\/}}, {\it{state\/}})\index{right-chain} $=$ {\rm{all-rights}}\,({\it{state\/}}, {\it{n\/}})\index{all-rights})\-
\end{tabbing}


\noindent{\sc Event}:   Disable right-chain-canonicalize-all-rights.

\addvspace{18pt}

\noindent{\sc Event}:   Disable right-chain-extend-right.

\addvspace{18pt}

\noindent{\sc Event}:   Disable right-chain-canonicalize.

\addvspace{18pt}

\noindent{\sc Event}:   Disable right-chain-combine.

\addvspace{18pt}

\noindent{\sc Event}:   Disable break-right-chain.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  not-eventually-left-implies \\ \index{not-eventually-left-implies}
\=\+(\=\+({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{initial-condition}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{proper-phils}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}} \\ 
{\tt{(}}{\tt{proper-forks}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{initial-condition} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{eventually-stable}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{hungry}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}{\tt{owns-left}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{eventually-stable}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{true}}{\tt{)}}, \\ 
{\tt{`}}{\tt{(}}\=\+{\tt{or}} \\ 
{\tt{(}}{\tt{owns-right}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{sub1-mod}}{\tt{ }}{\tt{n}}{\tt{ }}{\tt{index}}{\tt{)}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{or}} \\ 
{\tt{(}}{\tt{free}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{or}} \\ 
{\tt{(}}{\tt{eating}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}{\tt{thinking}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}{\tt{)}}\-{\tt{)}}\-{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{leads-to}\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  not-eventually-right-implies \\ \index{not-eventually-right-implies}
\=\+(\=\+({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{initial-condition}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{proper-phils}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}} \\ 
{\tt{(}}{\tt{proper-forks}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{initial-condition} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{eventually-stable}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{hungry}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}{\tt{owns-right}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{eventually-stable}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{true}}{\tt{)}}, \\ 
{\tt{`}}{\tt{(}}\=\+{\tt{or}} \\ 
{\tt{(}}{\tt{owns-left}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1-mod}}{\tt{ }}{\tt{n}}{\tt{ }}{\tt{index}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{or}} \\ 
{\tt{(}}{\tt{free}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{(}}{\tt{add1-mod}}{\tt{ }}{\tt{n}}{\tt{ }}{\tt{index}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{or}} \\ 
{\tt{(}}{\tt{eating}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}} \\ 
{\tt{(}}{\tt{thinking}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}{\tt{)}}\-{\tt{)}}\-{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{leads-to}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  right-chain-induction \\ \index{right-chain-induction}
\=\+(\=\+{\rm{strongly-fair}}\,({\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\index{strongly-fair} \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{initial-condition}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{proper-phils}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}} \\ 
{\tt{(}}{\tt{proper-forks}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{initial-condition} \\ 
$\wedge$$\;\;\;\;${\rm{eventually-stable}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{hungry}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{j}}{\tt{)}} \\ 
{\tt{(}}{\tt{owns-right}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{j}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{eventually-stable})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{eventually-stable}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{right-chain}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{i}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{j}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{ }}{\tt{state}}{\tt{)}}, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{eventually-stable}\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  eventually-stable-right-implies-all-rights \\ \index{eventually-stable-right-implies!-all-rights}
\=\+(\=\+({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{strongly-fair}}\,({\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\index{strongly-fair} \\ 
$\wedge$$\;\;\;\;${\rm{initial-condition}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{proper-phils}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}} \\ 
{\tt{(}}{\tt{proper-forks}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{initial-condition} \\ 
$\wedge$$\;\;\;\;${\rm{eventually-stable}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{hungry}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{j}}{\tt{)}} \\ 
{\tt{(}}{\tt{owns-right}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{j}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{eventually-stable})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{eventually-stable}}\,({\tt{`}}{\tt{(}}{\tt{all-rights}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}, {\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\index{eventually-stable}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  never-all-rights \\ \index{never-all-rights}
\=\+({\rm{deadlock-free}}\,({\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\index{deadlock-free} $\wedge$ ({\tt{1}} $<$ {\it{n\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{invariant}}\,({\tt{`}}{\tt{(}}{\tt{not}}{\tt{ }}{\tt{(}}{\tt{all-rights}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}{\tt{)}}, {\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\index{invariant}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  not-eventually-owns-right \\ \index{not-eventually-owns-right}
\=\+(\=\+({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{strongly-fair}}\,({\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\index{strongly-fair} \\ 
$\wedge$$\;\;\;\;${\rm{deadlock-free}}\,({\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\index{deadlock-free} \\ 
$\wedge$$\;\;\;\;${\rm{initial-condition}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{proper-phils}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}} \\ 
{\tt{(}}{\tt{proper-forks}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{initial-condition})\- \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{eventually-stable}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{hungry}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{j}}{\tt{)}} \\ 
{\tt{(}}{\tt{owns-right}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{j}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{eventually-stable})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  hungry-leads-to-owns-left \\ \index{hungry-leads-to-owns-left}
\=\+(\=\+({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{initial-condition}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{proper-phils}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}} \\ 
{\tt{(}}{\tt{proper-forks}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{initial-condition} \\ 
$\wedge$$\;\;\;\;${\rm{strongly-fair}}\,({\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\index{strongly-fair} \\ 
$\wedge$$\;\;\;\;${\rm{deadlock-free}}\,({\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\index{deadlock-free})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{hungry}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}, \\ 
{\tt{`}}{\tt{(}}{\tt{owns-left}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{leads-to}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  left-chain-induction \\ \index{left-chain-induction}
\=\+(\=\+{\rm{strongly-fair}}\,({\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\index{strongly-fair} \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{initial-condition}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{proper-phils}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}} \\ 
{\tt{(}}{\tt{proper-forks}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{initial-condition} \\ 
$\wedge$$\;\;\;\;${\rm{eventually-stable}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{hungry}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{j}}{\tt{)}} \\ 
{\tt{(}}{\tt{owns-left}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{j}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{eventually-stable})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{eventually-stable}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{left-chain}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{i}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{j}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{ }}{\tt{state}}{\tt{)}}, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{eventually-stable}\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  eventually-stable-left-implies-all-lefts \\ \index{eventually-stable-left-implies-!all-lefts}
\=\+(\=\+({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{strongly-fair}}\,({\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\index{strongly-fair} \\ 
$\wedge$$\;\;\;\;${\rm{initial-condition}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{proper-phils}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}} \\ 
{\tt{(}}{\tt{proper-forks}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{initial-condition} \\ 
$\wedge$$\;\;\;\;${\rm{eventually-stable}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{hungry}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{j}}{\tt{)}} \\ 
{\tt{(}}{\tt{owns-left}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{j}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{eventually-stable})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{eventually-stable}}\,({\tt{`}}{\tt{(}}{\tt{all-lefts}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}, {\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\index{eventually-stable}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  never-all-lefts \\ \index{never-all-lefts}
\=\+({\rm{deadlock-free}}\,({\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\index{deadlock-free} $\wedge$ ({\tt{1}} $<$ {\it{n\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{invariant}}\,({\tt{`}}{\tt{(}}{\tt{not}}{\tt{ }}{\tt{(}}{\tt{all-lefts}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}{\tt{)}}, {\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\index{invariant}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  not-eventually-owns-left \\ \index{not-eventually-owns-left}
\=\+(\=\+({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{strongly-fair}}\,({\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\index{strongly-fair} \\ 
$\wedge$$\;\;\;\;${\rm{deadlock-free}}\,({\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\index{deadlock-free} \\ 
$\wedge$$\;\;\;\;${\rm{initial-condition}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{proper-phils}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}} \\ 
{\tt{(}}{\tt{proper-forks}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{initial-condition})\- \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{eventually-stable}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{hungry}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{j}}{\tt{)}} \\ 
{\tt{(}}{\tt{owns-left}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{j}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{eventually-stable})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  hungry-leads-to-owns-right \\ \index{hungry-leads-to-owns-right}
\=\+(\=\+({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{initial-condition}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{proper-phils}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}} \\ 
{\tt{(}}{\tt{proper-forks}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{initial-condition} \\ 
$\wedge$$\;\;\;\;${\rm{strongly-fair}}\,({\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\index{strongly-fair} \\ 
$\wedge$$\;\;\;\;${\rm{deadlock-free}}\,({\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\index{deadlock-free})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{hungry}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}, \\ 
{\tt{`}}{\tt{(}}{\tt{owns-right}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{leads-to}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  correctness \\ \index{correctness}
\=\+(\=\+({\tt{1}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{index\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{initial-condition}}\,(\=\+{\tt{`}}{\tt{(}}\=\+{\tt{and}} \\ 
{\tt{(}}{\tt{proper-phils}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}} \\ 
{\tt{(}}{\tt{proper-forks}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{n}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{initial-condition} \\ 
$\wedge$$\;\;\;\;${\rm{strongly-fair}}\,({\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\index{strongly-fair} \\ 
$\wedge$$\;\;\;\;${\rm{deadlock-free}}\,({\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\index{deadlock-free})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{leads-to}}\,(\=\+{\tt{`}}{\tt{(}}{\tt{hungry}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}, \\ 
{\tt{`}}{\tt{(}}{\tt{eating}}{\tt{ }}{\tt{state}}{\tt{ }}{\tt{'}}{\tt{,}}{\tt{index}}{\tt{)}}, \\ 
{\rm{phil-prg}}\,({\it{n\/}})\index{phil-prg})\-\index{leads-to}\-
\end{tabbing}


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