%\documentstyle[11pt,tla94-1,twoside]{article}
%\documentstyle[llncstla]{llncs}
\documentstyle{article}
%%* "Specifying and Verifying Fault-Tolerant Systems"
%%*  by Leslie Lamport and Stephan Merz.
%%*  TLA+ specification and verification of a simple Byzantine generals
%%*  algorithm.  To appear in FTRTFT'94.
%%
%% Cleared by Sam, 28 Jul 94 
%%     typo corrected 14 Oct 94

\makeatletter
%% file llncs.st
% LLNCS DOCUMENT STYLE -- version 1.2
% for LaTeX version 2.09

% This style file is an adaptation of
% the original LaTeX article.sty
% Modified by Leslie Lamport to
%  * remove the silly ``This article was typset using the ...'' at the
%    end.
%  * remove stretch between paragraphs.
%  * add page numbers, far enough from the text that Springer should
%    be able to cope with them.
%  * made optional argument work with the figure command
%
\typeout{Document Style `llncs', <version 1.2>}

\frenchspacing
\def~{\penalty\@M\kern3pt}

% Language dependant section
\def\literaturename{References}
\def\contentsname{Table of Contents}
\def\listoffiguresname{List of Figures}
\def\figurename{Fig.\thinspace}
\def\listoftablesname{List of Tables}
\def\tablename{Table }
\def\abstractname{Abstract.}
\newif\if@deutsch\@deutschfalse
%
\def\ds@deutsch{\typeout{German version}
\def\literaturename{Literatur}
\def\contentsname{Inhaltsverzeichnis}
\def\listoffiguresname{Abbildungsverzeichnis}
\def\figurename{Abb.\thinspace}
\def\listoftablesname{Tabellenverzeichnis}
\def\tablename{Tabelle }
\def\abstractname{Zusammenfassung.}
\@deutschtrue}

\def\thebibliography#1{\section*{\literaturename}\small\list
  {\arabic{enumi}.}{\settowidth\labelwidth{#1.}\leftmargin\labelwidth
    \advance\leftmargin\labelsep
    \usecounter{enumi}}
    \def\newblock{\hskip .11em plus .33em minus -.07em}
    \sloppy
    \sfcode`\.=1000\relax}

\def\ds@citeauthoryear{\def\thebibliography##1{\section*{\literaturename}%
    \small\list{}{\settowidth\labelwidth{}\leftmargin\parindent
    \itemindent=-\parindent
    \labelsep=\z@
    \usecounter{enumi}}%
    \def\newblock{\hskip .11em plus .33em minus -.07em}%
    \sloppy
    \sfcode`\.=1000\relax}%
    \def\@cite##1{##1}%
    \def\@lbibitem[##1]##2{\item[]\if@filesw
      {\def\protect####1{\string ####1\space}\immediate
    \write\@auxout{\string\bibcite{##2}{##1}}}\fi\ignorespaces}}%

\newif\if@envcountreset\@envcountresetfalse
\def\ds@envcountreset{\@envcountresettrue}

\def\@mbi{cmmib10}
\def\@ptsize{0} \@namedef{ds@11pt}{\def\@ptsize{1}}
\@namedef{ds@12pt}{\def\@ptsize{2}}
\def\ds@twoside{\@twosidetrue \@mparswitchtrue}
\def\ds@draft{\overfullrule
5pt}
\@options

\ds@twoside

\lineskip 1pt \normallineskip 1pt
\def\baselinestretch{1}

\def\@normalsize{\@setsize\normalsize{12pt}\xpt\@xpt
\abovedisplayskip=3 mm plus6pt minus 4pt
\belowdisplayskip=3 mm plus6pt minus 4pt
\abovedisplayshortskip=0mm plus6pt minus 2pt
\belowdisplayshortskip=2 mm plus4pt minus 4pt}

\mathchardef\Gamma="0100
\mathchardef\Delta="0101
\mathchardef\Theta="0102
\mathchardef\Lambda="0103
\mathchardef\Xi="0104
\mathchardef\Pi="0105
\mathchardef\Sigma="0106
\mathchardef\Upsilon="0107
\mathchardef\Phi="0108
\mathchardef\Psi="0109
\mathchardef\Omega="010A

\def\small{\@setsize\small{11pt}\ixpt\@ixpt
\abovedisplayskip=2.5 mm plus5pt minus 3pt
\belowdisplayskip=2.5 mm plus5pt minus 3pt
\abovedisplayshortskip=0mm plus6pt minus 2pt
\belowdisplayshortskip=2 mm plus4pt minus 4pt
\def\@listi{\leftmargin\leftmargini\topsep 4pt plus 2pt minus 2pt}}

\def\footnotesize{\@setsize\footnotesize{11pt}\ixpt\@ixpt
\abovedisplayskip=2.5 mm plus5pt minus 3pt
\belowdisplayskip=2.5 mm plus5pt minus 3pt
\abovedisplayshortskip=0mm plus6pt minus 2pt
\belowdisplayshortskip=2 mm plus4pt minus 4pt
\def\@listi{\leftmargin\leftmargini\topsep 4pt plus 2pt minus 2pt}}

\def\scriptsize{\@setsize\scriptsize{8.4pt}\viipt\@viipt}

\def\tiny{\@setsize\tiny{6pt}\vpt\@vpt}
\def\large{\@setsize\large{13.2pt}\xipt\@xipt}
\def\Large{\@setsize\Large{14.4pt}\xiipt\@xiipt}
\def\LARGE{\@setsize\LARGE{16.8pt}\xivpt\@xivpt}
\def\huge{\@setsize\huge{22pt}\xxpt\@xxpt}
\def\Huge{\@setsize\Huge{30pt}\xxvpt\@xxvpt}
\@normalsize

\if@twoside
   \oddsidemargin  44pt
   \evensidemargin 82pt
   \marginparwidth 107pt
\else \oddsidemargin 63pt \evensidemargin 63pt
 \marginparwidth 90pt
\fi
\marginparsep 11pt
\topmargin 11pt \headheight 12pt \headsep 13.66pt
\footheight 12pt \footskip 30pt
\textwidth 12.2truecm
\textheight 19.3truecm
\columnsep 1cc \columnseprule 0pt

\footnotesep 7.7pt
\skip\footins 9pt plus 4pt minus 2pt
\floatsep 12pt plus 2pt minus 2pt
\textfloatsep 8mm plus 2pt minus 4pt
\intextsep 8mm plus 2pt minus 2pt
\@maxsep 8mm

\dblfloatsep 12pt plus 2pt minus 2pt
\dbltextfloatsep 20pt plus 2pt minus 4pt
\@dblmaxsep 20pt

\@fptop 0pt plus 1fil \@fpsep 8pt plus 2fil \@fpbot 0pt plus 1fil
\@dblfptop0pt plus1fil \@dblfpsep8pt plus2fil\@dblfpbot 0pt plus1fil
\marginparpush 5pt

%% \parskip 0pt plus 1pt    %% Original version.
\parskip 0pt                %% Version modified by L.L to remove stretch
\parindent 1.5em \topsep 8pt plus 2pt minus 4pt
\partopsep 2pt plus 1pt minus 1pt \itemsep \z@
\@lowpenalty 51 \@medpenalty 151 \@highpenalty 301
\@beginparpenalty-\@lowpenalty\@endparpenalty -\@lowpenalty\@itempenalty
-\@lowpenalty

\def\vec#1{\mathchoice{\mbox{\boldmath$\displaystyle\bf#1$}}
{\mbox{\boldmath$\textstyle\bf#1$}}
{\mbox{\boldmath$\scriptstyle\bf#1$}}
{\mbox{\boldmath$\scriptscriptstyle\bf#1$}}}

\def\@sect#1#2#3#4#5#6[#7]#8{\ifnum #2>\c@secnumdepth
  \def\@svsec{}\else
  \refstepcounter{#1}\edef\@svsec{\csname the#1\endcsname\quad }\fi
  \@tempskipa #5\relax
   \ifdim \@tempskipa>\z@
  \begingroup #6\relax
  \noindent{\hskip #3\relax\@svsec}{\interlinepenalty \@M #8\par}
  \endgroup
    \csname #1mark\endcsname{#7}\addcontentsline
   {toc}{#1}{\ifnum #2>\c@secnumdepth \else
            \protect\numberline{\csname the#1\endcsname}\fi
          #7}\else
  \def\@svsechd{#6\hskip #3\@svsec #8\csname #1mark\endcsname
            {#7}\addcontentsline
             {toc}{#1}{\ifnum #2>\c@secnumdepth \else
               \protect\numberline{\csname the#1\endcsname}\fi
             #7}}\fi
  \@xsect{#5}}

\def\part{\par \addvspace{4ex} \@afterindentfalse \secdef\@part\@spart}

\def\@part[#1]#2{\ifnum \c@secnumdepth >\m@ne \refstepcounter{part}
\addcontentsline{toc}{part}{\thepart \hspace{1em}#1}\else
\addcontentsline{toc}{part}{#1}\fi { \parindent 0pt \raggedright
 \ifnum \c@secnumdepth >\m@ne \Large \bf
 Part\thepart\par\nobreak\fi\huge
\bf #2\markboth{}{}\par } \nobreak \vskip 3ex \@afterheading }

\def\@spart#1{{\parindent 0pt \raggedright
 \huge \bf
 #1\par} \nobreak \vskip 3ex \@afterheading }

\def\section{\@startsection {section}{1}{\z@}{-18pt plus -4pt minus
-4pt}{12pt plus 4pt minus 4pt}{\Large\bf\boldmath
\pretolerance=10000\relax\rightskip=0pt plus8em}}
\def\subsection{\@startsection{subsection}{2}{\z@}{-18pt plus-4pt minus
 -4pt}{8pt plus 4pt minus 4pt}{\normalsize\bf\boldmath
\pretolerance=10000\relax\rightskip=0pt plus8em}}
\def\subsubsection{\@startsection{subsubsection}{3}{\z@}{-18pt plus-4pt
 minus -4pt}{-0.5em plus -.22em minus -0.1em}{\normalsize\bf\boldmath}}
\def\paragraph{\@startsection{paragraph}{4}{\z@}{-12pt plus -4pt minus
 -4pt}{-0.5em plus -.22em minus -0.1em}{\normalsize\it}}
\def\subparagraph#1{\typeout{LLNCS Warning: You should not use
\protect\subparagraph \space in this style.}\vskip0.5cm
You should not use $\backslash${\tt subparagraph} in this
style.\vskip0.5cm}

\setcounter{secnumdepth}{2}

\def\appendix{\par
 \setcounter{section}{0}
 \setcounter{subsection}{0}
 \def\thesection{\Alph{section}}}

\leftmargini 17pt     \leftmarginii 17pt
\leftmarginiii 17pt   \leftmarginiv 17pt
\leftmarginv 10pt       \leftmarginvi 10pt
\leftmargin\leftmargini \labelwidth\leftmargini
\advance\labelwidth-\labelsep
\labelsep 5pt
\parsep 0pt plus 1pt
\def\@listi{\leftmargin\leftmargini}
\def\@listii{\leftmargin\leftmarginii
 \labelwidth\leftmarginii\advance\labelwidth-\labelsep
 \topsep 0pt plus 1pt}
\def\@listiii{\leftmargin\leftmarginiii
 \labelwidth\leftmarginiii\advance\labelwidth-\labelsep
 \topsep 0pt plus 1pt}
\def\@listiv{\leftmargin\leftmarginiv
 \labelwidth\leftmarginiv\advance\labelwidth-\labelsep
 \topsep 0pt plus 1pt}
\def\@listv{\leftmargin\leftmarginv
 \labelwidth\leftmarginv\advance\labelwidth-\labelsep
 \topsep 0pt plus 1pt}
\def\@listvi{\leftmargin\leftmarginvi
 \labelwidth\leftmarginvi\advance\labelwidth-\labelsep
 \topsep 0pt plus 1pt}

\def\labelenumi{\arabic{enumi}.}
\def\theenumi{\arabic{enumi}}
\def\labelenumii{(\alph{enumii})}
\def\theenumii{\alph{enumii}}
\def\p@enumii{\theenumi}
\def\labelenumiii{\roman{enumiii}.}
\def\theenumiii{\roman{enumiii}}
\def\p@enumiii{\theenumi(\theenumii)}
\def\labelenumiv{\Alph{enumiv}.}
\def\theenumiv{\Alph{enumiv}}
\def\p@enumiv{\p@enumiii\theenumiii}

\def\labelitemi{\bf --}
\def\labelitemii{$\bullet$}
\def\labelitemiii{$\ast$}
\def\labelitemiv{$\cdot$}

\def\verse{\let\\=\@centercr
 \list{}{\itemsep\z@ \itemindent -1.5em\listparindent \itemindent
 \rightmargin\leftmargin\advance\leftmargin 1.5em}\item[]}
\let\endverse\endlist
\def\quotation{\list{}{\listparindent 1.5em
 \itemindent\listparindent
 \rightmargin\leftmargin}\item[]}
\let\endquotation=\endlist
\def\quote{\list{}{\rightmargin\leftmargin}\item[]}
\let\endquote=\endlist

\def\descriptionlabel#1{\hspace\labelsep \bf #1}
\def\description{\list{}{\labelwidth\z@ \itemindent-\leftmargin
 \let\makelabel\descriptionlabel}}
\let\enddescription\endlist

\def\theequation{\arabic{equation}}

\def\titlepage{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn
 \else \newpage \fi \thispagestyle{empty}\c@page\z@}
\def\endtitlepage{\if@restonecol\twocolumn \else \newpage \fi}

\arraycolsep 1.4pt \tabcolsep 1.4pt \arrayrulewidth .4pt \doublerulesep
2pt
\tabbingsep \labelsep

\skip\@mpfootins = \skip\footins
\fboxsep = 3pt \fboxrule = .4pt

%\newcounter{part}
%\newcounter {section}
%\newcounter {subsection}[section]
%\newcounter {subsubsection}[subsection]
%\newcounter {paragraph}[subsubsection]

\def\thepart{\Roman{part}}
\def\thesection {\arabic{section}}
\def\thesubsection {\thesection.\arabic{subsection}}
\def\thesubsubsection {\thesubsection.\arabic{subsubsection}}
\def\theparagraph {\thesubsubsection.\arabic{paragraph}}

\def\@pnumwidth{1.55em}
\def\@tocrmarg {2.55em}
\def\@dotsep{4.5}
\setcounter{tocdepth}{3}

\def\tableofcontents{\section*{\contentsname}
 \@starttoc{toc}}
\def\l@part#1#2{\addpenalty{\@secpenalty}
 \addvspace{2.25em plus 1pt} \begingroup
 \@tempdima 3em \parindent \z@ \rightskip \@pnumwidth \parfillskip
-\@pnumwidth
 {\Large \bf \leavevmode #1\hfil \hbox to\@pnumwidth{\hss #2}}\par
 \nobreak \endgroup}
%
\def\numberline#1{\advance\hangindent by\@tempdima%
\hbox to\@tempdima{\hss#1\enspace}}
%
\def\bf@dottedtocline#1#2#3#4#5{\ifnum #1>\c@tocdepth \else
  \vskip \z@ plus .2pt
  {\leftskip #2\relax \rightskip \@tocrmarg \parfillskip -\rightskip
    \parindent #2\relax\@afterindenttrue
   \interlinepenalty\@M
   \leavevmode
   \@tempdima #3\relax \advance\leftskip \@tempdima \hbox{}\hskip
   -\leftskip
{\bf#4}\nobreak\leaders\hbox{$\m@th \mkern \@dotsep mu.\mkern \@dotsep
       mu$}\hfill \nobreak \hbox to\@pnumwidth{\hfil\rm #5}\par}\fi}
%
\def\l@section{\vskip2mm\bf@dottedtocline{1}{0em}{1.7em}}
\def\l@subsection{\@dottedtocline{2}{1.7em}{2.3em}}
\def\l@subsubsection{\@dottedtocline{3}{4em}{2em}}
\def\l@paragraph{\@dottedtocline{4}{6em}{2em}}
\def\l@subparagraph{\@dottedtocline{5}{8em}{2em}}
\def\listoffigures{\section*{\listoffiguresname\markboth
 {\listoffiguresname}{\listoffiguresname}}\@starttoc{lof}}
\def\l@figure{\@dottedtocline{1}{1.5em}{2.3em}}
\def\listoftables{\section*{\listoftablesname\markboth
 {\listoftablesname}{\listoftablesname}}\@starttoc{lot}}
\let\l@table\l@figure

\def\endthebibliography{\endlist\normalsize}

\newif\if@restonecol
\def\theindex{\@restonecoltrue\if@twocolumn\@restonecolfalse\fi
\columnseprule \z@
\columnsep 35pt\twocolumn[\section*{Index}]
 \markboth{Index}{Index}\thispagestyle{plain}\parindent\z@
 \parskip\z@ plus .3pt\relax\let\item\@idxitem}
\def\@idxitem{\par\hangindent 40pt}
\def\subitem{\par\hangindent 40pt \hspace*{20pt}}
\def\subsubitem{\par\hangindent 40pt \hspace*{30pt}}
\def\endtheindex{\if@restonecol\onecolumn\else\clearpage\fi}
\def\indexspace{\par \vskip 10pt plus 5pt minus 3pt\relax}

\def\footnoterule{\kern-3\p@\hrule width 2 true cm\kern 2.6\p@}

\long\def\@makefntext#1{\@setpar{\@@par\@tempdima \hsize
  \advance\@tempdima-1em\parshape \@ne 1em\@tempdima}\par
  \parindent 1em\noindent \hbox to \z@{\hss$^{\@thefnmark}$\ }#1}

\setcounter{topnumber}{2}
\def\topfraction{.9}
\setcounter{bottomnumber}{1}
\def\bottomfraction{.3}
\setcounter{totalnumber}{3}
\def\textfraction{.15}
\def\floatpagefraction{.85}
\setcounter{dbltopnumber}{2}
\def\dbltopfraction{.85}
\def\dblfloatpagefraction{.85}

\long\def\@makecaption#1#2{
 \vskip 10pt
 \setbox\@tempboxa\hbox{{\bf #1} #2}
 \ifdim \wd\@tempboxa >\hsize \unhbox\@tempboxa\par \else \hbox
to\hsize{\hfil\box\@tempboxa\hfil}
 \fi\vskip5pt}

\long\def\@caption#1[#2]#3{\addcontentsline{\csname
  ext@#1\endcsname}{#1}{\protect\numberline{\csname
  the#1\endcsname}{\ignorespaces #2}}\par
  \begingroup
    \@parboxrestore
    \@makecaption{\csname fnum@#1\endcsname}{\ignorespaces #3}\par
  \endgroup}

%\newcounter{figure}
\def\thefigure{\@arabic\c@figure}

\def\fps@figure{htbp}
\def\ftype@figure{1}
\def\ext@figure{lof}
\def\fnum@figure{\figurename\thefigure.}
%%\def\figure{\small\rm\@float{figure}}           %% Original
\def\figure{\@ifnextchar[{\@yfigure}{\@xfigure}}  %% New version by L.L.
\def\@xfigure{\small\rm\@float{figure}}           %% "
\def\@yfigure[#1]{\small\rm\@float{figure}[#1]}   %% "
\def\endfigure{\vskip-5pt\end@float}
\@namedef{figure*}{\@dblfloat{figure}}
\@namedef{endfigure*}{\end@dblfloat}

%\newcounter{table}
\def\thetable{\@arabic\c@table}
\def\fps@table{htbp}
\def\ftype@table{2}
\def\ext@table{lot}
\def\fnum@table{\tablename\thetable.}
\def\table{\small\rm\@float{table}}
\let\endtable\end@float
\@namedef{table*}{\@dblfloat{table}}
\@namedef{endtable*}{\end@dblfloat}

% LaTeX does not provide a command to enter the authors institute
% addresses. The \institute command is defined here.

\newcounter{@inst}
\newcounter{@auth}

\def\institute#1{\gdef\@institute{#1}}

\def\institutename{\par
 \begingroup
 \parskip=\z@
 \parindent=\z@
 \setcounter{@inst}{1}%
 \def\and{\par\stepcounter{@inst}%
 \noindent$^{\the@inst}$\enspace\ignorespaces}%
 \setbox0=\vbox{\def\thanks##1{}\@institute}%
 \ifnum\c@@inst=1\relax
 \else
   \setcounter{footnote}{\c@@inst}%
   \setcounter{@inst}{1}%
   \noindent$^{\the@inst}$\enspace
 \fi
 \ignorespaces
 \@institute\par
 \endgroup}

\def\@thanks{}

\def\@fnsymbol#1{\ifcase#1\or\star\or{\star\star}\or{\star\star\star}%
   \or \dagger\or \ddagger\or
   \mathchar "278\or \mathchar "27B\or \|\or **\or \dagger\dagger
   \or \ddagger\ddagger\else\@ctrerr\fi\relax}

\def\inst#1{\unskip$^{#1}$}

\def\subtitle#1{\gdef\@subtitle{#1}}
\def\@subtitle{}

\def\maketitle{\par
 \begingroup
 \parindent=\z@
 \def\thefootnote{\fnsymbol{footnote}}
 \if@twocolumn
 \twocolumn[\@maketitle]
 \else \newpage
 \global\@topnum\z@ \@maketitle \fi\thispagestyle{empty}\@thanks
 \endgroup
 \let\maketitle\relax
 \let\@maketitle\relax
 \gdef\@thanks{}\gdef\@author{}\gdef\@title{}\gdef\@subtitle{}%
 \let\thanks\relax}

\def\@maketitle{\newpage
 \begin{center}%
 {\LARGE \bf\boldmath
  \pretolerance=10000
  \@title \par}\vskip .8cm
\if!\@subtitle!\else {\Large \bf\boldmath
  \vskip -.65cm
  \pretolerance=10000
  \@subtitle \par}\vskip .8cm\fi
{\normalsize\rm\lineskip .5em
\@author\vskip.35cm}
 {\small\rm\institutename}
 \end{center}%
 }

\mark{{}{}}

% Define `abstract' environment
\def\abstract{%
\list{}{\advance\topsep by0.35cm\relax\small\rm
 \leftmargin=1cm
 \labelwidth=\z@
 \listparindent=\z@
 \itemindent\listparindent
 \rightmargin\leftmargin}\item[\hskip\labelsep\bf\abstractname]}
\let\endabstract=\endlist
\def\quote{\list{}{\rightmargin\leftmargin}\item[]}
\let\endquote=\endlist

%% original:
% \def\ps@headings{\def\@evenhead{}%  
% \let\@oddhead\@evenhead         
% \let\@evenfoot\@evenhead
% \let\@oddfoot\@evenhead     
% \def\sectionmark##1{}%
% \def\subsectionmark##1{}}

%%% Modified by L.L. to print page numbers:
\def\ps@headings{\def\@evenhead{\makebox[\textwidth]{\hfill 
   \raisebox{2cm}[0pt][0pt]{\fbox{\LARGE\thepage}\hspace{-2cm}}}}%
\let\@oddhead\@evenhead
\def\@evenfoot{}
\let\@oddfoot\@evenfoot
\def\sectionmark##1{}%
\def\subsectionmark##1{}}


\def\ps@myheadings{\let\@mkboth\@gobbletwo
\def\@oddhead{\hbox{}\small\rm\rightmark \hfil\thepage}%
\def\@oddfoot{}\def\@evenhead{\small\rm\thepage\hfil
\leftmark\hbox {}}%
\def\@evenfoot{}\def\sectionmark##1{}\def\subsectionmark##1{}}

\def\today{\ifcase\month\or
 January\or February\or March\or April\or May\or June\or
 July\or August\or September\or October\or November\or December\fi
 \space\number\day, \number\year}

\ps@headings \pagenumbering{arabic} \onecolumn
\if@twoside\else\raggedbottom\fi

% new environments and theorems
% borrowed form the LTMP-style of Springer-Verlag
% designed by Dr. Christoph Ender
%
% define the new theorem like environments
% define a new style of environments where it is possible to define
% the font % used as the theorem name and the fontfamily for the text.
%
% \newstytheorem{name}{thefont}{txtfont}{Text}[Counter]
% \newstytheorem{name}{thefont}{txtfont}[oldname]{Text}
%
% #1 - name of theorem
% #2 - theorem font
% #3 - text font
%
\def\newstytheorem#1#2#3{%
\@ifnextchar[{\che@othm{#1}{#2}{#3}}{\che@nthm{#1}{#2}{#3}}}
%
% #1 - name of theorem
% #2 - theorem font
% #3 - text font
% #4 - text string of thorem name
%
\def\che@nthm#1#2#3#4{%
\@ifnextchar[{\che@xnthm{#1}{#2}{#3}{#4}}{\che@ynthm{#1}{#2}{#3}{#4}}}
%
% #1 - name of theorem
% #2 - theorem font
% #3 - text font
% #4 - text string of thorem name
% #5 - add theorem counter to reset list of another counter
%
\def\che@xnthm#1#2#3#4[#5]{\expandafter
\@ifdefinable\csname #1\endcsname
{\@definecounter{#1}\if@envcountreset\@addtoreset{#1}{#5}\fi
\expandafter\xdef\csname the#1\endcsname{\@thmcounter{#1}}%
\global\@namedef{#1}{\che@thm{#1}{#4}{#2}{#3}}\global
\@namedef{end#1}{\@endtheorem}}}
%
% #1 - name of theorem
% #2 - theorem font
% #3 - text font
% #4 - text string of thorem name
%
\def\che@ynthm#1#2#3#4{\expandafter\@ifdefinable\csname #1\endcsname
{\@definecounter{#1}%
\expandafter\xdef\csname the#1\endcsname{\@thmcounter{#1}}%
\global\@namedef{#1}{\che@thm{#1}{#2}{#3}{#4}}\global
\@namedef{end#1}{\@endtheorem}}}
%
% change oldthm if oldname in specification is '*'
% then don't use a counter
% #1 - countername
% #2 - theorem font
% #3 - text font
% #4 - counter used
% #5 - string containing theorem name to print
%
\def\che@othm#1#2#3[#4]#5{\expandafter\@ifdefinable
\csname#1\endcsname%
{\@@othm@{#1}{#2}{#3}{#4}{#5}\global\@namedef{end#1}{\@endtheorem}}}
%
\def\@@othm@#1#2#3#4#5{\if *#4{\global\@namedef{the#1}{\relax}
\global\@namedef{#1}{\@bthm@{}{#5}{#2}{#3}}}\else
{\global\@namedef{the#1}{\@nameuse{the#4}}% define the counter
\global\@namedef{#1}{\che@thm{#4}{#5}{#2}{#3}}}\fi}
%
% new defs for theorem environment che 17-MAR-1989
% it improves the option possible
%
% #1 - countername  = theorem name
% #2 - string containing theorem name to print
% #3 - theorem font
% #4 - text font
\def\che@thm#1#2#3#4{\@ifnextchar({\@athm{#1}{#2}{#3}{#4}}{%
\@ifnextchar *{\@bthm{#1}{#2}{#3}{#4}}%
{\@@thm{#1}{#2}{#3}{#4}}}}
%
% \begin{thm}(A.1)[test]      results in:
% \end{thm}                               thm A.1 (test) ....
% #1 - theorem
% #2 - string of theorem name
% #3 - font for theorem name and label
% #4 - Text font
% #5 - is the new label
% #6 - optional string
%
\def\@athm#1#2#3#4(#5){\@ifnextchar[{%
\@aythm{#1}{#2}{#3}{#4}{#5}}{\@axthm{#1}{#2}{#3}{#4}{#5}}}
\def\@axthm#1#2#3#4#5{\@@locthmlab{#1}{#5}%
\@begintheorem{#2}{#5}{#3}{#4}\ignorespaces}
\def\@aythm#1#2#3#4#5[#6]{\@@locthmlab{#1}{#5}%
\fuh@opargbegintheorem{#2}{#5}{#6}{#3}{#4}\ignorespaces}
%
% \begin{thm}*[xytest]        results in:
% \end{thm}                               thm (xytest) ....
% #1 - theorem
% #2 - string of theorem name
% #3 - font for theorem name and label
% #4 - Text font
% #5 - optional string
%
\def\@bthm@#1#2#3#4{\@ifnextchar[{\@bythm{#1}{#2}{#3}{#4}}{%
\@bxthm{#1}{#2}{#3}{#4}}}
\def\@bthm#1#2#3#4*{\@ifnextchar[{\@bythm{#1}{#2}{#3}{#4}}{%
\@bxthm{#1}{#2}{#3}{#4}}}
\def\@bxthm#1#2#3#4{\if !#1!\relax\else\@@locthmlab{#1}{}\fi
\@@begintheorem{#2}{#3}{#4}\ignorespaces}
\def\@bythm#1#2#3#4[#5]{%
\@@opargbegintheorem{#2}{#3}{#4}{#5}\ignorespaces}
%
% define local label
%   if no number or a user specified label occured
%
\def\@@locthmlab#1#2{\expandafter\def\csname the#1\endcsname{#2}
\let\@chetempa\protect\def\protect{\noexpand\protect\noexpand}%
\edef\@currentlabel{\csname p@#1\endcsname\csname the#1\endcsname}%
\let\protect\@chetempa}
%
% #1 - counter = theorem name
% #2 - string with name
% #3 - font for theorem name and label
% #4 - font for text
\def\@@thm#1#2#3#4{\refstepcounter
    {#1}\@ifnextchar[{\che@ythm{#1}{#2}{#3}{#4}}{%
    \che@xthm{#1}{#2}{#3}{#4}}}
%
\def\che@xthm#1#2#3#4{\che@begintheorem{#2}{\csname
the#1\endcsname}{#3}{#4}\ignorespaces}
\def\che@ythm#1#2#3#4[#5]{\che@opargbegintheorem{#2}{\csname
       the#1\endcsname}{#5}{#3}{#4}\ignorespaces}
%
% #1 - name of theorem
% #2 - label string
% #3 - font for name and lable
% #4 - text fomt
%
\def\che@begintheorem#1#2#3#4{#4\trivlist\item[\hskip\labelsep
#3#1\ts #2.]}
%
% #1 - name of theorem
% #2 - label string
% #3 - additonal text
% #4 - font for name and lable
% #5 - text fomt
%
\def\che@opargbegintheorem#1#2#3#4#5{#5\trivlist
\item[\hskip\labelsep#4#1\ts #2\ #3.]}
%
\def\fuh@opargbegintheorem#1#2#3{\it \trivlist
      \item[\hskip \labelsep{\bf #1\ #2\ (#3).}]}
%
\def\@@begintheorem#1#2#3{#3\trivlist\item[\hskip\labelsep
#2#1.]}
\def\@@opargbegintheorem#1#2#3#4{#3\trivlist\item[\hskip\labelsep
#2#1 #4.]}

\if@deutsch
\newstytheorem{theorem}{\bf}{\it}{Theorem}[section]
\newstytheorem{example}{\it}{\rm}{Beispiel}[section]
\newstytheorem{proposition}{\bf}{\it}[theorem]{Proposition}
\newstytheorem{corollary}{\bf}{\it}[theorem]{Korollar}
\newstytheorem{lemma}{\bf}{\it}[theorem]{Lemma}
\newstytheorem{proof}{\it}{\rm}[*]{Beweis}
\newstytheorem{definition}{\bf}{\rm}[theorem]{Definition}
\newstytheorem{remark}{\it}{\rm}[*]{Anmerkung}
\newstytheorem{exercise}{\it}{\rm}[theorem]{\"{U}bung}
\newstytheorem{problem}{\it}{\rm}[theorem]{Problem}
\newstytheorem{solution}{\it}{\rm}[theorem]{L\"{o}sung}
\newstytheorem{note}{\it}{\rm}[theorem]{Hinweis}
\newstytheorem{question}{\it}{\rm}[theorem]{Frage}
\else
\newstytheorem{theorem}{\bf}{\it}{Theorem}[section]
\newstytheorem{example}{\it}{\rm}{Example}[section]
\newstytheorem{proposition}{\bf}{\it}[theorem]{Proposition}
\newstytheorem{corollary}{\bf}{\it}[theorem]{Corollary}
\newstytheorem{lemma}{\bf}{\it}[theorem]{Lemma}
\newstytheorem{proof}{\it}{\rm}[*]{Proof}
\newstytheorem{definition}{\bf}{\rm}[theorem]{Definition}
\newstytheorem{remark}{\it}{\rm}[*]{Remark}
\newstytheorem{exercise}{\it}{\rm}[theorem]{Exercise}
\newstytheorem{problem}{\it}{\rm}[theorem]{Problem}
\newstytheorem{solution}{\it}{\rm}[theorem]{Solution}
\newstytheorem{note}{\it}{\rm}[theorem]{Note}
\newstytheorem{question}{\it}{\rm}[theorem]{Question}
\fi

\def\squareforqed{\hbox{\rlap{$\sqcap$}$\sqcup$}}
\def\qed{\ifmmode\squareforqed\else{\unskip\nobreak\hfil
\penalty50\hskip1em\null\nobreak\hfil\squareforqed
\parfillskip=0pt\finalhyphendemerits=0\endgraf}\fi}

\def\getsto{\mathrel{\mathchoice {\vcenter{\offinterlineskip
\halign{\hfil
$\displaystyle##$\hfil\cr\gets\cr\to\cr}}}
{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr\gets
\cr\to\cr}}}
{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr\gets
\cr\to\cr}}}
{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
\gets\cr\to\cr}}}}}
\def\lid{\mathrel{\mathchoice {\vcenter{\offinterlineskip\halign{\hfil
$\displaystyle##$\hfil\cr<\cr\noalign{\vskip1.2pt}=\cr}}}
{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr<\cr
\noalign{\vskip1.2pt}=\cr}}}
{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr<\cr
\noalign{\vskip1pt}=\cr}}}
{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
<\cr
\noalign{\vskip0.9pt}=\cr}}}}}
\def\gid{\mathrel{\mathchoice {\vcenter{\offinterlineskip\halign{\hfil
$\displaystyle##$\hfil\cr>\cr\noalign{\vskip1.2pt}=\cr}}}
{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr>\cr
\noalign{\vskip1.2pt}=\cr}}}
{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr>\cr
\noalign{\vskip1pt}=\cr}}}
{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
>\cr
\noalign{\vskip0.9pt}=\cr}}}}}
\def\grole{\mathrel{\mathchoice {\vcenter{\offinterlineskip
\halign{\hfil
$\displaystyle##$\hfil\cr>\cr\noalign{\vskip-1pt}<\cr}}}
{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr
>\cr\noalign{\vskip-1pt}<\cr}}}
{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr
>\cr\noalign{\vskip-0.8pt}<\cr}}}
{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
>\cr\noalign{\vskip-0.3pt}<\cr}}}}}
\def\bbbr{{\rm I\!R}} %reelle Zahlen
\def\bbbm{{\rm I\!M}}
\def\bbbn{{\rm I\!N}} %natuerliche Zahlen
\def\bbbf{{\rm I\!F}}
\def\bbbh{{\rm I\!H}}
\def\bbbk{{\rm I\!K}}
\def\bbbp{{\rm I\!P}}
\def\bbbone{{\mathchoice {\rm 1\mskip-4mu l} {\rm 1\mskip-4mu l}
{\rm 1\mskip-4.5mu l} {\rm 1\mskip-5mu l}}}
\def\bbbc{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm C$}\hbox{\hbox
to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
{\setbox0=\hbox{$\textstyle\rm C$}\hbox{\hbox
to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
{\setbox0=\hbox{$\scriptstyle\rm C$}\hbox{\hbox
to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
{\setbox0=\hbox{$\scriptscriptstyle\rm C$}\hbox{\hbox
to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}}}
\def\bbbq{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm
Q$}\hbox{\raise
0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.8\ht0\hss}\box0}}
{\setbox0=\hbox{$\textstyle\rm Q$}\hbox{\raise
0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.8\ht0\hss}\box0}}
{\setbox0=\hbox{$\scriptstyle\rm Q$}\hbox{\raise
0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.7\ht0\hss}\box0}}
{\setbox0=\hbox{$\scriptscriptstyle\rm Q$}\hbox{\raise
0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.7\ht0\hss}\box0}}}}
\def\bbbt{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm
T$}\hbox{\hbox to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
{\setbox0=\hbox{$\textstyle\rm T$}\hbox{\hbox
to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
{\setbox0=\hbox{$\scriptstyle\rm T$}\hbox{\hbox
to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
{\setbox0=\hbox{$\scriptscriptstyle\rm T$}\hbox{\hbox
to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}}}
\def\bbbs{{\mathchoice
{\setbox0=\hbox{$\displaystyle     \rm S$}\hbox{\raise0.5\ht0\hbox
to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\hbox
to0pt{\kern0.55\wd0\vrule height0.5\ht0\hss}\box0}}
{\setbox0=\hbox{$\textstyle        \rm S$}\hbox{\raise0.5\ht0\hbox
to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\hbox
to0pt{\kern0.55\wd0\vrule height0.5\ht0\hss}\box0}}
{\setbox0=\hbox{$\scriptstyle      \rm S$}\hbox{\raise0.5\ht0\hbox
to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\raise0.05\ht0\hbox
to0pt{\kern0.5\wd0\vrule height0.45\ht0\hss}\box0}}
{\setbox0=\hbox{$\scriptscriptstyle\rm S$}\hbox{\raise0.5\ht0\hbox
to0pt{\kern0.4\wd0\vrule height0.45\ht0\hss}\raise0.05\ht0\hbox
to0pt{\kern0.55\wd0\vrule height0.45\ht0\hss}\box0}}}}
\def\bbbz{{\mathchoice {\hbox{$\sf\textstyle Z\kern-0.4em Z$}}
{\hbox{$\sf\textstyle Z\kern-0.4em Z$}}
{\hbox{$\sf\scriptstyle Z\kern-0.3em Z$}}
{\hbox{$\sf\scriptscriptstyle Z\kern-0.2em Z$}}}}
\def\ts{\thinspace}

%% Original version.
% \if@deutsch
% \def\typeset{\vfill\small\noindent Dieser Artikel wurde mit
% dem \LaTeX\ Makro-Paket und dem LLNCS-Style formatiert.\par}
% \else
% \def\typeset{\vfill\small\noindent This article was processed using
% the \LaTeX\ macro package with LLNCS style\par}
% \fi

%% Version modified by L.L. to supress the LaTeX ack,
%%  "This article was processed using
%%  the \LaTeX\ macro package with LLNCS style"
\def\typeset{\vfill\small\noindent 
\par}

\def\enddocument{\par\typeset
\@checkend{document}\clearpage\begingroup
\if@filesw \immediate\closeout\@mainaux
\def\global\@namedef##1##2{}\def\newlabel{\@testdef r}%
\def\bibcite{\@testdef b}\@tempswafalse\makeatletter\input \jobname.aux
\if@tempswa \@warning{Label(s) may have changed. Rerun to get
cross-references right}\fi\fi\endgroup\deadcycles\z@\@@end}

%% file llncstla.sty

%%  TLA DOCUMENT STYLE
%%  (c) 1994 by Leslie Lamport
%
%   This style calls the pf style, which should not be loaded
%   separately.
%
%   Thes style puts LaTeX in TLA mode.  This mode causes the following 
%   changes to LaTeX's normal math mode:
%   
%  Characters are in the normal italic font, rather than math italic.
%  Thus $Off$ will produce something that looks like {\it Off} rather
%  than the usual formula that's supposed to equal $Of^{2}$.
%  
%  The following sequences produce the following commands when LaTeX is
%  `inside math mode', where being inside math mode means being in math
%  mode or in the argument of a command or in an environment (such as
%  \mbox or a minipage or tabular environment) that appears inside a math
%  formula.
%  
%    ==  :  equals by definition (\deq)
%    =>  : \Rightarrow
%    :\: : \backslash
%    []  : \Box 
%    <>  : \Diamond
%    <-  : \leftarrow
%    <<  : \langle
%    >>  : \rangle
%    ->  : \rightarrow
%    |-  : \vdash
%    |=  : \models
%    |-> : \mapsto
%    #   : \neq
%    \/  : \lor
%    /\  : \land   (This command must be followed by a space, and must
%                   not come at the end of a line, unless the line is
%                   ended by a % )
%    "text"  :  {\rm ``{\sf text}''}  (a TLA+ string constant)
%    _.      :  \, 
%    __      :  Produces a `unit' space
%    ___     :  Produces two `unit' spaces
%    __..._  :  Produces n `unit' spaces
%           The default value of a unit space is 1em.  You can reset its 
%           value to .75em by \indentspace{.75em}.
%  
%  The style issues a \coloncommands declaration.  This declaration
%  causes LaTeX to enter colon-command mode.  In colon-command mode,
%  whenever LaTeX is inside math-mode, the string :xxx: is interpreted as
%  \xxx, for any `xxx'.  When LaTeX is inside math mode, a regular colon
%  must be followed by a space.  The declaration \nocoloncommands causes
%  LaTeX to leave colon-command mode.
%  
%  You can leave TLA mode with the \notla declaration, and re-enter it
%  with the \tla declaration.  
%  
%  In TLA mode, the following characters are active while inside math
%  mode:  
%  
%     : [ = < > " _ | / ! - #
%  
%  This means that these characters cannot be used for many purposes--
%  for example:
%  
%     You can't use [ to begin an optional argument.
%     You can't use the following with \left or \right: < > / |
%     You can't use - as a minus sign in something like \hspace{-3pt}.
%  
%  (Since \\ is often used with an optional argument for adding
%  space, the command \V is proved, where \V{.7} means \\[.7em])
%  You can make these characters inactive by a \notlachars command,
%  and reactivate them with \tlachars--for example, so you can write
%  
%       {\notlachars \sqrt[n]{2}}
%  
%  in TLA mode--so long as this doesn't appear in the argument of any
%  command.  The command \xtla{...} is equivalent to
%  
%       {\notlachars ... }
%  
%  
%  The style also defines the following math commands (some particular
%  useful in colon-command mode):
%  
%    \A  :  \forall
%    \E  :  \exists
%    \EE :  bold \exists (TLA's temporal existential quantification)
%    \AA :  bold \forall (TLA's temporal universal quantification)
%    \X  :  \times
%  
%  The following commands, defined here (or in the pf style) are useful
%  in formatting math formulas:
%  
%    For conjunction and disjunction lists, use the conj and disj environments;
%    use noj for a nonbulleted list.
%   
%       \begin{conj}                   /\ x = 7
%          x = 7 \\                    /\ \/ x > z                       
%          \begin{disj}                   \/ (y < foo)  =>
%             x > z \\                         x = 7
%             \begin{noj}
%               (y < foo) => \\ 
%               __x = 7
%             \end{noj}
%           \end{disj}              
%       \end{conj}
%   
%    The environments noj2, noj3, and noj4 make 2-, 3-, and 4-column
%    arrays, with columns separated by &, as usual.
%    These are array environments.
%   
%    if/then/else's are made as follows:
%      \IF{x > 0}    \\                              IF x > 0
%           \THEN    foo                    \\         THEN foo
%           \ELSE    \IF{y > 3} \THEN y + 6 \\         ELSE IF y > 3 THEN y + 6
%                               \ELSE y + 7 \FI \\                   ELSE y + 7
%                    + 3  \FI \\                            + 3
%
%    Let's are made as follows:
%       \LET x == ... \\
%            y == ... 
%       \IN  ...  \NI
%
%    CASE's are made with the \CASE command, which just makes the
%    "CASE"--e.g.,
%
%      \CASE \begin{noj3}
%              p & -> & xy + 7 \\
%              q & -> & xx + 33
%            \end{noj3}
%  The commands \comment{text} and \tlacomment{text} produce
%  multiline comments (lines separated by \\) that take up no
%  vertical space.  Text is "normal" in \comment, and in TLA mode
%  in \tlacomment.
%
%  The style provides the following environments for TLA+ specs:
%     The module, decls, and submodule environments work as 
%     indicated below:
%                           
%       \begin{module}{name}                __________| name |___________
%                                          |          |      |           |
%    
%         \begin{decls}{parameters}          PARAMETERS
%            xyz    : \variable \\            xyz : VARIABLE
%            foobar : \constant               foobar : CONSTANT
%         \end{decls}
%    
%       \midbar                            |-----------------------------|
%    
%          \begin{decls}{actions}            ACTIONS
%              ...                            ...
%          \end{decls}
%   
%          \begin{submodule}{submod}          _________| submod |________
%                                            |         |        |        |
%                ...                              ...   
%    
%          \end{submodule}                   |___________________________|
%    
%       \end{module}                       |_____________________________|
%   
%   
%    The decls environment is a tabbing environment, so lines are ended with 
%    \\, and \= , \>, \\, etc. work as usual.  However, its entries are set 
%    in math mode (so TLA-mode commands work).  Inside a module or submodule
%    environment but outside a decls environment, LaTeX is in paragraph
%    mode, with \it in effect.
%
%    The nodecls environment is like the decls environment, except it 
%    has no title (and no argument) and does not indent and does
%
%    The following commands produce the obvious keywords:
%
%       \IMPORT  \EXPORT   \INCLUDE   \AS  
%       \variable   \constant  \boolean \action \statefcn
%       \unchanged  \except  \enabled \choose [replaces Plain TeX command]
%       \domain \SUBSET \union \true \false
%
%    These are written as in
%
%       \INCLUDE Foo \AS Bar
%
%    not as "\INCLUDE\ Foo".
%
%    The following commands are used to introduce space:
%        \s{1.2}     A 1.2em horizontal space
%        \vs{1.2}    A 1.2em vertical space, made either with a vertical strut 
%                    extending 1.2em below the line, or a \vspace{1.2em}, 
%                    depending on whether used in outer par mode or not.
%        \V{1.2}     Equivalent to \\[1.2em] (which can't be used in math
%                    mode in TLA mode).
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% \tlamathcodes
%% \notlamathcodes
%%   The \tlamathcodes command makes all letters in math mode come
%%   from the text italic font (family 4) rather than the usual math
%%   italic family.  Thus $Word$ is just an italic word, not a
%%   weird math formula.  Useful when math symbols are mostly
%%   multiletter. \notlamathcodes resets to normal.
%%
\newcommand{\tlamathcodes}{%
\mathcode`a="7461%
\mathcode`b="7462%
\mathcode`c="7463%
\mathcode`d="7464%
\mathcode`e="7465%
\mathcode`f="7466%
\mathcode`g="7467%
\mathcode`h="7468%
\mathcode`i="7469%
\mathcode`j="746A%
\mathcode`k="746B%
\mathcode`l="746C%
\mathcode`m="746D%
\mathcode`n="746E%
\mathcode`o="746F%
\mathcode`p="7470%
\mathcode`q="7471%
\mathcode`r="7472%
\mathcode`s="7473%
\mathcode`t="7474%
\mathcode`u="7475%
\mathcode`v="7476%
\mathcode`w="7477%
\mathcode`x="7478%
\mathcode`y="7479%
\mathcode`z="747A%
\mathcode`A="7441%
\mathcode`B="7442%
\mathcode`C="7443%
\mathcode`D="7444%
\mathcode`E="7445%
\mathcode`F="7446%
\mathcode`G="7447%
\mathcode`H="7448%
\mathcode`I="7449%
\mathcode`J="744A%
\mathcode`K="744B%
\mathcode`L="744C%
\mathcode`M="744D%
\mathcode`N="744E%
\mathcode`O="744F%
\mathcode`P="7450%
\mathcode`Q="7451%
\mathcode`R="7452%
\mathcode`S="7453%
\mathcode`T="7454%
\mathcode`U="7455%
\mathcode`V="7456%
\mathcode`W="7457%
\mathcode`X="7458%
\mathcode`Y="7459%
\mathcode`Z="745A}

\newcommand{\notlamathcodes}{%
\mathcode`a="7161%
\mathcode`b="7162%
\mathcode`c="7163%
\mathcode`d="7164%
\mathcode`e="7165%
\mathcode`f="7166%
\mathcode`g="7167%
\mathcode`h="7168%
\mathcode`i="7169%
\mathcode`j="716A%
\mathcode`k="716B%
\mathcode`l="716C%
\mathcode`m="716D%
\mathcode`n="716E%
\mathcode`o="716F%
\mathcode`p="7170%
\mathcode`q="7171%
\mathcode`r="7172%
\mathcode`s="7173%
\mathcode`t="7174%
\mathcode`u="7175%
\mathcode`v="7176%
\mathcode`w="7177%
\mathcode`x="7178%
\mathcode`y="7179%
\mathcode`z="717A%
\mathcode`A="7141%
\mathcode`B="7142%
\mathcode`C="7143%
\mathcode`D="7144%
\mathcode`E="7145%
\mathcode`F="7146%
\mathcode`G="7147%
\mathcode`H="7148%
\mathcode`I="7149%
\mathcode`J="714A%
\mathcode`K="714B%
\mathcode`L="714C%
\mathcode`M="714D%
\mathcode`N="714E%
\mathcode`O="714F%
\mathcode`P="7150%
\mathcode`Q="7151%
\mathcode`R="7152%
\mathcode`S="7153%
\mathcode`T="7154%
\mathcode`U="7155%
\mathcode`V="7156%
\mathcode`W="7157%
\mathcode`X="7158%
\mathcode`Y="7159%
\mathcode`Z="715A}

%% Redefine Math Mode commands to use \tla@everymath
%%
%%  (Can't use \everymath because $ apparently gives next character its 
%%  catcode before executing \everymath)

\def\tla@math{\relax\ifmmode $\else $\tla@everymath\fi}
\let\@begmath\(
\let\@begdispmath\[
\def\tla@everymath{}  %% initialization

\catcode`$\active
\let$\tla@math
\def\({\@begmath\tla@everymath}
\def\[{\@begdispmath\tla@everymath}


%% \tlachars 
%% \notlachars 
%%    Sets / unsets the catcodes of the following characters to active
%%    :  [  =  <  -  /  |  #  "  _   ! 

\begingroup
\catcode`#12\relax
\gdef\tlachars{%
\catcode`:=\active\relax%     :
\catcode`[=\active\relax%     [
\catcode`=\active\relax%      =
\catcode`<=\active\relax%     <
\catcode`>=\active\relax%     >
\catcode`"=\active\relax%     "
\catcode`_=\active\relax%     _
\catcode`|=\active\relax%     |
\catcode`/=\active\relax%     /
\catcode`!=\active\relax%     !
\catcode`-=\active\relax%     -
\catcode`#=\active\relax%    #
}      
\endgroup

\begingroup
\gdef\notlachars{%
\catcode`:=12\relax%     :
\catcode`[=12\relax%     [
\catcode`=12\relax%      =
\catcode`<=12\relax%     <
\catcode`>=12\relax%     >
\catcode`"=12\relax%     "
\catcode`_=12\relax%     _
\catcode`!=12\relax%     !
\catcode`/=12\relax%     /
\catcode`|=12\relax%     |
\catcode`-=12\relax%     -
\catcode`##=12\relax%    #
}      
\endgroup


%%%%  The following definitions are made with TLA catcodes activated
%%%%  and with "." catcoded to mean "#"
%

 \newif\if@tlamode
 \@tlamodetrue

\begingroup
\catcode`?6\relax
\tlachars


%%% \tlaletactive : \let's the active characters to the right things
%%%

\gdef\tlaletactive{%
\let:\tla@colon%    :
\let[\tla@lb%       [
\let=\tla@eq%       =
\let<\tla@lt%       <
\let>\tla@gt%       >
\let"\tla@quote%    "
\let_\tla@under%    _
\let!\tla@bang%     !
\let/\tla@slash%    /
\let|\tla@vert%     |
\let-\tla@minus%    -
\let#\tla@hash%    #
}

%% :
\gdef\tla@colon{\@nsifnextchar{\:}{\ensuremath{\,\backslash}}{\tla@colonx}}
\gdef\tla@cmdcolon?1:{\ensuremath{\csname ?1\endcsname}}


%% =   Makes == : \deq
\gdef\tla@eq{\@nsifnextchar{=}{\tla@eqx}{\tla@eqy}}
\gdef\tla@eqx={\ensuremath{\;\;\deq\;\;}}
\gdef\tla@eqy{\@nsifnextchar{>}{\tla@eqz}{\tla@realeq}}
\gdef\tla@eqz>{\ensuremath{\Rightarrow}}

%% <   makes <> : \Diamond
%%           << : \langle
%%           <- : \leftarrow
\gdef\tla@lt{\@nsifnextchar{<}{\tla@ltx}{\tla@lty}}
\gdef\tla@ltx<{\ensuremath{\langle\@tthin}}
\gdef\tla@lty{\@nsifnextchar{>}{\tla@ltz}{\tla@ltw}}
\gdef\tla@ltz>{\ensuremath{\Diamond}}
\gdef\tla@ltw{\@nsifnextchar{-}{\tla@ltu}{\tla@reallt}}
\gdef\tla@ltu-{\ensuremath{\leftarrow}}

%% > makes >> : \rangle
\gdef\tla@gt{\@nsifnextchar{>}{\tla@gtx}{\tla@realgt}}
\gdef\tla@gtx>{\ensuremath{\@tthin\rangle}}

%% "
\gdef\tla@quote?1"{\mbox{\rm``{\sf ?1}''}}

%% -  makes ->   
\gdef\tla@minus{\@nsifnextchar{>}{\tla@minusx}{\tla@realminus}}
\gdef\tla@minusx>{\ensuremath{\rightarrow}}

%% _
\gdef\tla@under{\@nsifnextchar{_}{\tla@spaceunder}{\tla@underx}}
\gdef\tla@underx{\@nsifnextchar{.}{\tla@undery}{\tla@subscript}}
\gdef\tla@undery.{\,}
\gdef\tla@spaceunder_{\hspace*{\tla@indentspace}%
                        \@nsifnextchar{_}{\tla@spaceunder}{}}

%% |   produces |-  : \vdash
%%              |-> : \mapsto
%%              |=  : \models
\gdef\tla@vert{\@nsifnextchar{-}{\tla@vertx}{\tla@verty}}
\gdef\tla@vertx-{\@nsifnextchar{>}{\tla@vertw}{\ensuremath{\vdash}}}
\gdef\tla@verty{\@nsifnextchar{=}{\tla@vertz}{\tla@realvert}}
\gdef\tla@vertz={\ensuremath{\models}}
\gdef\tla@vertw>{\ensuremath{\mapsto}}

%% ~  produces ~  : \lnot
%%             ~> : \leadsto
\gdef\tla@tilde{\@nsifnextchar{>}{\tla@tildex}{\tla@tildey}}
\gdef\tla@tildex>{\ensuremath{\leadsto}}
\gdef\tla@tildey{\ensuremath{\lnot}}
\endgroup

%%%%%%%%%%%%%%%%%%%%%%%%  end of active characters  %%%%%%%%%%%%%%%%%


%% \optional
\newcommand{\xtla}{\begingroup \notlachars \@xtla}
\newcommand{\@xtla}[1]{#1\endgroup}


%% :
%% \coloncommands
%% \nocoloncommands
%%    Declarations that enable or disable the interpreting of :...: as 
%%    commands in TLA mode. However, :\: is always interpreted as \backslash
%%    in TLA mode.  The default is \coloncommands.
\newcommand{\coloncommands}{%
  \def\tla@colonx{\@ifspace{\tla@realcolon}{\tla@cmdcolon}}}
\newcommand{\nocoloncommands}{\def\tla@colonx{\tla@realcolon}}

\coloncommands  %% THE DEFAULT
\def\tla@realcolon{\ifmmode \,:\,\else{\rm :}\fi}

%% [   makes [] : \Box       %%% must be changed if ] is made active
\def\tla@lb{\@nsifnextchar{]}{\tla@lbx}{[}}
\def\tla@lbx]{\ensuremath{\Box}}

%% =   
\def\tla@realeq{=}

%% <
\def\tla@reallt{\ensuremath{<}}

%% >
\def\tla@realgt{\ensuremath{>}}

%% !
\def\tla@bang{\ensuremath{\@tthin!\@tthin}}

%% /
\def\tla@slash{\@nsifnextchar{\ }{\tla@slashx}{/}}
\def\tla@slashx\ {\ensuremath{\land}}

%% -
\def\tla@realminus{-}

%%_
\def\tla@subscript#1{\ensuremath{\mbox{}_{#1}}}

%% |
\def\tla@realvert{\ensuremath{|}}



%% # produces \neq
\def\tla@hash{\ensuremath{\neq}}


%% \tla ==  Make characters active;
%%          
\def\tla{\@tlamodetrue
          \def\tla@everymath{%
                \tlamathcodes
                \tlachars
                \tlaletactive
                \def\/{\lor}%
                \let~\tla@tilde}%
          \tlaletactive\ifmmode\tla@everymath\fi}

\def\notla{\def\tla@everymath{}%
  \@tlamodefalse
  \notlamathcodes
  \def\/{\@italcor}%
  \let~\@realtilde
  \notlachars}



%%% MISCELLANY
%% \ensuremath: the LaTeX2e command
%
\def\ensuremath#1{\relax\ifmmode #1\else $#1$\fi}

% \@italcor = normal \/
% \@realtilde = normal ~
\let\@italcor\/ %%%%% \/ redefined to \or
\let\@realtilde~

% SPACING
%
% \@tthin : a math-mode space 1/2 the width of \,
%
\def\@tthin{\mskip.5\thinmuskip}
\def\indentspace#1{\def\tla@indentspace{#1}}
\indentspace{1em}


% \@ifspace{A}{B} executes A if the next token is a space token,
% else it executes B and replaces next token.
%
% \@nsifnextchar like \@ifnextchar, except it doesn't skip over
% space tokens.

\def\@ifspace#1#2{\def\@tempa{#1}\def\@tempb{#2}\futurelet\@tempc\@ifspacex}
\def\@ifspacex{\ifx\@sptoken\@tempc\let\@tempd\@tempa\else
     \let\@tempd\@tempb\fi\@tempd}

\def\@nsifnextchar#1#2#3{\let\@tempe #1\def\@tempa{#2}\def\@tempb{#3}\futurelet
    \@tempc\@ifnsnch}
\def\@ifnsnch{\ifx \@tempc \@tempe\let\@tempd\@tempa\else\let\@tempd\@tempb\fi
      \@tempd}

%%%%%%%%%%%%%%%%%%%%%%%%%%%% MATH SYMBOLS %%%%%%%%%%%%%%%%%%%
%
\newcommand{\deq}{\mathrel{\stackrel{\scriptscriptstyle\mathchar"7001}{=}}}
\def\A{\forall\,}
\def\E{\exists\,}
\newcommand{\EE}{\makebox{$\raisebox{.05em}{\makebox
   [0pt][l]{$\exists\s{-.517}\exists\s{-.517}\exists$}}\exists\s{-.517}\exists
            \s{-.517}\exists\,$}}
\renewcommand{\AA}{\makebox{$\raisebox{.05em}{\makebox
   [0pt][l]{$\forall\s{-.517}\forall\s{-.517}\forall$}}\forall\s{-.517}\forall
            \s{-.517}\forall\,$}}
\newcommand{\X}{\ensuremath{\times}}

%%%%%%%%%%%%%%%% INITIALZE

%%%%%%%%%%% LOAD pf.sty %%%%%%%%%%%%%%%
%\typeout{Loading llncspf style}
%\input{llncspf.sty}

% llncspf.sty
%
% last modified on Fri Oct 14 15:54:36 PDT 1994 by lamport

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                       THE pf STYLE                          %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%  CONTENTS
%    1. Introduction
%    2. The Basic Commands
%    3. Different Styles of Numbering 
%    4. Indentation
%    5. Assumptions
%    6. Portions of a Proof
%    7. Conjunctions and Disjunctions
%    8. Miscellany
%    9. List of all Commands and Environments
%
%  1. INTRODUCTION
%
%    The pf style provides commands and environments for typesetting
%    hierarchically structured proofs.  Below is an example of what 
%    such a proof looks like, and the commands that generate it.
%    The commands are explained individually below.  Then
%
%    THE OUTPUT                         THE INPUT
%    ~~~~~~~~~~                         ~~~~~~~~~
%    Any text...                        Any text
%                                       \begin{proof}
%    1. Text of step 1.                   \step{label-1}{Text of step 1.}
%                                         \begin{proof}
%       1.1. Text of step.                  \step{label-1.1}{Text of step}
%                                            \begin{proof}
%            Proof: Paragraph                  \pf\ Paragraph proof.~\qed
%            proof. []                       \end{proof}
%                                      
%       1.2. Text of step.                   \step{label-1.2}{Text of step.}
%                                            \begin{proof}
%            Proof: Paragraph                  \pf\ Paragraph proof.~\qed
%            proof. []                       \end{proof}
%
%       1.3. QED                             \qedstep
%                                            \begin{proof}
%            1.3.1. Text of step               \step{label-1.3.1}{Text...}
%                   Proof: ... []              \begin{proof} ... \end{proof}
%                                            
%            1.3.2. QED                        \qedstep
%                   Proof: ...                 \begin{proof}...\end{proof}
%                                            \end{proof}
%                                         \end{proof}
%
%    2. Text of step 2.                   \step{label-2}{Text of step 2.}
%        Proof: ...                        \begin{proof} \pf\ ... \end{proof}
%
%    3. QED                               \qedstep
%       Proof: ...                        \begin{proof} \pf\ ... \end{proof}
%     
%
%   The best way to read such proofs is hierarchically.  To find out
%   how, search below for the \pfhidelevel command and the \hideqedproof
%   command.
%
%
% 2. THE BASIC COMMANDS
%
% The proof Environment:
%   Increments the proof depth, and indents the enclosed text the
%   appropriate amount.  For example, if the proof environment follows a
%   \step command that produces step number 2.6.7, then the first \step
%   command inside the environment will produce step number 2.6.7.1.
%
% \step{LABEL}{TEXT}
%    This command produces a proof step such as
%        2.6.7.1. TEXT
%    The step number 2.6.7.1 is determined by the position of the \step
%    command in the proof.  The LABEL is a symbol label used to refer to the
%    step number.  A subsequent \stepref{LABEL} command will generate the
%    step number 2.6.7.1.  The same LABEL may be re-used, but
%    not in a context where it is legal to refer to a previous step with the
%    same label.  (See the discussion of step numbering below.)
%    
%    This command is equivalent to
%           \begin{step+}{LABEL}
%              TEXT
%           \end{step+}
%    The step+ environment form is more convenient if TEXT is long or
%    complicated.
%
% \qedstep
%    This command produces something like
%    
%       2.6.7.5. QED
%    
%    If the proof of step 2.6.7 is a sequence of steps (rather than a
%    paragraph proof), then the last step in its proof is normally of this
%    form.  The "QED" in the statement simply denotes the current
%    goal---what must be proved to prove step 2.6.7.  The proof of this QED
%    step will be followed immediately by the
%    \end{proof} command that ends the proof of step 2.6.7.
%    
%    The pf style does not enforce this method of structuring proofs;
%    the proof of statement 2.6.7 could end with an ordinary \step
%    command.
%
% \pf, \qed
%    These are simple text-producing commands that normally begin and end a
%    paragraph-style proof.  However, they are not required.  Remember to
%    put a "\ " after the \pf command, and to tie the \qed command to the
%    last word of the proof with a "~".
%
% \pfsketch
%    
%    An intuitive prook sketch often introduces a multi-step proof, as in
%    
%         1.3. All odd numbers are prime.
%              Proof sketch:  The proof is by induction, with the
%              base case proved in step 1 and the induction step in
%              step 2.
%              1.3.1. The number 1 is a prime.
%                     Proof: ...
%              1.3.2. If n is an odd prime, then n+2 is prime.
%                     Proof: ...
%              1.3.3. QED
%                     Proof: 1.3.1, 1.3.2, and mathematical induction.
%    
%    This is entered as 
%    
%      \step{label-1.3}{All odd numbers  are prime}
%      \begin{proof}
%      \pfsketch\ The proof is by induction...
%       \step{label-1.3.2}{The number 1 is a prime}
%       ...
%      \end{proof}
%    
%    The \pfsketch command is, like \pf, just produces the text.  It isn't
%    required by the pf style.
%    
%
%  3. DIFFERENT STYLES OF NUMBERING 
%
%    In the long style of proof numbering, a step number is something like
%    2.6.7.5, meaning that it is the fifth step in the proof of statement
%    2.6.7, which is the seventh step in the proof of statement 2.6, which
%    is...  Statement 2.6.7.5 has the short name <4>5, meaning it is the
%    fifth statement in the current level-4 proof.  Numbering style is
%    controlled by the commands
%    
%      \pfshortnumbers{N} : Use short step numbers for all levels
%                           >= N (Default is N = 1, using only short
%                           numbers.
%    
%    These are local declarations that obey the usual scoping rules.  Thus,
%    putting a \pfshortnumbers declarations right after a \begin{proof}
%    command causes all steps in that proof to have short numbers.
%
%    Steps 2.6.7.5, 2.6.6.5, and 4.9.1.5 all have the same short numbers
%    <4>5.  However, no ambiguity arises from the use of short numbers
%    because at most one of these steps can be mentioned at any point in a
%    proof.  Let the ANCESTORS of step 2.6.7.5 be steps 2.6.7, 2.6, and 2.
%    Let the ELDER SIBLINGS of step 2.6.7.5 be steps 2.6.7.1, 2.6.7.2,
%    2.6.7.3, and 2.6.7.4.  The proof statement 2.6.7.5 may refer only
%    to steps in the following two sets:
%       (i) The elder siblings of itself and of its ancestors.
%      (ii) Itself and its ancestors.
%    The steps in (i) are the previously-proved assertions that can be used
%    in the proof of 2.6.7.5.  The assumptions of the steps in (ii) are the
%    ones that are being assumed in the proof.  (Assumptions are discussed
%    below.)
%    
%    The command \stepref{LABEL} anywhere in the proof of step 2.6.7.5 (or in
%    the step itself) produces the step number of a step lying in sets (i)
%    or (ii) having LABEL as its label (the first argument of its \step
%    command).  An error message is generated if the \step command has a
%    label that is the label of a step in set (i) or (ii).
%    
%    Note that the last step of a proof is never an elder sibling, so it
%    can't be in the set (i) for any statement.  A QED-step has no
%    assumptions, so it can't be in the set (ii) for any statement.  That is
%    why the \qedstep command does not specify a label.  Actually, \qedstep
%    is defined to equal \label{qedstepN}{...}, where N is the current
%.   level number. Thus, an error will be generated if two \qedstep commands 
%    occur in the same proof, since they will have the same labels.

%
%    Short step numbers are really nice.  They take up less space and are
%    easier to read.  They are the preferred form for long proofs.  However,
%    long step numbers are better for referring to a proof step from outside
%    the proof.  The pf style allows you to print the long numbers of steps as
%    marginal notes, something like
%    
%       Theorem:  ...
%       ...
%     2.4.5.6.         <4>6. All odd numbers greater than 2 are prime.
%     2.4.5.6.1.             <5>1. The number 3 is prime.
%       ...
%    
%    (The long numbers are printed in a smaller font, so it looks
%    better than you'd guess from this.)  The relevant commands are:
%    
%    \pfsidenumbers{N}{D} 
%       Print side numbers for proof steps of all levels \geq N, left-aligned 
%       a distance D to the left of the left margin of the text.
%    
%    \pfnosidenumbers  
%       Do not print side numbers (the default)
%
%
%  4. INDENTATION
%
%    There are two styles of indentation:
%    
%       Long Style 
%          1. XXXXX
%             1.1. XXXXX
%                  1.1.1. XXXXX
%                         1.1.1.1. XXXX
%                                  Proof: ...
%    
%       Short Style 
%          1. XXXXX
%            1.1. XXXXX
%              1.1.1. XXXXX
%                1.1.1.1. XXXX
%                  Proof: ...
%    
%    In the long style, the proof of a statement lines up with the text of
%    the statement.  In the short form, each level is indented the same
%    distance from the next higher level.  The relevant declarations
%    are
%    
%    \pflongindent 
%       Indent proofs to full width of item label
%    
%    \pfshortindent 
%       Indent proofs by the length parameter \pfindent (the default)
%
%
%  5. ASSUMPTIONS
%
%    A common form of a step is 
%        
%          <4>5. Assume: 1. n is an odd number
%                        2. n > 2
%                Prove:  n is prime 
%    
%    This asserts that the Prove clause follows from the Assume clause.  The
%    "QED" at the end of the proof of this step refers to the Prove clause.
%    The input to produce this is
%    
%        \step{label-4.5}{
%          \assume{\begin{enumerate}
%                    \item $n$ is an odd number
%                    \item $n>2$
%                  \end{enumumerate}}
%          \prove{$n$ is prime}}
%    
%    The relevant command syntax is
%    
%       \assume{TEXT}
%       \prove{TEXT}
%    
%    The formatting of the enumerate environment is changed to work
%    propertly inside a proof environment.  (It is actually redefined
%    to be the pfenum environment, described far below.)  Note that
%    \label and \ref command for subitem b of item 3 produces the label
%    "3b".  Note: there is an enumerate* environment that is like
%    enumerate, except it indents the items.
%     
%    
%    Another form of assumption is a Case assumption.  The statement
%    
%          <5>1. Case: n is of the form 4n+1
%    
%    means
%    
%          <5>1. Assume: n is of the form 4n+1
%                Prove:  QED
%    
%    where QED is the current goal.  A proof by cases is structured
%    as follows
%    
%          <4>5. Assume: 1. n is an odd number
%                        2. n > 2
%                Prove:  n is prime 
%    
%               <5>1. Assume: n equals 4m+1 for some m
%                     Prove:  QED
%                     Proof:  ... []
%    
%               <5>2. Assume: n equals 4m+3 for some m
%                     Prove:  QED
%                     Proof: ... []
%    
%               <5>3. QED
%                     Proof: By <5>1, <5>2, and assumption <4>.2 (which 
%                     states that n is odd), since any odd number has
%                     the form 4m+1 or 4m+3. []
%    
%    A case assumption is produced with a \case command, which works like
%    \assume and \prove.  It has the syntax
%    
%        \case{TEXT}
%    
%    Corresponding to the \assume, \prove, and \case commands are
%    the assume+, prove+, and case+ environments.  For example, \prove{TEXT}
%    is equivalent to \begin{prove+} TEXT \end{prove+}
%    
%    Note the reference, in the proof of <5>3, to the second conjunct of the
%    Assume clause in statement <4>5 as "assumption <4>.2".  Since a proof
%    of a step can only use assumptions in that step or its ancestors, a
%    level number suffices to identify an assumption.  The Assume clause of
%    statement <4>5 is called "assumption <4>".  The ".2" refers to the
%    second item in that clause.  As mentioned below, this use of ".2" to
%    refer to the second component of a conjunction can be used 
%    in other circumstances as well.
%    
%    When long numbering is used, assumptions must be referred to by the
%    name of the statement containing the assumption.  Thus, "assumption
%    2.6.7.5.2" could potentially mean either the Assume clause of statement
%    2.6.7.5.2, or the second item in the Assume clause of 2.6.7.5.  One way
%    to remove the ambiguity is to use something other than "." in long step
%    numbers.  The possibilities 2:6:7:5 and 2-6-7-5 don't look too good;
%    the best alternative to "." seems to be a raised period ($\cdot$).  The
%    "." is changed by redefining \pfdot, as described below.  Assumptions
%    are referred to with the following commands:
%    
%       \levelref{LABEL}
%         If \stepref{LABEL} produces <4>5, then \levelref{label} 
%         produces <4>.
%         If \stepref{LABEL} produces 2.6.7.5, then \levelref{label} also 
%         produces 2.6.7.5.
%
%       \toplevel
%         If \stepref{LABEL} produces <4>5, then \toplevel
%         produces "<0>".
%         If \stepref{LABEL} produces 2.6.7.5, then \toplevel
%         produces "0".
%
%
%  6. PORTIONS OF A PROOF
%
%    You may want to format only part of a proof--for example, you might
%    want to write the proof of statement 2.1.3 as a separate proof.  You'd
%    want something like
%    
%    2.1.3. All odd numbers are prime.
%           2.1.3.1. ...
%    
%    To do this, first imagine the shortest proof you can that has a
%    statement numbered 2.1.3: 
%    
%        1. X
%        2. X
%           2.1. X
%                2.1.1. X
%                2.1.2. X
%                2.1.3. All odd numbers are prime.
%                       2.1.3.1. ...
%    
%    Write this using the \step command and prove environment.  Now, change
%    every \step{LABEL}{X} command to \nostep{LABEL}, and change the proof
%    environments surrounding the proofs of steps 2 and 2.1 by noproof
%    environments.  This yields
%    
%        \begin{proof}
%          \nostep{label-1}
%          \nostep{label-2}
%          \begin{noproof}
%            \nostep{label-2.1}
%            \begin{noproof}
%              \nostep{label-2.1.1}
%              \nostep{label-2.1.2}
%        
%               \step{label-2.1.3} All oddnumbers are prime
%               \begin{proof}
%                  \step{label-2.1.3.1} ...
%               \end{proof}
%              \end{noproof}
%            \end{noproof}
%        \end{proof}
%    
%    which produces the desired result.  Note that the labels of the \nostep
%    commands can be used to refer to the corresponding step numbers.
%
%  7. CONJUNCTIONS AND DISJUNCTIONS
%
%    It is very convenient to write conjunctions as lists bulleted by \land.
%    This is done with the conj environment, where
%    
%     $X =  \begin{conj}    PRODUCES    X =  /\ A
%             A \\ B \\ C                    /\ B
%           \end{conj}$                      /\ C
%
%    The conj* environment is similar, except it numbers the conjuncts.
%    
%     $X = \begin{conj*}    PRODUCES    X = 1./\ A
%            A \\ B \\ C                    2./\ B
%          \end{conj*}$                     3./\ C
%
%    If X is defined in this way, then X.2 denotes the formula B.
%
%    The disj and disj* environments are similar. Disjuncts
%    are numbered a, b, c 
%
%    These environments are implemented with the array environment.
%    They should nest properly.  They can be used only in math mode.
%
%
%  8. MISCELLANY
%
%    \pfhidelevel{N} : A counter that controls what levels of proof
%        are shown.  The command \setcounter{pfhidelevel}{2} causes
%        only level-1 and level-2 steps to be printed, and the proofs
%        of level-2 steps (including all level-3 and higher steps)
%        to be omitted.  The default value of the counter is very large.
%        The value of the counter should always be positive.
%
%   \unhideqedproof 
%   \hideqedproof   : Used in conjunction with the pfhidelevel counter.
%        The \unhideqedproof command causes one extra level of proof 
%        to be displayed for the lowest level \qedstep.  The \hideqedproof
%        returns to the default of not showing this extra level.
%       
%    \pflet  : like \prove and \assume, but with keyword "Let"
%
%    \kwfont : Selects the font for the keywords "Proof", "Assume",
%              "Prove", and "Case".  Default is \sc; you can 
%              change it by something like \renewcommand{\kwfont}{\em}
%
%    \pfdot : Defines the "." in long step numbers.  Try
%             \renewcommand{\pfdot}{\mbox{$\cdot$}} for variety.
%
%    \pfindent : The amount by which proof levels are indented in
%                the short indent option.  Changed with \setlength.
%                This is a local declaration.
%
%    \pfstepnumber{LEVEL}{NUMBER}{LONGNUMBER} :
%        Generates either <LEVEL>NUMBER or LONGNUMBER, depending
%        on the numbering style in effect.
%
%    \pflevelnumber{LEVEL}{LONGNUMBER} :
%        Generates either <LEVEL> or LONGNUMBER, depending
%        on the numbering style in effect.
%
%    The following parameters control vertical spacing.  
%    
%      \pftopsep  : space above first proof environment
%      \pfbotsep  : space below first proof environment
%      \pfsep     : space above and below inner proof environment
%      \stepsep   : space above and below proof step
%    
%    The last two are set to zero, and probably should remain there.  It
%    might be desirable to have vertical spacing depend more finely on the
%    level number.  This can be done using the \makefcn command (see far
%    below), and will be if there seems to be a need.  However,
%    zero extra vertical spacing seems to be fine.
%
%    \pf, \qed, \pfsketch  :  Described above.  Can be changed with 
%                             \renewcommand
%
%
%  9. LIST OF ALL COMMANDS AND ENVIRONMENTS
%
%    Text-Producting Commands            Environments
%      \pf, \pfsketch                      proof
%      \qed                                noproof
%      \step                               step+   [version of \step]        
%      \nostep                             assume+ [version of \assume]
%      \qedstep                            prove+  [version of \prove]        
%      \assume                             case+   [version of \case]        
%      \prove                              conj, conj*
%      \pflet                              disj, disj*
%      \case                               pfenum, enumerate*
%      \pfdot ["." in long names]          
%      \stepref, \levelref, \toplevel
%      \pfstepnumber, \pflevelnumber
%      
%    Declarations
%      \kwfont [keyword font]
%      \pfshortnumbers
%      \pfsidenumbers, \pfnosidenumbers
%      \pflongindent, \pfshortindent
%      \pfindent
%      \pftopsep, \pfbotsep  
%      \pfsep, \stepsep   


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                       SPACING                               %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% COMMANDS
%   \pflongindent == Indent proofs to full width of item label
%   \pfshortindent == Indent proofs by \pfindent [the default]

\newif\if@pfLongIndent %  true if indent proof to width of label.
\@pfLongIndentfalse
\newcommand{\pflongindent}{\@pfLongIndenttrue}
\newcommand{\pfshortindent}{\@pfLongIndentfalse}

% PARAMETERS
%  \pfindent   == indentation at beginning of a proof
%  \pftopsep   == space above first proof environment
%  \pfbotsep   == space below first proof environment
%  \pfsep      == space above and below inner proof environment
%  \stepsep    == space above and below proof step
%  pfhidelevel == counter, specifying level at which proofs are hidden

\newlength{\pfindent}      
\newlength{\pftopsep}  
\newlength{\pfbotsep}  
\newlength{\pfsep}  
\newlength{\stepsep}        
\newbox{\pfbox}
\newcounter{pfhidelevel}
\setcounter{pfhidelevel}{9999}
\newcommand{\pfhidelevel}[1]{\setcounter{pfhidelevel}{#1}}

\setlength{\pfindent}{1em} 
\setlength{\pftopsep}{1ex}     % space above first proof environment
\setlength{\pfbotsep}{1ex}     % space below first proof environment
\setlength{\pfsep}{0pt}        % space above and below inner proof environment
\setlength{\stepsep}{0pt}      % space above and below proof step

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                   STEP NUMBERING                            %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% COMMANDS
%   \pfshortnumbers{N} == Use short step numbers for all levels >= N
%
%   \pfsidenumbers{N}{D} == print side numbers for proof steps of all
%                           levels >= N, left-aligned length D 
%                           to left of left margin
%   \pfnosidenumbers     == do not print side numbers (the default)

%\newcommand{\pflongnumbers}{\@pfLongNumberstrue}
\newcommand{\pfshortnumbers}[1]{\pfshortNumberLevel=#1\relax}

\newcount\pfshortNumberLevel \pfshortNumberLevel=0

% \@pfLongNumbersfalse}
% \newif\if@pfLongNumbers %  true if indent proof to width of label.
%\@pfLongNumbersfalse

\newcommand{\pfstepnumber}[3]{%
   \ifnum \pfLevelCount < \pfshortNumberLevel
       #3%
     \else $\langle#1\rangle#2$%
   \fi}

\newcommand{\pflevelnumber}[2]{%
   \ifnum \pfLevelCount < \pfshortNumberLevel
       #2%
     \else $\langle#1\rangle$%
   \fi}

\newif\if@pfSideNumbers %  true if putting long numbers at margin
\@pfSideNumbersfalse
\newcounter{pf@sidenumberdepth}
\newlength{\pf@sidenumberoutdent}
\newcommand{\pfsidenumbers}[2]{\@pfSideNumberstrue
     \setcounter{pf@sidenumberdepth}{#1}%
     \addtocounter{pf@sidenumberdepth}{-1}%
     \setlength{\pf@sidenumberoutdent}{#2}}
\newcommand{\pfnosidenumbers}{\@pfSideNumbersfalse}


\newcount\pfLevelCount  \pfLevelCount=0 % current level number
\newcount\pfStepCount   \pfStepCount=0  % current step number
\newcommand{\pfLongLevel}{} % The long version of current level--e.g., 2.7.5
\newcommand{\pfLongStep}{}  % The long version of current step--e.g., 2.7.5.2
\newcommand{\pfStepName}{}  % {current level name}{current step name} 

% \pfSetName ==  LongStep := current long step name
%                StepName := current step name
\newcommand{\pfSetName}{%
  \edef\pfLongStep{%
    \ifnum\pfLevelCount>\@ne
      \pfLongLevel\pfdot\the\pfStepCount
     \else\the\pfStepCount\fi}%
  \edef\pfStepName{%
   \ifnum \pfLevelCount < \pfshortNumberLevel
    {\pfLongStep}{\pfLongStep}%
    \else
     {$\langle\the\pfLevelCount\rangle$}%
     {$\langle\the\pfLevelCount\rangle\the\pfStepCount$}%
   \fi}}

% \pfSetRef{foo} ==  IF \pf@foo UNDEFINED
%                       THEN \pf@foo := StepName 
%                       ELSE WARNING
\newcommand{\pfSetRef}[1]{%
  \@ifundefined{pf@#1}%
    {\expandafter
      \edef\csname pf@#1\endcsname{\pfStepName}}%
    {\typeout{WARNING:
         proof step "#1" (<\the\pfLevelCount>\the\pfStepCount) 
        already defined}}%
    }


\newcommand{\pfPrintStepNumber}[2]{#2}
\newcommand{\pfPrintLevelNumber}[2]{#1}

% \stepref{FOO} == Print \pf@FOO as a step number
\newcommand{\stepref}[1]{\@ifundefined{pf@#1}{{\bf ??}\typeout{WARNING:
 proof step "#1" undefined}}{\expandafter\expandafter\expandafter
 \pfPrintStepNumber\csname pf@#1\endcsname}}

\newcommand{\levelref}[1]{\@ifundefined{pf@#1}{{\bf ??}\typeout{WARNING:
 proof step #1 undefined}}%
  {\expandafter\expandafter\expandafter
 \pfPrintLevelNumber\csname pf@#1\endcsname}}

\newcommand{\toplevel}{\pflevelnumber{0}{0}}

\newlength{\pf@outdent}
\newcommand{\pfSideNumber}{%
  \if@pfSideNumbers 
   \ifnum\pfLevelCount>\value{pf@sidenumberdepth}%
    \hspace*{-\pf@outdent}%
    \makebox[0pt][l]{\footnotesize\pfLongStep}%
    \hspace*{\pf@outdent}%
    \else\fi
   \else\fi}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                   THE pflist ENVIRONMENT                    %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%% The pflist environment is the same as list environment except 
%% it can be nested deeper.

\def\pflist#1#2{\ifnum \@listdepth >15\relax \@toodeep 
     \else \global\advance\@listdepth\@ne \fi
  \rightmargin \z@ \listparindent\z@ \itemindent\z@
  \csname @list\romannumeral\the\@listdepth\endcsname 
  \def\@itemlabel{#1}\let\makelabel\@mklab \@nmbrlistfalse #2\relax
  \@trivlist
  \parskip\parsep \parindent\listparindent
  \advance\linewidth -\rightmargin \advance\linewidth -\leftmargin
  \advance\@totalleftmargin \leftmargin
  \parshape \@ne \@totalleftmargin \linewidth 
  \ignorespaces}

\def\endpflist{\global\advance\@listdepth\m@ne
    \endtrivlist}

\let\@listvii=\@listv
\let\@listviii=\@listv
\let\@listix=\@listv
\let\@listx=\@listv
\let\@listxi=\@listv
\let\@listxii=\@listv
\let\@listxiii=\@listv
\let\@listxiv=\@listv
\let\@listxv=\@listv
\let\@listxvi=\@listv

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                   THE proof ENVIRONMENT                     %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%

\renewenvironment{proof}{%       BEGIN:
  \edef\pfLongLevel          % LongLevel := 
   {\ifnum\pfLevelCount>\z@  %    IF LevelCount > 0
     \ifnum\pfLevelCount>\@ne%     THEN IF LevelCount > 1
      \pfLongLevel\pfdot\else\fi  %            THEN LongLevel * "." FI
      \the\pfStepCount       %          * StepCount
     \else\fi}%              %     ELSE FI
  \advance\pfLevelCount\@ne  %   LevelCount := LevelCount + 1
  \@tempcnta=\value{pfhidelevel}%
  \ifnum\@tempcnta<\@ne
    \setcounter{pfhidelevel}{1}%
    \typeout{WARNING: pfhidelevel < 1, setting to 1}%
    \@tempcnta=\@ne\fi
  \advance\@tempcnta\@ne
  \if@qedstep
    \advance\@tempcnta\@ne
    \ifnum\pfLevelCount 
        = \@tempcnta 
     \sbox{\pfbox}\bgroup\begin{minipage}{\textwidth}\fi
  \else     
   \ifnum\pfLevelCount 
        = \@tempcnta 
     \sbox{\pfbox}\bgroup\begin{minipage}{\textwidth}\fi\fi
  \pfStepCount=\z@           %   StepCount  := 0
  \ifnum\pfLevelCount>\@ne   %   IF LevelCount > 1
   \begin{pflist}{}{%          %     THEN Begin List with
    \topsep=\pfsep\relax     %           \topsep     := \pfsep
    \itemsep=\z@             %           \itemsep    := 0
    \parsep=\z@              %           \parsep     := 0
    \partopsep=\z@           %           \partopsep  := 0
    \if@pfLongIndent         %          IF LongIndent
     \settowidth{\leftmargin}%%           THEN
      {\expandafter          %              \leftmargin := width of step name
       \pfPrintStepNumber    %                             + \labelsep
       \pfStepName.}%
     \advance\leftmargin
     \labelsep 
    \else                    %           ELSE
    \leftmargin=\pfindent    %            \leftmargin := \pfindent
    \fi\relax        
   }   \item[]
   \else \par                %     ELSE \par
    \addvspace{\pftopsep}%   %          addvspace of \pftopsep
    \parindent=\z@           %          \parindent := 0
    \parskip = \z@           %          \parskip := 0
    \@ifundefined{mathindent}{%
      \abovedisplayskip=\z@ plus .2ex       % set display skips
      \abovedisplayshortskip=\z@ plus .2ex
      \belowdisplayskip=\z@ plus .2ex
      \belowdisplayshortskip=\z@ plus .2ex}{%
      \mathindent=1em}%
    \let\enumerate\pfenum       %   enumerate environment <- pfenum
    \let\endenumerate\endpfenum %
 \fi
\@qedstepfalse
    }%                       % END:
  {\ifnum\pfLevelCount>\@ne  %   IF LevelCount > 1
    \end{pflist}%              %     THEN End List
   \else \par                %     ELSE \par
     \addvspace{\pfbotsep}%  %          addvspace of \pfbotsep
   \fi
  \@tempcnta=\value{pfhidelevel}%
  \advance\@tempcnta\@ne
  \if@qedstep
    \advance\@tempcnta\@ne
    \ifnum\pfLevelCount 
        = \@tempcnta 
     \end{minipage}\egroup\sbox{\pfbox}{}\@qedstepfalse\fi
  \else 
      \ifnum\pfLevelCount 
        =\@tempcnta 
        \end{minipage} 
        \egroup\sbox{\pfbox}{}\fi
 \fi}


\newenvironment{noproof}{%   % BEGIN:
  \edef\pfLongLevel          % LongLevel := 
   {\ifnum\pfLevelCount>\z@  %    IF LevelCount > 0
     \ifnum\pfLevelCount>\@ne%     THEN IF LevelCount > 1
      \pfLongLevel.\else\fi  %            THEN LongLevel * "." FI
      \the\pfStepCount       %          * StepCount
     \else\fi}%              %     ELSE FI
  \advance\pfLevelCount\@ne  %   LevelCount := LevelCount + 1
  \pfStepCount=\z@           %   StepCount  := 0
  \par                       %   \par
  \parindent=\z@             %          \parindent := 0
  \parskip = \z@             %          \parskip := 0
  \@ifundefined{mathindent}{%
      \abovedisplayskip=\z@ plus .2ex       % set display skips
      \abovedisplayshortskip=\z@ plus .2ex
      \belowdisplayskip=\z@ plus .2ex
      \belowdisplayshortskip=\z@ plus .2ex}{%
      \mathindent=1em}%
  \let\enumerate\pfenum       %   enumerate environment <- pfenum
  \let\endenumerate\endpfenum %
  }%                         % END:
  {\par}                     %  \par

%% step 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                     \step, \assume, ETC.                    %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
\newcommand{\step}[2]{\begin{step+}{#1}#2\end{step+}}
\newif\if@qedstep %  true right after a \qedstep if in the scope of an 
                  %  \unhideqedproof declaration
\@qedstepfalse

\newif\if@unhideqedstep % set true by \unhideqproof, false by \hideqproof. 

\@unhideqedstepfalse
\newcommand{\unhideqedproof}{\@unhideqedsteptrue}
\newcommand{\hideqedproof}{\@unhideqedstepfalse}

\newcommand{\qedstep}{\step{qedstep\the\pfLevelCount}{Q.E.D.}
\if@unhideqedstep\@qedsteptrue\fi}

\newcommand{\nostep}[1]{% 
  \advance\pfStepCount\@ne       % StepCount := StepCount + 1
  \pfSetName                     % SetName
  \pfSetRef{#1}%                 % SetRef
  }

\newenvironment{step+}[1]%
 {\endgroup                      % Move Outside environment scope
  \advance\pfStepCount\@ne       % StepCount := StepCount + 1
  \pfSetName                     % SetName
  \pfSetRef{#1}%                 % SetRef
 \begingroup\@endpefalse         % Move inside environment scope
   \def\@currenvir{step+}%       %   by simulating \begin{step+}
 \begin{pflist}{}{%                % Begin list environment with
   \setlength
     {\pf@outdent}{\textwidth}%  %   \pf@outdent = outdent
   \addtolength                  %                 for side numbers
    {\pf@outdent}{-\linewidth}%  
   \addtolength
    {\pf@outdent}%
    {\pf@sidenumberoutdent}%
   \topsep=\stepsep\relax        %   \topsep     := \stepsep
   \itemsep=\z@                  %   \itemsep    := 0
   \parsep=\z@                   %   \parsep     := 0
   \partopsep=\z@                %   \partopsep  := 0
   \settowidth{\labelwidth}%     %   \labelwidth := width of step name.
     {\expandafter
      \pfPrintStepNumber
      \pfStepName.}%
   \leftmargin=\labelwidth\relax %   \leftmargin := \labelwidth
   \advance\leftmargin\labelsep %                   + \labelsep
   \relax}%
 \item[\pfSideNumber%               % \item[ \pfSideNumber
  \expandafter                       %        StepNumber]
  \pfPrintStepNumber\pfStepName.]}%
 {\end{pflist}}

%%%%% \assume, \prove, and \case commands

\newenvironment{assume+}{%
 \begin{pflist}{}{%                % Begin list environment with
   \topsep=\z@                   %   \topsep     := 0
   \itemsep=\z@                  %   \itemsep    := 0
   \parsep=\z@                   %   \parsep     := 0
   \partopsep=\z@                %   \partopsep  := 0
   \settowidth{\labelwidth}%     %   \labelwidth := width "Assume:"
     {{\kwfont Assume\/}:}%
   \leftmargin=\labelwidth\relax %   \leftmargin := \labelwidth
   \advance\leftmargin\labelsep  %                   + \labelsep
   \relax}%
 \item[{\kwfont Assume\/}:]}%    % \item[Assume:]]
 {\end{pflist}}

\newcommand{\assume}[1]{\begin{assume+}#1\end{assume+}}

\newcommand{\prove}[1]{\begin{prove+}#1\end{prove+}}
\newenvironment{prove+}{%
 \begin{pflist}{}{%                % Begin list environment with
   \topsep=\z@                   %   \topsep     := 0
   \itemsep=\z@                  %   \itemsep    := 0
   \parsep=\z@                   %   \parsep     := 0
   \partopsep=\z@                %   \partopsep  := 0
   \settowidth{\labelwidth}%     %   \labelwidth := width "Assume:"
     {{\kwfont Assume\/}:}%
   \leftmargin=\labelwidth\relax %   \leftmargin := \labelwidth
   \advance\leftmargin\labelsep  %                   + \labelsep
   \relax}%
 \item[{\kwfont 
          Prove\/}:\hfill]}%     % \item[Prove:]]
 {\end{pflist}}

\newcommand{\pflet}[1]{\begin{pflet+}#1\end{pflet+}}
\newenvironment{pflet+}{%
 \begin{pflist}{}{%                % Begin list environment with
   \topsep=\z@                   %   \topsep     := 0
   \itemsep=\z@                  %   \itemsep    := 0
   \parsep=\z@                   %   \parsep     := 0
   \partopsep=\z@                %   \partopsep  := 0
   \settowidth{\labelwidth}%     %   \labelwidth := width "Assume:"
     {{\kwfont Let\/}:}%
   \leftmargin=\labelwidth\relax %   \leftmargin := \labelwidth
   \advance\leftmargin\labelsep  %                   + \labelsep
   \relax}%
 \item[{\kwfont 
          Let\/}:\hfill]}%     % \item[Let:]]
 {\end{pflist}}

%\newcommand{\prove}[1]{%
% \begin{pflist}{}{%                % Begin list environment with
%   \topsep=\z@                   %   \topsep     := 0
%   \itemsep=\z@                  %   \itemsep    := 0
%   \parsep=\z@                   %   \parsep     := 0
%   \partopsep=\z@                %   \partopsep  := 0
%   \settowidth{\labelwidth}%     %   \labelwidth := width "Assume:"
%     {{\kwfont Assume\/}:}%
%   \leftmargin=\labelwidth\relax %   \leftmargin := \labelwidth
%   \advance\leftmargin\labelsep  %                   + \labelsep
%   \relax}%
% \item[{\kwfont Prove\/}:\hfill]     % \item[Prove:]]
% #1
% \end{pflist}}

\newcommand{\case}[1]{%
 \begin{pflist}{}{%                % Begin list environment with
   \topsep=\z@                   %   \topsep     := 0
   \itemsep=\z@                  %   \itemsep    := 0
   \parsep=\z@                   %   \parsep     := 0
   \partopsep=\z@                %   \partopsep  := 0
   \settowidth{\labelwidth}%     %   \labelwidth := width "Case:"
     {{\kwfont Case\/}:}%
   \leftmargin=\labelwidth\relax %   \leftmargin := \labelwidth
   \advance\leftmargin\labelsep  %                   + \labelsep
   \relax}%
 \item[{\kwfont
           Case\/}:]             % \item[Case:]]
 #1
 \end{pflist}}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                       MISCELLANY                            %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
\newcommand{\pf}{{\kwfont Proof\/}:}
\newcommand{\pfsketch}{{\kwfont Proof sketch\/}:}
%\newcommand{\qed}{\rule{.4em}{1.75ex}}
\renewcommand{\qed}{{\fboxsep=\z@\fbox{\rule{.5em}{0pt}\rule{0pt}{2ex}}}}
\let\kwfont=\sc
\def\pfdot{.}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                        STACKS                               %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% \@push{\stack}{element}  == \stack := <<element>> :o: \stack
% \@pop{\stack}{\cmd}  == \cmd := head(\stack)
%                            \stack := tail(\stack)
% \newstack{\stack}  == \stack := emptystack
%
% \@head{\stack}{\var}  ==  \var := head(\stack)
%   Note: to push a counter value, use \the\value{ctr}
%         to push a length \foo, use \the\foo

%
\def\@push#1#2{{\let\@nil\relax\let\@elt\relax\xdef#1{#2\@elt#1}}}
\def\@pop#1#2{{\let\@nil\relax\let\@elt\relax
              \xdef#2{\expandafter\@innerhead#1}
              \xdef#1{\expandafter\@innerpop#1}}}
\def\@innerpop#1\@elt#2\@nil{#2\@nil}
\def\@head#1#2{{\let\@elt\relax\xdef#2{\expandafter\@innerhead#1}}}
\def\@innerhead#1\@elt#2\@nil{#1}
\def\newstack#1{\gdef#1{\@nil}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%           LISTS OF CONJUNCTIONS AND DISJUNCTIONS            %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%    \begin{conj}       ->   /\ A
%      A \\ B \\ C           /\ B
%    \end{conj}              /\ C
%
%    \begin{conj*}      ->   1./\ A
%      A \\ B \\ C           2./\ B
%    \end{conj*}             3./\ C
%
%    The disj and disj* environments are similar. Disjuncts
%    are numbered a, b, c 
%
%    These environments are arrays; they must be used in math mode.

\newcounter{pf@conjCounter}   % counter for conj* and disj*
\newstack\pf@conj             % stack of counters

\newenvironment{conj}{%
 \begin{array}[t]{@{\land\;}l@{}}%
 }{%
 \end{array}}

\newenvironment{disj}{%
 \begin{array}[t]{@{\lor\;}l@{}}%
 }{%
 \end{array}}

\newenvironment{conj*}{%
 \@push\pf@conj{\the\value{pf@conjCounter}}%
 \setcounter{pf@conjCounter}{0}%
 \begin{array}[t]{@{\addtocounter{pf@conjCounter}{1}%
   \mbox{\protect\small\protect\arabic{pf@conjCounter}.}
   \land\;}l@{}}%
 }{%
 \end{array}%
 \@pop\pf@conj\pf@temp
  \setcounter{pf@conjCounter}{\pf@temp}}

\newenvironment{disj*}{%
 \@push\pf@conj{\the\value{pf@conjCounter}}%
 \setcounter{pf@conjCounter}{0}%
 \begin{array}[t]{@{\addtocounter{pf@conjCounter}{1}%
   \mbox{\protect\small\protect\alph{pf@conjCounter}.}
   \lor\;}l@{}}%
 }{%
 \end{array}%
 \@pop\pf@conj\pf@temp
  \setcounter{pf@conjCounter}{\pf@temp}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                      ENUMERATED LISTS                       %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% pfenum environment : In proofs, the enumerate environment 
%                      is redefined to be the pfenum environment
%
% enumerate* environment : Like pfenum, except with additional
%                          indentation.
%
% \enumindent :  The indentation for enumerate*
% pfenumdepth  : Depth of current pfenum list
% pfenum       : pfenum list counter
%
% Uses counters pfenumi, ... , pfenumiii just like the
% ordinary enumerate environment uses counters enumi, ... , enumiv.
% \pf@setEnumWidth{\cmd} : Sets \cmd to the width of the label of the
%                          item number 2 for the current enumeration level.
%
% \pf@enumLabel : prints the current pfenum label, using the
%                 pfenumi... counter.

\newcounter{pfenum}
\newcounter{pfenumdepth}
\newlength{\enumindent}
\setlength{\enumindent}{1em}

\@definecounter{pfenumi}
\@definecounter{pfenumii}
\@definecounter{pfenumiii}
%\@definecounter{pfenumiv}

\def\labelpfenumi{\thepfenumi.}    
\def\thepfenumi{\arabic{pfenumi}}     
 
\def\labelpfenumii{(\thepfenumii)}
\def\thepfenumii{\alph{pfenumii}}
\def\p@pfenumii{\thepfenumi}

\def\labelpfenumiii{\thepfenumiii.}
\def\thepfenumiii{\roman{pfenumiii}}
\def\p@pfenumiii{\thepfenumi\thepfenumii}

%\def\labelpfenumiv{\thepfenumiv.}
%\def\thepfenumiv{\Alph{pfenumiv}}     
%\def\p@pfenumiv{\p@pfenumiii\thepfenumiii}


\newcommand{\pf@setEnumWidth}[1]{%
  \settowidth{#1}{\setcounter{\@pfenumctr}{2}%
  \csname the\@pfenumctr\endcsname.%
  \setcounter{\@pfenumctr}{0}}}



\newcommand{\pf@enumLabel}{%
  \hfill\makebox[0pt][r]{\csname the\@pfenumctr\endcsname.}}

\newenvironment{pfenum}{%        % BEGIN
  \ifnum \value{pfenumdepth}>2%  %  IF pfenumdepth > 2
    \relax\@toodeep \else        %    THEN error
  \addtocounter{pfenumdepth}{1}% %    ELSE  pfenumdepth := pfenumdepth + 1
  \edef\@pfenumctr{pfenum%           %          @pfenumctr  := pfenumN
    \romannumeral\the            %            where N = Roman(pfenumdepth)
    \value{pfenumdepth}}%        %
   \fi                           %  FI
  \begin{pflist}%                  %   Begin list environment with
  {\pf@enumLabel}{%              %    Default label = pf@enumlabel
   \labelsep=                    %   \labelsep =
    \ifcase\value{pfenumdepth}   %     CASE OF pfenumdepth
      \labelsep                  %        
     \or .67\labelsep            %       1 -> .67\labelsep
     \or .67\labelsep            %       2 -> .67\labelsep
     \else \labelsep             %      >2 -> \labelsep
     \fi                         %
   \topsep=\z@                   %    \topsep     := 0
   \itemsep=\z@                  %    \itemsep    := 0
   \parsep=\z@                   %    \parsep     := 0
   \partopsep=\z@                %    \partopsep  := 0
   \pf@setEnumWidth\labelwidth   %    set \labelwidth with setEnumWidth
   \leftmargin=\labelwidth\relax %    \leftmargin := \labelwidth
   \advance\leftmargin\labelsep  %                   + \labelsep
   \relax
   \usecounter{\@pfenumctr}%       %    counter @pfenumctr
 }%
 }{%                             % END
   \end{pflist}%                   %   End list
   \addtocounter{pfenumdepth}{-1}%   pfenumdepth := pfenumdepth - 1
 }

\newenvironment{enumerate*}{%    % BEGIN
  \ifnum \value{pfenumdepth}>2%  %  IF pfenumdepth > 2
    \relax\@toodeep \else        %    THEN error
  \addtocounter{pfenumdepth}{1}% %    ELSE  pfenumdepth := pfenumdepth + 1
  \edef\@pfenumctr{pfenum%           %          @pfenumctr  := pfenumN
    \romannumeral\the            %            where N = Roman(pfenumdepth)
    \value{pfenumdepth}}%        %
   \fi                           %  FI
  \begin{pflist}%                  %   Begin list environment with
  {\pf@enumLabel}{%              %    Default label = pf@enumlabel
   \labelsep=                    %   \labelsep =
    \ifcase\value{pfenumdepth}   %     CASE OF pfenumdepth
      \labelsep                  %        
     \or .67\labelsep            %       1 -> .67\labelsep
     \or .67\labelsep            %       2 -> .67\labelsep
     \else \labelsep             %      >2 -> \labelsep
     \fi                         %
   \topsep=\z@                   %    \topsep     := 0
   \itemsep=\z@                  %    \itemsep    := 0
   \parsep=\z@                   %    \parsep     := 0
   \partopsep=\z@                %    \partopsep  := 0
   \pf@setEnumWidth\labelwidth   %    set \labelwidth with setEnumWidth
   \leftmargin=\labelwidth\relax %    \leftmargin := \labelwidth
   \advance\leftmargin\labelsep  %                   + \labelsep
   \advance\leftmargin\enumindent%                   + \enumindent
   \relax
   \usecounter{\@pfenumctr}%       %    counter @pfenumctr
 }%
 }{%                             % END
   \end{pflist}%                   %   End list
   \addtocounter{pfenumdepth}{-1}%   pfenumdepth := pfenumdepth - 1
 }

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                        FUNCTIONS                            %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% \makefcn{\FOO}{V0}{{V1}...{Vk}} :
%      Defines \FOO{n}  ==  CASE  n = 0    -> V0
%                                 n = 1    -> V1
%                                 ...
%                                 n \geq k -> Vk
%
%      Useful when Vi is a dimension applying to a depth-i environment

\def\makefcn#1#2#3{{\let\or\relax
     \gdef\fcn@temp{}%
     \gdef\fcn@tempb{#2}%
     \@tfor\foo:=#3\do{\xdef\fcn@temp{\fcn@temp\or\foo}\xdef\fcn@tempb{\foo}}%
     \let\ifcase\relax\let\else\relax\let\fi\relax
     \xdef#1##1{\ifcase ##1 #2\fcn@temp\else\fcn@tempb\fi}}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                        FUNCTIONS                            %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% \pfif{A}{B}{C} :  if A then B    \pfIF{A}{B}{C} :  if A
%                        else C                        THEN B
%                                                      ELSE C

\newcommand{\pfmathdef}[1]{\relax\ifmmode #1\else $#1$\fi}
\newcommand{\pfif}[3]{{\pfmathdef{%
 \begin{array}[t]{@{}l@{\;\;}l@{\;\;}l@{}}
   {\bf if}\;\;#1&{\bf then}&#2\\
                 &{\bf else}&#3
   \end{array}}}}

\newcommand{\pfIF}[3]{{\pfmathdef{%
 \begin{array}[t]{@{}l@{\;\;}l@{}}
   {\bf if}\;\;#1\\ 
  \begin{array}[t]{@{\hspace{1em}}l@{\;\;}l@{}}
     {\bf then}&#2\\
     {\bf else}&#3
   \end{array}
  \end{array}}}}


\tla


% Redefine conj and disj to leave more space, and \pf to remove
% \/.

\renewenvironment{conj}{%
 \begin{array}[t]{@{\land\ }l@{}}%
 }{%
 \end{array}}

\renewenvironment{disj}{%
 \begin{array}[t]{@{\lor\ }l@{}}%
 }{%
 \end{array}}

\renewenvironment{conj*}{%
 \@push\pf@conj{\the\value{pf@conjCounter}}%
 \setcounter{pf@conjCounter}{0}%
 \begin{array}[t]{@{\addtocounter{pf@conjCounter}{1}%
   \mbox{\protect\small\protect\arabic{pf@conjCounter}.}
   \land\ }l@{}}%
 }{%
 \end{array}%
 \@pop\pf@conj\pf@temp
  \setcounter{pf@conjCounter}{\pf@temp}}

\renewenvironment{disj*}{%
 \@push\pf@conj{\the\value{pf@conjCounter}}%
 \setcounter{pf@conjCounter}{0}%
 \begin{array}[t]{@{\addtocounter{pf@conjCounter}{1}%
   \mbox{\protect\small\protect\alph{pf@conjCounter}.}
   \lor\ }l@{}}%
 }{%
 \end{array}%
 \@pop\pf@conj\pf@temp
  \setcounter{pf@conjCounter}{\pf@temp}}

\renewcommand{\pf}{{\kwfont Proof\@italcor}:}

%%%%%%%%%%%%% redefine some pf.sty commands with $ having its normal definition
\begingroup
\catcode`$3\relax

\gdef\pfstepnumber#1#2#3{%
   \ifnum \pfLevelCount < \pfshortNumberLevel
       #3%
     \else $\langle#1\rangle#2$%
   \fi}

\gdef\pflevelnumber#1#2{%
   \ifnum \pfLevelCount < \pfshortNumberLevel
       #2%
     \else $\langle#1\rangle$%
   \fi}

\gdef\pfSetName{%
  \edef\pfLongStep{%
    \ifnum\pfLevelCount>\@ne
      \pfLongLevel\pfdot\the\pfStepCount
     \else\the\pfStepCount\fi}%
  \edef\pfStepName{%
   \ifnum \pfLevelCount < \pfshortNumberLevel
    {\pfLongStep}{\pfLongStep}%
    \else
     {$\langle\the\pfLevelCount\rangle$}%
     {$\langle\the\pfLevelCount\rangle\the\pfStepCount$}%
   \fi}}
\endgroup

%% Redefine \step, \assume, \prove, \pflet, and \case  so their arguments
%% have characters made active.

\let\tla@stepy\step
\renewcommand{\step}[1]{\begingroup\if@tlamode\tlachars\fi\tla@stepx{#1}}
\def\tla@stepx#1#2{\endgroup\tla@stepy{#1}{#2}}

\let\tla@assumey\assume
\renewcommand{\assume}{\begingroup\if@tlamode\tlachars\fi\tla@assumex}
\newcommand{\tla@assumex}[1]{\endgroup\tla@assumey{#1}}

\let\tla@provey\prove
\renewcommand{\prove}{\begingroup\if@tlamode\tlachars\fi\tla@provex}
\newcommand{\tla@provex}[1]{\endgroup\tla@provey{#1}}

\let\tla@casey\case
\renewcommand{\case}{\begingroup\if@tlamode\tlachars\fi\tla@casex}
\newcommand{\tla@casex}[1]{\endgroup\tla@casey{#1}}

\let\tla@pflety\pflet
\renewcommand{\pflet}{\begingroup\if@tlamode\tlachars\fi\tla@pfletx}
\newcommand{\tla@pfletx}[1]{\endgroup\tla@pflety{#1}}


%%%%%%%%%%%%%%  Module formatting commands

%%%% noj, if/then/else %%%%%%%%%%%%%%%%%%
\def\IF#1{\begin{array}[t]{@{}l@{}l@{}l@{}}%
            \@ifnextchar{\\}%
              {\makebox[.6em][l]{{\bf if\, }$#1$}}{\mbox{{\bf if }$#1$ }}}
\def\THEN{&\mbox{\bf \,then }&\begin{array}[t]{@{}l@{}}}
\def\ELSE{\end{array}\\ &\mbox{\bf \,else }&\begin{array}[t]{@{}l@{}}}
\def\FI{\end{array}\end{array}}

\newenvironment{noj}{\begin{array}[t]{@{}l@{}}}{\end{array}}
\newenvironment{noj2}{\begin{array}[t]{@{}l@{\;\;}l@{}}}{\end{array}}
\newenvironment{noj3}{\begin{array}[t]{@{}l@{\;\;}l@{\;\;}l@{}}}{\end{array}}
\newenvironment{noj4}%
  {\begin{array}[t]{@{}l@{\;\;}l@{\;\;}l@{\;\;}l@{}}}{\end{array}}

%\newenvironment{noj}{\begin{array}[t]{@{}l@{}}}%
%                    {\end{array}}


%%%% let %%%%%%%%
\newcommand{\LET}{\begin{array}[t]{@{}l@{\;\;}l@{}} {\bf let}% 
                              &\begin{array}[t]{@{}l@{}}} 
\newcommand{\IN}{\end{array}\\{\bf in}&\begin{array}[t]{@{}l@{}}}
\newcommand{\NI}{\end{array}\end{array}}

%%%% case %%%
\newcommand{\CASE}{{\bf case\ }}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%    
%                  COMMANDS FROM spec92.sty                      %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%    
\newlength{\@charwidth}
\settowidth{\@charwidth}{{\small\tt M}}
\newlength{\boxrulewd}\setlength{\boxrulewd}{.4pt}
\newlength{\boxindent}\setlength{\boxindent}{22\@charwidth}
\newlength{\boxlineht}\setlength{\boxlineht}{.5\baselineskip}
\newcommand{\boxsep}{\@charwidth}
\newlength{\boxruleht}
\newlength{\boxruledp}
\newcommand{\@computerule}{%
  \setlength{\boxruleht}{.5ex}%
  \setlength{\boxruledp}{-\boxruleht}%
  \addtolength{\boxruledp}{\boxrulewd}}
\newcommand{\boxrule}{\leaders\hrule height \boxruleht depth \boxruledp
                      \hfill\mbox{}}

\newcommand{\@nmlineraise}{\if@botline -\boxrulewd
    \else-\boxlineht\fi}
\newcommand{\nameline}[1]{\hspace*{-\boxsep}%
    \raisebox{\@nmlineraise}[0pt][0pt]{\rule[.5ex]{\boxrulewd
               }{\boxlineht}}%
    \boxrule
    #1\boxrule
    \raisebox{\@nmlineraise}[0pt][0pt]{\rule[.5ex]{\boxrulewd
               }{\boxlineht}}\hspace{-\boxsep}\vspace{.5\baselineskip}}
\newif\if@botline

%%%%%%%%%%%%%%%%%%END COMMANDS FROM spec92.sty %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\newenvironment{module}[1]{\begin{trivlist}\flushleft\@computerule
            \item[]\tlanameline{\ {\bf module} {\it #1\@italcor} }\par\it
            \catcode`_=\active\relax
        }{\par\tlabotline\end{trivlist}}


\newenvironment{submodule}[1]{\par
        \vspace{-.5em}%%%%%%%%%%%  space at top of submodule
    \begin{list}{}{%
       \leftmargin=1em%
       \labelwidth=0pt%
       \labelsep=0pt%
       \parsep=0pt%
       \topsep=0pt%
       \partopsep=0pt%
       \itemsep=0pt}\flushleft\@computerule
            \item[]\tlanameline{\ {\bf module} {\it #1\@italcor} }\par
        }{\par\tlabotline\end{list}}


\newcommand{\tlanameline}[1]{\hspace*{-\boxsep}%
    \raisebox{\@nmlineraise}[0pt][0pt]{\rule[.5ex]{\boxrulewd
               }{\boxlineht}}%
    \boxrule
    #1\boxrule
    \raisebox{\@nmlineraise}[0pt][0pt]{\rule[.5ex]{\boxrulewd
               }{\boxlineht}}\hspace{-\boxsep}%
          \vspace{.2em}%%% EXTRA SPACE BELOW TOP LINE OF MODULE
               }

%%%%% Fix to \midline and \botline from spec92

\newcommand{\midbar}{\par\hspace{-\boxsep}%
    \raisebox{-.5\boxlineht}[0pt][0pt]{\rule[.5ex]{\boxrulewd
               }{\boxlineht}}%
     \boxrule
    \raisebox{-.5\boxlineht}[0pt][0pt]{\rule[.5ex]{\boxrulewd
               }{\boxlineht}}\hspace{-\boxsep}%
         \vspace{-.2em}%%% SPACE BELOW \midbar
                \par}

\newcommand{\tlabotline}{\hspace{-\boxsep}%
    \raisebox{-\boxrulewd}[0pt][0pt]{\rule[.5ex]{\boxrulewd
               }{\boxlineht}}%
     \boxrule
    \raisebox{-\boxrulewd}[0pt][0pt]{\rule[.5ex]{\boxrulewd
               }{\boxlineht}}\hspace{-\boxsep}\vspace{0pt}}

\newcommand{\xtrivlist}{\begin{list}{}{%
       \leftmargin=1em%
       \labelwidth=0pt%
       \labelsep=0pt%
       \parsep=0pt%
       \topsep=0pt%     
       \partopsep=0pt%
       \itemsep=0pt}}
\def\endxtrivlist{\end{list}}

\let\@@startfield\@startfield
\let\@@stopfield\@stopfield

%% need to change \@tabcr because its look-ahead at the next
%  character causes that character to be prematurely cat-coded.
%
\def\tla@tabcr{\@stopline\@startline\ignorespaces}

\def\xtabbing{\lineskip \z@\let\>\@rtab\let\<\@ltab\let\=\@settab
     \def\@startfield{\@@startfield\(}
     \def\@stopfield{\)\@@stopfield}
     \let\+\@tabplus
     \let\-\@tabminus
     \let\`\@tabrj\let\'\@tablab
     \let\\=\tla@tabcr
     \global\@hightab\@firsttab
     \global\@nxttabmar\@firsttab
     \dimen\@firsttab\@totalleftmargin
     \global\@tabpush0 \global\@rjfieldfalse
     \xtrivlist \item[]\if@minipage\else\vskip\parskip\fi
     \setbox\@tabfbox\hbox{\rlap{\indent\hskip\@totalleftmargin
       \the\everypar}}\def\@itemfudge{\box\@tabfbox}\@startline\ignorespaces}

\def\endxtabbing{\@stopline\ifnum\@tabpush > 0 \@badpoptabs \fi\endxtrivlist}

\newenvironment{decls}[1]{\par
      \addvspace{.4em}%%%  EXTRA SPACE ABOVE decls ENVIRONMENT
{\bf #1}\begin{xtabbing}%
  \hspace{1em}\=\+\kill}{\end{xtabbing}}

\newenvironment{nodecls}{\par
      \addvspace{.4em}%%%  EXTRA SPACE ABOVE nodecls ENVIRONMENT
\begin{xtabbing}}{\end{xtabbing}}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%% KEYWORDS %%%%%%%%%%%%%%%%%%
%
\newcommand{\tlacomment}{\begingroup\tlachars\@comment}
%\newcommand{\@tlacomment}[1]{\endgroup\mbox{\footnotesize\rm #1}}
\newcommand{\comment}{\begingroup\notlachars\@comment}
\newcommand{\@comment}[1]{\endgroup
    \raisebox{0pt}[0pt][0pt]{\footnotesize\rm %
       \begin{tabular}[t]{@{}l@{}}#1\end{tabular}}}
%\newcommand{\@comment}[1]{\endgroup
%    \mbox{\footnotesize\rm \raisebox{0pt}[0pt][0pt]{%
%       \begin{tabular}[t]{@{}l@{}}#1\end{tabular}}}}
\newcommand{\variable}{\mbox{\sc variable}}
\newcommand{\action}{\mbox{\sc action}}
\newcommand{\statefcn}{\mbox{\sc state fcn}}
\newcommand{\IMPORT}{{\bf import }}
\newcommand{\EXPORT}{{\bf export }}
\newcommand{\INCLUDE}{{\bf include }}
\newcommand{\AS}{\,{\bf as }}
\newcommand{\WITH}{\,{\bf with }}
\newcommand{\constant}{\mbox{\sc constant}}
\newcommand{\boolean}{\mbox{\sc boolean}}
\newcommand{\union}{\mbox{\sc union }}
\newcommand{\true}{\mbox{\sc true}}
\newcommand{\false}{\mbox{\sc false}}
\newcommand{\unchanged}{\mbox{\sc unchanged }}
\newcommand{\except}{\mbox{\sc\ except }}
\renewcommand{\choose}{\mbox{\sc choose }}
\newcommand{\enabled}{\mbox{\sc Enabled\s{.2}}}
\newcommand{\domain}{\mbox{\sc Domain\s{.2}}}
\newcommand{\SUBSET}{\mbox{\sc Subset\s{.2}}}
\newcommand{\WF}{\mbox{\rm WF}}
\newcommand{\SF}{\mbox{\rm SF}}

%%%%%%%%%%%%%%%%%%%%%%% SPACE COMMANDS %%%%%%%%%%%%%%%%%%%%%%
%
\newcommand{\s}{\begingroup\notlachars\tla@s}
\newcommand{\tla@s}[1]{\endgroup\hspace*{#1em}}
\newcommand{\vs}{\begingroup\notlachars\tla@vs}
\newcommand{\tla@vs}[1]{\endgroup\ifinner
                       \raisebox{-.34em}{\raisebox{-#1em}{\rule{0pt}{.1pt}}}
                      \else \vspace{#1em}\fi}
\newcommand{\V}{\begingroup\notlachars\tla@V}
\def\tla@V#1{\endgroup\vs{#1}\\}


\makeatother
\makeatletter
\def\floatpagefraction{.6}
\def\fps@figure{tbp}
\makeatother

%% NOTATION CHANGES
%%   OK    -> \OK  (defined to produce Loyal)
%%   now_0 -> Now_0
%%   For Module MidLevel: Rcv  -> Issue
%%                        Init -> LInit

\title{Specifying and Verifying \\ Fault-Tolerant Systems}
\author{Leslie Lamport and Stephan Merz}
\date{25 July 1994\\
      minor correction: 14 October 1994}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                 MODIFICATION DATE                               %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                                 %
% Defines \moddate to expand to modification date such as         %
%                                                                 %
%    Mon  5 Aug 1991  [10:34]                                     %
%                                                                 %
% and \prdate to print it in a large box.  Assumes editor         %
% updates modification date in standard SRC Gnu Emacs style.      %
% (should work for any user name).                                %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\def\ypmd{%                                                       %
%                                                                 %
%                                                                 %
       modified on Wed Jun 22 11:50:30 PDT 1994 by merz           %
  endypmd}                                                        %
%                                                                 %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\moddate}{\expandafter\xpmd\ypmd}                     %
\def\xpmd Last modified                                           %
on #1 #2 #3 #4:#5:#6 #7 #8 by #9 endypmd{#1 \ #3 #2 #8 \ [#4:#5]} %
\newcommand{\prdate}{\noindent\fbox{\Large\moddate}}              %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                  llncs STYLE STUFF                             %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\institute{Digital Equipment
       Corporation, Systems Research Center}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                           EMACS MACROS                         %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%&b&{\bf #}&
%&s&\str{#}&
%&r&\expref{#}&
%&l&\explabel{#}&
%&"&"#"&


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                  NOTATION FOR SPECS IN THIS DOCUMENT           %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\?}{\_\!\_}
\newcommand{\oo}{\infty}
\renewcommand{\O}{\circ}
\newcommand{\OK}{Loyal}
\renewcommand{\qed}{}          % remove the Halmos bars from proofs.
\newcommand{\implies}{\Rightarrow}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                      MISCELLANEOUS COMMANDS                    %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%

% \rightcomment{foo} :
%    For use inside a decls/nodecls environment.  Makes comment
%    "foo" flushed right and raised.

\newcommand{\rightcomment}[1]{\`{\notla\raisebox
            {1.2ex}[0pt]{\makebox[0pt][r]{\comment{#1}}}}}
% \TLA+ == TLA^+
\def\TLA+{\mbox{TLA$^{+}$}}
% \str{foo} == "foo"
\newcommand{\str}[1]{\mbox{\rm``{\sf #1}''}}

% \explabel{foo} : Makes boxed marginal number, assigning that number to 
%                  label "foo".
% \expref{foo}   : Makes boxed superscript of number defined by label "foo".
%
\setlength{\fboxsep}{1pt}
\newcounter{explanation}
\renewcommand{\theexplanation}{\arabic{explanation}}
\newcommand{\explabel}[1]{{\refstepcounter{explanation}%
%%%%
%%%%%%%%% UNCOMMENT THE FOLLOWING LINE TO HELP FIND "MOVED MARGINPAR'S".
%%%%
%   \typeout{Explanatory note \theexplanation.}%
\label{#1}}%
  \marginpar[\mbox{}\hfill\fbox{\small\theexplanation}]{\fbox{\small\theexplanation}}}
\newcommand{\expref}[1]{\ensuremath{^{\fbox{\tiny\ref{#1}\s{-.05}}}}}

\newenvironment{describe}[1]%
   {\begin{list}{}{\settowidth{\labelwidth}{#1}%
            \setlength{\leftmargin}{\labelwidth}% 
            \addtolength{\leftmargin}{\labelsep}%
            \def\makelabel##1{\rm ##1\hfill}}}%
   {\end{list}}

%\newcommand{\suggest}[2]{  % suggested changes: print old version below
%  \begin{noj}
%  #1 \\ 
%  \fbox{\comment{original: #2}}
%  \end{noj}
%}

\newcommand{\suggest}[2]{#1}

\begin{document}
%try
 \thispagestyle{empty}
 \mbox{}
 \vfill
 \begin{center}
 \LARGE
 \bf Specifying and Verifying \\ Fault-Tolerant Systems

 \large

 \vspace{1.5\baselineskip}
   \begin{tabular}[t]{r}
     Leslie Lamport \\[-2pt]
    {\small\tt lamport@src.dec.com}
   \end{tabular}
   \ and \
  \begin{tabular}[t]{l}
    Stephan Merz\\[-2pt]
   {\small\tt merz@src.dec.com}
  \end{tabular}
\\[3mm]
   {\small Digital Equipment Corporation}\\[-.2em]
   {\small Systems Research Center}\\[-.2em]
   

\vspace{1.5\baselineskip}
%\moddate
25 July 1994\\
minor correction: 14 October 1994

\vspace{3\baselineskip} 

%\fbox{\begin{minipage}{.75\textwidth} 
%\LARGE THIS PAGE SHOULD NOT APPEAR IN THE
%PROCEEDINGS.
%\end{minipage}}

 \end{center}
 

 \vspace{7\baselineskip} 
 
 \noindent
To appear in Proceedings of the Third International Symposium on
Formal Techniques in Real Time and Fault Tolerant Systems, held
19--23 September 1994 in L\"{u}beck, Germany.
 \vfill \vfill 
 \newpage

\setcounter{page}{1}

%try
\maketitle

\begin{abstract}
We formally specify a well known solution to the Byzantine generals
problem and give a rigorous, hierarchically structured proof of its
correctness.  We demonstrate that this is an engineering exercise,
requiring no new scientific ideas.  
\end{abstract}
%try

\section{Introduction}

Assertional verification of concurrent systems began almost twenty
years ago with the work of Ashcroft~\cite{ashcroft:proving}.  By the
early 1980's, the basic principles of formal specification and
verification of concurrent systems were
known~\cite{lam:protocol,lamport:specifying,misra:proofs}.  More
precisely, we had learned how to specify and verify those aspects of a
system that can be expressed as the correctness of an individual
execution.  Fault-tolerant systems are just one class of concurrent
systems; they require no special techniques.

The most important problems that remain are in the realm of
engineering, not science.  Scientific ideas must be translated into
engineering practice.  We describe here what we believe to be a
suitable framework for an engineering discipline of formal
specification and verification.

The limited space provided by these proceedings, and the limited time
and patience of the authors, have forced us to choose a simple
example---the specification and hierarchical verification of a well
known fault-tolerant algorithm.  Our example is OM$(1)$, the
one-traitor ``oral-message'' solution to the Byzantine generals
problem~\cite{lamport:byzantine}.  In this problem, there is a
collection of generals---a commander and a set of lieutenants---who
communicate with one another by message.  Any of the generals,
including the commander, may be a traitor.  The commander must send an
order to all the lieutenants so that (i)~all loyal lieutenants agree
on the same order $o$, and (ii)~if the commander is loyal, then $o$ is
the order that she issued.  Algorithm OM$(1)$ satisfies these
conditions if at most one of the generals is a traitor.  We augment
the traditional statement of the problem by requiring that all loyal
generals choose their order within some fixed time after the start of
the algorithm.  A solution to the Byzantine generals problem lies at
the heart of a fault-tolerant system in which faulty processors can
exhibit completely arbitrary behavior.

This algorithm was formally specified and verified in 1983, in an
appendix to a final report~\cite{neumann:highly-dependable}.  Even
then, it was considered too straightforward an exercise to be worth
writing up separately for publication.  The specification and
verification of fault-tolerant algorithms is not rocket science, but
it is still not standard engineering practice.  Most of the literature
on verification concentrates on the underlying formalism and ignores
the problem of defining a language for specifying real
systems~\cite{lam:specifying,lynch:hierarchical,manna:temporal}.  The
literature on specification languages generally ignores the problem of
reasoning formally about specifications of real
systems~\cite{hoare:csp-book,kurki-suonio:operational}.

We address these practical issues by using existing tools: a precisely
defined specification language and a hierarchical proof method.
Section~\ref{sec:spec} contains the formal specifications of the
problem and the algorithm.  There are three specifications, a
high-level problem specification, a mid-level specification of the
algorithm at roughly the level of detail provided in
\cite{lamport:byzantine}, and a low-level specification that more
realistically models message passing.  Section~\ref{sec:proofs} proves
that each specification implements the next higher-level one.  A
correctness property of the high-level specification is also proved.
Section~\ref{sec:discussion} discusses the specifications and proofs.

%try


\section{The Formal Specifications} \label{sec:spec}

Our specifications are written in \TLA+, a complete specification
language based on TLA, the Temporal Logic of Actions.  The semantics
of TLA is defined in terms of states and behaviors.  A state is an
assignment of values to variables, and a behavior is an infinite
sequence of states.  A TLA formula is interpreted as a boolean
function on behaviors.

In TLA, a system is modeled by choosing variables whose values
describe the system's state, and an execution of the system is
represented by a behavior.  The system is specified by a TLA formula
that is true of a behavior iff (if and only if) that behavior
represents a correct execution of the system.  A specification is a
mathematical formula with precisely defined semantics.  The
correspondence between the real system and the mathematical formula
lies in the interpretation of the formula's variables.  The free
variables of the specification represent the system's interface---the
part of the system that is being specified.  A description of TLA and
its proof rules can be found in~\cite{lamport:newtla}.  However, we
try to explain the meaning of the TLA formulas in our specification
well enough so they can be read with no prior knowledge of TLA\@.

Some formalisms describe systems in terms of events (often called
actions) rather than states.  An event in such a formalism corresponds
to a change to the value of an interface variable in a TLA
specification.  The basic method of writing and reasoning about
specifications is the same for event-based and state-based formalisms.


\TLA+ provides a language for writing TLA specifications.  In addition
to the operators of TLA, it contains operators for defining and
manipulating data structures and syntactic structures for handling
large specifications.  The first published description of \TLA+ was
in~\cite{lamport:hybrid}.  Since then, the following changes have been
made to the language: (i)~explicit specification of sorts is no longer
required for definitions, (ii)~the {\sc except} construct (described
below) has replaced the earlier syntax for the same operator,
(iii)~single square brackets have replaced double square brackets for
record operators.  (Record operators are not used here.)  All of these
changes preceded work on this particular example.


\setcounter{explanation}{97}

Some formulas in the specifications have been annotated with boxed
numbers, such as \expref{sampleref}\,.  A boxed number refers to the
corresponding number in the margin of the text, such as the one on
this line\explabel{sampleref}, which marks the point where the formula
is explained.  

Our specifications provide a crash course in \TLA+, since they use
almost all the basic syntactic features of the language and many of
its predefined operators.  Figures
\ref{fig:keywords}--\ref{fig:TLA+operators} at the end of this paper
list all the syntactic constructs and predefined operators of \TLA+.
Ones that are used in the specifications are annotated with pointers
to the places in the text where they are explained.


\setcounter{explanation}{0}

\subsection{The High-Level Specification} \label{sec:hi-level-spec}

The high-level specification appears in Figure~\ref{fig:hi-level}.  It
begins with a module named \explabel{module}$SpecParams$.  The
module is the basic unit of a \TLA+ specification.  It is a collection
of declarations, definitions, assumptions, and theorems.

\begin{figure}
\begin{module}{SpecParams\expref{module}}
\IMPORT FiniteSets, 
              Reals\expref{Reals} \\
   \begin{nodecls}
 {\bf parameters} \s{1}\=
      Cmdr, Lt, Order, Now_0, :Delta:\expref{SpecConstants}  : 
                  \constant \\
      \> status, ord, now\expref{SpecVariables} : \variable
   \end{nodecls}
\midbar
   \begin{nodecls}
{\bf assumption} \s{1}
      HiAssump\expref{CAssumpDef}  == 
         \begin{conj} 
            (IsFiniteSet(Lt)) /\ (Cmdr :notin: Lt)  \\
            "?" :notin: Order                      \\
            Now_0 :in: Real                         \\
            (:Delta: :in: Real) /\ (0 < :Delta:)
         \end{conj}
   \end{nodecls}
%
\midbar
%                                               
   \begin{nodecls}
     \OK(g)\s{1}\= \kill
     Gen\expref{OK}    \> == Lt \cup \{Cmdr\}\\
     \OK(g)\expref{OK}  \> == status[g] = "Loyal"
   \end{nodecls}
\end{module}

\vspace{-10pt}

\begin{module}{HiLevel}
   \IMPORT  SpecParams, Reals, RealTime 
\midbar
   \begin{nodecls}
     Choose(g)\s{1} \=\kill
     LInit(g)\expref{LSpec} \> == \begin{conj}
                           status[g] :in: \{"Loyal", "Traitor"\}\\
                           \OK(g) => (ord[g] = "?")
                        \end{conj} \\
     CInit\expref{CInit}  \> == \begin{conj}
                           status[Cmdr] :in: \{"Loyal", "Traitor"\}\\
                           \OK(Cmdr) => (ord[Cmdr] :in: Order)
                        \end{conj} \\
     Fail(g)\expref{Fail}   \> ==  status'[g] = "Traitor"   \\
     Choose(g)\expref{Choose} \> ==  
        \begin{conj}
            \OK(g)  /\ (ord[g] = "?")                      \\ 
            ord'[g] :in: Order                            \\
           :A: h :in: Gen : \OK(h)' /\ (ord'[h] # "?") => (ord'[g] = ord'[h]) \\
          \unchanged status[g]
        \end{conj} \\
%
     var(g)\expref{CInit} \> == <<ord[g], status[g]>> \\
%
      CSpec\expref{CSpec} \> == CInit /\ :Box: [Fail(Cmdr)]_{var(Cmdr)} \V{.2}
%
      LSpec(g)\expref{LSpec} \> ==                                              
         \begin{conj}
            LInit(g) /\  :Box: [Choose(g) \/ Fail(g)]_{var(g)} \V{.3}
            [](\OK(g) /\ (ord[g] = "?") => (now :leq: Now_0 + :Delta:))
         \end{conj}  \\
%
     Spec\expref{Spec} \> == 
         \begin{conj}
            CSpec \\
            :A: g :in: Lt : LSpec(g)\\
            (now = Now_0) \\ 
            RT(<<ord, status>>)
         \end{conj}
   \end{nodecls}

\begin{decls}{theorem}
% {\bf theorem} \s{1}
SpecGood\expref{SpecGood} ==  
 Spec => [] \,\= :A: g :in: Gen : \\
                  \> __\OK(g) /\ (Now_0 + :Delta: < now )\\
                  \> ___=> \begin{conj}
                             ord[g] :in: Order \\
                             :A: h :in: Gen : \OK(h) => (ord[g] = ord[h])
                           \end{conj}
\end{decls}
\end{module}
\vspace{-5pt}
\caption{The high-level specification.} \label{fig:hi-level}
\end{figure}

The {\bf import}\explabel{import} statement imports the contents of
the modules $FiniteSets$ and $Reals$.  This statement has almost the
same effect as inserting the text of these modules into module
$SpecParams$.  The only difference is that when another module imports
or includes module $SpecParams$, it does not obtain the definitions
that $SpecParams$ imported from modules $FiniteSets$ and $Reals$.

Module $FiniteSets$\explabel{Reals} defines $IsFiniteSet(S)$ to equal
\true\ iff $S$ is a finite set.  The module $Reals$ defines the set
$Real$ of real numbers, with the zero element $0$ and the usual
operators $+$, $*$, $<$, and $\leq$ on real numbers.  Our
specification can be understood without knowing precisely how these
imported operators are defined.  For the reader who wants to see the
formal definitions, we include module $FiniteSets$ without further
explanation in Figure~\ref{fig:FiniteSets}, at the end of the paper.
We omit module $Reals$.  (Starting with the predefined module $Naturals$
that defines the natural numbers, it takes fewer than fifty lines to
define the set $Real$ and all the operators on real numbers used in
our specification.)

Returning to module $SpecParams$, we next encounter a {\bf
parameters}\explabel{parameter} statement, which declares the module's
parameters.  The parameters are the free symbols of a module.  All
formulas defined in a module can be expressed in terms of its
parameters and the built-in operators of \TLA+.  There are two classes
of module parameters, constants\explabel{constant} and variables.
Constants are the rigid variables of temporal logic; they represent
quantities that are unchanged during a behavior.  Variables are the
flexible variables of temporal logic; they represent quantities that
can change during the course of a behavior.  The constant parameters
of the specification are:
\begin{describe}{$Order$}
\item[$Cmdr$] The\explabel{SpecConstants} commander.
\item[$Lt$] The set of lieutenants.
\item[$Order$] The set of all possible orders.
\item[$Now_0$] The time at which the algorithm starts.
\item[$\Delta$] The maximum length of time it can take for
      the loyal generals to decide on their values.
\end{describe}
The variable parameters are: 
\begin{describe}{$status$}
\item[$status$] For\explabel{SpecVariables} each general $g$, the value of
  $status[g]$ will be the string \str{Loyal} or
  \str{Traitor}, denoting whether or not the general is loyal.
  (Strings, denoted by expressions of the form $"\,\ldots\,"$,
  are a predefined data type of \TLA+.)
The Byzantine generals problem is expressed in terms of which generals
are loyal.  In the formal specification, the state must describe which
generals are loyal.  Hence, we introduce the variable $status$.


\item[$ord$] For each general $g$, the value of
  $ord[g]$ denotes the order chosen by general $g$, or the
  string \str{?} if $g$ has not yet chosen an order.

\item[$now$] The variable $now$ will be a real number that
  denotes the current time.
\end{describe}
In our informal discussion, we describe the values that variables will
have in a behavior that satisfies the specification.  TLA is a
typeless logic, which means that a variable can assume any value.
(More precisely, for any value $v$ and variable $x$, there is a state
in which the value of $x$ is $v$.)  Thus, when we say that the value
of $status[g]$ will be a string, we mean that its value will be a
string in every state of every behavior that satisfies the
specification we are about to describe.

The
 {\makeatletter\@computerule\makebox[5em]{\s{1}\midbar\s{1}}}%
\explabel{midbar} lines are primarily decorative, though the second
one serves to delimit the {\bf assumption} section.

An {\bf assumption}\explabel{assumption} section asserts assumptions
about constant parameters.  In this module, there is a single
assumption named $HiAssump$, which is defined to be the
expression to the right of the $\,\deq\,$\@.  In general, the symbol
$\,\deq\,$\explabel{==} denotes that the identifier to its left is defined
to equal the expression to its right. The formula
\explabel{CAssumpDef}$HiAssump$ is the conjunction of four
assertions:
\begin{enumerate}
\item $Lt$ (the set of lieutenants) is a finite
      set that does not contain $Cmdr$.  

\item $"?"$ is not a possible order. 

\item $Now_0$ is a real number.

\item $\Delta$ is a positive real number.
\end{enumerate}

\TLA+ \explabel{conjNotation}
  %%% there was a typo here--corrected after the face: 14 Oct 94
uses the notation that a
list of expressions bulleted by $/\ $ denotes their conjunction,
and a list of expressions bulleted by $\/ $ denotes their disjunction.
Indentation is used to eliminate parentheses.  

Following the {\bf assumption} section is a section consisting of two
definitions.  The constant operator $Gen$\explabel{OK} is defined to
be the set of all generals---both the lieutenants and the commander.
The boolean operator $\OK$ is defined so that $\OK(x)$ equals \true\
iff $status[x]$ equals $"Loyal"$, for any $x$.  (We care about the
value of $\OK(x)$ only when $x$ is an element of $Gen$.)  Round
parentheses denote application of an operator to its argument (or
arguments).  The symbol $\OK$ by itself, without an argument, is not a
syntactically complete expression.  Square brackets denote function
application.  Both $status$ and $status[e]$ are syntactically complete
expressions that denote values, for any expression $e$.

The 
 {\makeatletter
    \@computerule\raisebox{-.5ex}{\makebox[5em]{\s{1}\tlabotline\s{1}}}}%
\explabel{tlabotline}
line ends the module.

The actual specification is contained in module $HiLevel$, which comes
next.  This module imports the modules $SpecParams$, $Reals$, and
$RealTime$.  

The $RealTime$ module is used to express real-time properties.  It is
essentially the same module as in~\cite{lamport:hybrid}, which in turn
used the definitions from~\cite{abadi:old-fashioned}.\footnote{The
definition of
  $VTimer$ in the $RealTime$ module of~\cite{lamport:hybrid} contains
  a typographical error; the correct definition appears in
  \cite{abadi:old-fashioned} and Figure~\ref{fig:RealTime}.}
Specifying real-time properties is an engineering problem that is
solved by applying standard methods.  We will explain the operators in
the $RealTime$ module as they appear in our specification.  The module
is given in Figure~\ref{fig:RealTime}.  

Importing $SpecParams$ provides module $HiLevel$ with the
specification parameters and the definitions of $Gen$ and $\OK$.
Importing $SpecParams$ does not import the modules $FiniteSets$ and
$Reals$ that it in turn imports.

Instead of reading module $HiLevel$ in sequence, we examine next the
temporal formula $CSpec$\explabel{CSpec}, which specifies the
commander.  This formula has the canonical form
  \label{sec:canonical-form}%
$Init /\ [][Next]_v$ for a process specification\footnote{Since 
real-time conditions are used to specify progress, there are no fairness
conditions in our processes.}, where
\begin{describe}{$Init$}
\item[$Init$] is a {\em predicate\/}---a Boolean expression made from 
   constants and variables.  It describes the initial state of the
   process's variables.

\item[$Next$] is an {\em action\/}---a boolean expression made from
  constants, variables, and primed variables.  It describes all
  steps (pairs of successive states) that can change
  the process's variables.   In an action, unprimed variables denote
  values in the first (starting) state and primed variables denote
  values in the second (final) state.

\item[$v$] is a {\em state function\/}---a nonboolean expression
  made from constants and variables.  It is usually a tuple that
  describes all components of the process's state.
\end{describe}
The formula $[Next]_v$\explabel{SquareSub} denotes $Next \/ (v' = v)$,
so it represents a step that is either a $Next$ step or one that
leaves $v$ (and hence all variables in the tuple $v$) unchanged.
The temporal operator $[]$\explabel{Box} 
means {\em always}, so 
 $Init /\ [][Next]_v$ 
is true for a behavior (infinite sequence of states) iff the first
state satisfies $Init$ and every successive pair of states is either a
$Next$ step or leaves $v$ unchanged.

The commander's state is described by $ord[Cmdr]$ and $status[Cmdr]$,
which are the components of the tuple \explabel{CInit}$var(Cmdr)$.
(In \TLA+, tuples are enclosed in angle brackets $<<\ldots>>$.)  The
initial condition $CInit$ asserts that
\begin{enumerate}
\item The commander's status is either $"Loyal"$ or $"Traitor"$.

\item If her status is $"Loyal"$, then her order is an element
      of $Order$.  The symbol $=>$ denotes logical 
      implication.  It has lower precedence (binds more loosely) than
      any other boolean operator.
\end{enumerate}
The commander's next-state relation is $Fail(Cmdr)$\explabel{Fail},
which asserts that the new value of $status[Cmdr]$ is $"Traitor"$.
This allows any step that ends in a state with $status[Cmdr]$ equal to
$"Traitor"$.  Such a step can change $ord[Cmdr]$ to any value.  Thus,
the formula $CSpec$ is satisfied by any behavior that either
(i)~consists of an infinite number of states with
$status[Cmdr]="Loyal"$ and $ord[g]=o$, for some $o$ in $Order$, or
(ii)~starts with a finite (possibly empty) sequence of such states and
ends with an infinite sequence of states in which $status[Cmdr]$
equals $"Traitor"$ and $ord[Cmdr]$ assumes completely arbitrary
values.

The formula $CSpec$ describes only the values assumed by $ord[Cmdr]$
and $status[Cmdr]$.  It makes no assertion about any other part of the
state---such as the value of the variable $now$, or of $ord[g]$ for
$g$ different from $Cmdr$, or of a variable $foo$ that might be
introduced later.

The formula $LSpec(g)$\explabel{LSpec} is the specification of
lieutenant $g$.  It is the conjunction of two formulas.  The first
asserts that $LInit(g)$ holds initially and that each step is a
$Choose(g)$ step, a $Fail(g)$ step, or a step that leaves lieutenant
$g$'s state unchanged.  The initial predicate $LInit(g)$ asserts that
(i)~$status[g]$ has a correct value, and (ii)~if $g$ is loyal, then
$ord[g]$ equals $"?"$, denoting that $g$ has not yet chosen an order.
A $Choose(g)$\explabel{Choose} step is one in which
\begin{enumerate}
\item In the starting a state, $g$ is loyal and has not yet chosen
      an order.  (Any step taken by a traitorous general can be interpreted
      as a $Fail$ step.)

\item In the final state, $g$ has chosen an order.  

\item For every general $h$ that, in the final state, is loyal and has
   chosen an order, the order that $h$ has chosen is the same as the one 
   that $g$ has chosen.

\item $g$'s status does not change, which by (1) implies that he is
      still loyal in the final state.  The formula\explabel{unchanged} 
      $\unchanged f$ is an abbreviation for $f'= f$.  
%     (The angle brackets, which denote a tuple, are unnecessary.)
\end{enumerate}
The second conjunct of $LSpec(g)$ is of the form $[]P$, for a
predicate $P$.  Such a formula asserts of a behavior that $P$ is true
in every state.  In this case, the formula asserts that if $g$ is
loyal and has not chosen an order, then $now$ is at most
$Now_0+:Delta:$.  In other words, it asserts that if $now$ is greater
than $Now_0+:Delta:$ and $g$ is loyal, then he must have chosen an
order.  Since we interpret $now$ as the current time, the
second conjunct of $LSpec(g)$ asserts that if $g$ is loyal, then he
must choose an order by time $Now_0+:Delta:$.

The formula $Spec$\explabel{Spec} is the complete high-level
specification.  It asserts
\begin{enumerate}
  \item The commander's specification $CSpec$.
  \item The specification $LSpec(g)$, for each lieutenant $g$.
  \item $now=Now_0$, which means that the current time initially 
       (at the start of the algorithm) equals $Now_0$.
  \item Formula $RT(<<ord, status>>)$.  
Module $RealTime$ defines formula $RT(v)$\explabel{RT} to assert that
(a)~$now$ is a monotonically nondecreasing real number and (b)~steps
that change $now$ leave $v$ unchanged.  Thus, $RT(<<ord, status>>)$
asserts that (a)~$now$ changes the way we expect time to change, and
(b)~$ord$ and $status$ do not change when $now$ does.  Thus, in steps
that change $ord$ and $status$, the value of $now$ is the same in the
initial and final state.  Intuitively, this means that we are
considering changes to $ord$ and $status$ to happen instantaneously.
\end{enumerate} 
Formula $Spec$ is the high-level specification.  This means that we
consider a behavior to represent a correct execution of the algorithm
iff it satisfies $Spec$.  A specification is therefore a definition,
and a definition cannot be right or wrong.  However, a
specifications can fail to capture our intent.  To gain confidence in
a specification, we can prove theorems about it.  Such theorems
usually have the form $Spec => Prop$, which asserts that every
behavior satisfying the specification $Spec$ also satisfies the
property $Prop$.  Module $HiLevel$ asserts such a theorem, named
$SpecGood$\explabel{SpecGood}.  This theorem states that, in any
behavior satisfying $Spec$, it is always the case that, for any
general $g$, if $g$ is loyal and the time is later than 
  $Now_0 + :Delta:$, 
then $g$ has chosen an order and his order is the same as that of
every other loyal general.  In other words, every loyal general
chooses an order by time $Now_0 + :Delta:$, and that order is the same
as any other loyal general's order.  All theorems are proved in
Section~\ref{sec:proofs}.


%try
\subsection{The Mid-Level Specification} \label{sec:MidLevelSpec}

The mid-level specification describes Algorithm OM$(1)$ of
\cite{lamport:byzantine}, an ``oral-message'' Byzantine agreement
algorithm that works in the presence of at most one traitor.  It is a
two-round algorithm.  In the first round, the commander sends her
message to all lieutenants.  In the second round, each lieutenant
relays the message he received to all other lieutenants.  A lieutenant
chooses his order by applying a {\em majority\/} function to the
values that he has received.  The only requirements on this majority
function are (i)~if the same order $o$ is received from all but
one of the other generals, then $o$ is chosen, and (ii)~all
lieutenants use the same majority function.

This informal description is essentially the one given in
\cite{lamport:byzantine}.  It contains several tacit assumptions---for
example, that every lieutenant receives a value in the first round,
even if the commander is a traitor.  The formal specification makes
these assumptions explicit.  

Module $MidLevelParams$ of Figure~\ref{fig:MidLevelParams} declares
the following new parameters\explabel{MidParams} that are used in the
mid-level specification.
\begin{describe}{$rcvd$}%{$Majority$}
\item[$rcvd$] For each lieutenant $g$, the order that $g$ receives
directly from the commander is recorded in $rcvd[g][g]$, and the
relayed order that $g$ receives from each other lieutenant $h$ is
recorded in $rcvd[g][h]$.  Thus, for each lieutenant $g$, the value of
$rcvd[g]$ will be a function whose domain is the set $Lt$ of
lieutenants.  If lieutenant $g$ is loyal, then before any
orders have been sent, $rcvd[g][h]$ will equal $"?"$, for all
lieutenants $h$.

%
\begin{figure}[tbp]
\begin{module}{MidLevelParams}
\IMPORT SpecParams, Reals \\
\EXPORT\s{-.3}\expref{export}\s{.3} MidLevelParams, SpecParams, Reals
%
\begin{nodecls}
{\bf parameters} \s{1}
  \= rcvd\expref{MidParams}    : \variable \\
  \> Majority(:?:), :delta:, :epsilon:\expref{MidParams}
           : \constant  
\end{nodecls}
\midbar
\begin{decls}{assumption} 
  MidAssump\expref{MidAssump} == 
   \begin{conj}
       (:delta: :in: Real) /\ (:epsilon: :in: Real) 
        /\ (2* :delta: + :epsilon: :leq: :Delta:) \\
      \begin{noj}
      :A: f :in: [Lt -> Order]\expref{FcnSet} : \\
      __\begin{conj}
         Majority(f) :in: Order  \\
         :A: o :in: Order :
           \begin{noj}
           (:E: h :in: Lt : :A: g :in: Lt :\: \{h\} : f[g] = o)\\
           => (Majority(f) = o)
           \end{noj}
         \end{conj}
      \end{noj}
    \end{conj}
\end{decls}
\end{module}
\vspace{-5pt}

\caption[]{Module $MidLevelParams$.}
\label{fig:MidLevelParams}
\end{figure}
%
\item[$Majority$] The majority function.  More precisely, $Majority$
is an operator with a single argument.  We care about the value
of $Majority(f)$ only when $f$ is a function from $Lt$ to the set
$Order$ of orders.
   
\item[$\delta$] The maximum delay between when an order is sent and
when it is received.  This delay applies both to the sending of orders
by the commander and to the relaying of orders by the lieutenants.
(The delay $\delta$ includes the time needed to decide to send an
order.)

\item[$\epsilon$] The maximum time it takes a lieutenant to make a
decision.  In this specification, the only decision he has to make is
to choose an order once he has received all the relayed orders.
\end{describe}
Assumption $MidAssump$\explabel{MidAssump} makes the following
assertion about the constant parameters.  
\begin{enumerate}
\item $\delta$ and $\epsilon$ are real numbers such that
      $2*\delta+\epsilon$ is at most $\Delta$.

\item For any function $f$ that maps lieutenants to orders:
   \begin{enumerate}
      \item[1.] $Majority(f)$ is an order.
      \item[2.] If $o$ is an order such that $f[g]$ equals $o$ for every
            lieutenant except some lieutenant $h$, then $Majority(f)$
            equals $o$.
   \end{enumerate}
The expression $[Lt -> Order]$\explabel{FcnSet}
denotes the set of all functions $f$ with
domain $Lt$ such that $f[g]\in Order$, for all $g\in Lt$.
\end{enumerate}
The {\bf export}\explabel{export} statement causes the named
definitions to be imported by any module that imports
$MidLevelParams$.  A module name stands for all definitions from that
module.  (Omitting the {\bf export} statement would be equivalent to
writing \mbox{{\bf export} $MidLevelParams$}.)

Module $MidLevel$ in Figure~\ref{fig:MidLevel} defines the
formula $Spec$ to be the mid-level specification.  It first imports
two other modules.  Importing $MidLevelParams$ imports all its
parameters, including the ones it imported from $SpecParams$.

\begin{figure}
\begin{module}{MidLevel}
\IMPORT MidLevelParams, RealTime\\
%
\INCLUDE HiLevel \AS Hi\expref{IncludeHi}
%
\begin{nodecls}
  Relay(g, h)\s{.8} \= \kill
%
  LInit(g)\expref{MidLInit} == 
    \begin{conj}
       Hi.LInit(g) \\
       \OK(g) => (rcvd[g] = [h :in: Lt |-> "?"]) \vs{.4}
    \end{conj}\\
%
  Issue(g)\expref{MidIssue}  \> == 
    \begin{conj}
       \OK(g) /\ rcvd[g][g] = "?" \\
       :E: o :in: Order :  
           \begin{conj}
              rcvd'[g] = [rcvd[g] \except ![g] = o] \\
              \OK(Cmdr) => (o = ord[Cmdr])
           \end{conj}  \\
       \unchanged <<ord[g], status[g]>>        \vs{.4}
    \end{conj} \\
%
  Relay(g, h)\expref{MidRelay} \> == 
    \begin{conj}
       \OK(g) /\ rcvd[g][h] = "?" \\
       :E: o :in: Order : 
           \begin{conj}
              rcvd'[g] = [rcvd[g] \except ![h] = o] \\
              \OK(h) => (o = rcvd[h][h])
           \end{conj}\\
       \unchanged <<ord[g], status[g]>>         \vs{.4}
    \end{conj} \\
%
  Choose(g) \> ==
   \begin{conj}
        \OK(g) /\ ord[g] = "?"                 \\
        :A: h :in: Lt : rcvd[g][h] :neq: "?"   \\
        ord'[g] = Majority(rcvd[g])            \\
        \unchanged <<rcvd[g], status[g]>>      \vs{.4}    
   \end{conj}\\ 
%                                             
  Next(g)\expref{MidNext} \> == 
                Issue(g) \,\/\, (:E: h :in: Lt :\: \{g\} : Relay(g, h)) 
                \,\/\, Choose(g) \,\/\, Hi.Fail(g)\expref{MidFail}\s{-1}
                \V{.4}
% 
  var(g) == <<ord[g], rcvd[g], status[g]>> \V{.4}
%
   LSpec(g)  \= ==  
      \begin{conj}
         LInit(g) /\ :Box: [Next(g)]_{var(g)}\expref{MidLInit} \\
         [] (\OK(g) /\ (rcvd[g][g] = "?") => 
               (now :leq: Now_0 + :delta:))\expref{MidLSpec2} \\
         $\begin{noj}
         :A: h :in: Lt :\: \{g\} : \\
         __ [](\OK(g) /\ (rcvd[g][h] = "?") => 
                (now :leq: Now_0 + 2*:delta:))\expref{MidLSpec2}
         \end{noj}$  \\
         :EE: t : 
            \begin{conj}
               VTimer(t, Choose(g), :epsilon:, var(g))  \\
               MaxTimer(t)\expref{MaxTimer} \vs{.4}
            \end{conj} 
      \end{conj}\\
   Spec\expref{MidSpec}  \>  ==
   \begin{conj}
      Hi.CSpec \\
      :A: g :in: Lt : LSpec(g) \\
      now = Now_0               \\
      RT(<<ord, rcvd, status>>) \vs{.4}
   \end{conj}  
\end{nodecls}
%
\midbar
%
\begin{nodecls}
  OneTraitor\expref{MidCorrect} == 
    :E: h :in: Gen : :A: g :in: Gen :\: \{h\} : \OK(g)
\end{nodecls}
\begin{decls}{theorem} 
 MidCorrect\expref{MidCorrect} == ([] OneTraitor) /\ Spec => Hi.Spec
\end{decls}
\end{module}
\vspace{-5pt}
\caption[]{Module $MidLevel$}
\label{fig:MidLevel}
\end{figure}

The {\bf include}\explabel{IncludeHi} statement incorporates the
definitions from module $HiLevel$, with all defined symbols prefixed
by ``$Hi.$''; for example, a definition of $Hi.var$ is included that
makes $Hi.var(h)$ equal to $<<ord[h], status[h]>>$.  Parameters of an
included module are instantiated by expressions.  In the absence of
explicit instantiation (described below), a parameter is instantiated
by the symbol of the same name.  Thus, the parameter $Cmdr$ of
$HiLevel$ is instantiated by $Cmdr$ (a parameter of $MidLevel$,
obtained via the {\bf import} statement); the parameter $ord$ of
$HiLevel$ is instantiated by $ord$; etc.  When a module is included,
its assumptions (with the appropriate instantiations) must be provable
from the assumptions and definitions of the including module.  Thus,
assumption $Hi.HiAssump$, the assumption of the included module
$HiLevel$, must be provable from the assumptions and definitions of
module $MidLevel$.  This assumption follows trivially from assumption
$HiLevel$, which is imported from module $MidLevelParams$, which in
turn imports it from module $SpecParams$.

Formula $Spec$\explabel{MidSpec} is the specification of the mid-level
algorithm.  It is similar to the specification $Spec$ of module
$HiLevel$, consisting of the conjunction of four formulas that assert:
(i)~the specification $Hi.CSpec$ of the commander included from module
$HiLevel$, (ii)~formula $LSpec(g)$, for every lieutenant $g$,
(iii)~$now$ is initially equal to $Now_0$, and (iv)~formula $RT(<<ord,
rcvd, status>>)$.  As explained in Section~\ref{sec:hi-level-spec},
$RT(<<ord, rcvd, status>>)$ asserts that $now$ behaves the way we
expect it to and that $ord$, $rcvd$, and $status$ change
instantaneously.  The rest of the specification involves the
definition of $LSpec(g)$, the specification of lieutenant~$g$.
Formula $LSpec(g)$ is the conjunction of four formulas, which we
describe in turn.


The first conjunct of $LSpec(g)$\explabel{MidLInit} has the canonical
form $Init /\ [][Next]_v$ explained in
Section~\ref{sec:canonical-form}.  The initial predicate $LInit(g)$
asserts (i)~the initial condition $Hi.LInit(g)$ on $status[g]$ and
$ord[g]$ and (ii)~that $rcvd[g]$ is a function with domain $Lt$ such that
$rcvd[g][h]$ equals $"?"$ for every $h$ in $Lt$.  In general, the
construct $[x :in: S |-> exp(x)]$ denotes the function $f$ with domain
$S$ such that $f[x]=exp(x)$ for all $x$ in $S$.  The next-state
relation $Next(g)$\explabel{MidNext} is the disjunction of four
actions:
\begin{describe}{$Hi.Fail(g)$}
\item[$Issue(g)$] Represents\explabel{MidIssue} the sending of an
order by the commander to lieutenant~$g$.  It is enabled iff $g$ is
loyal and $rcvd[g][g]$ equals $"?"$, denoting that $g$ has not yet
received an order from the commander.  The action sets $rcvd[g][g]$ to
an order that, if the commander is loyal, is actually her order.  The
notation $[f \except ![x] = exp]$ denotes a function $\widehat{f}$ that is the
same as $f$ except that $\widehat{f}[x]$ equals $exp$.  

\item[$\exists\,  h \in Lt \backslash \{g\} : Relay(g, h)$]
Asserts\explabel{MidRelay} that a $Relay(g,h)$ step occurs, for some
lieutenant $h$ other than~$g$.  Such a step represents the relaying of
an order from $h$ to $g$.  If $h$ is loyal, then the relayed order is
$rcvd[h][h]$.

\item[$Hi.Fail(g)$] As described\explabel{MidFail} above, an action
taken when $g$ is or becomes a traitor.  It allows arbitrary changes
to $ord[g]$ and $rcvd[g]$ (and all variables other than $status[g]$).

\item[$Choose(g)$] The action in which $g$ chooses his order by
applying $Majority$ to his array $rcvd[g]$ of relayed values.
\end{describe}
The final three conjuncts of $LSpec(g)$ place timing bounds on when
$g$'s actions must occur.  The second\explabel{MidLSpec2} conjunct
asserts that (it is always true that) if $g$ is loyal and $rcvd[g][g]$
equals $"?"$, then $now$ is at most $Now_0+\delta$.  If $g$ is loyal,
$rcvd[g][g]$ equals $"?"$ iff an $Issue(g)$ step has not occurred.
Thus, this conjunct asserts that, if $g$ is loyal, then an
$Issue(g)$ step must occur by time $Now_0+\delta$.  Similarly, the
third conjunct asserts that, if $g$ is loyal, then a $Relay(g,h)$ step
must occur by time $Now_0+2*\delta$.

The final conjunct of $LSpec(g)$ places a timing bound on the
$Choose(g)$ action, using the temporal formulas $VTimer$\explabel{MaxTimer}
and $MaxTimer$, defined in module
$RealTime$.  These formulas were introduced in \cite{abadi:old-fashioned}
and used again in \cite{lamport:hybrid} as a general method for
specifying real-time bounds.  If $A$ is an action and $v$ a state
function such that any $A$ step changes $v$, and if $t$ is a variable
that does not occur in $A$ or $v$, then the formula
  \mbox{$VTimer(t, A, \epsilon, v) \land MaxTimer(t)$} 
asserts that $A$ cannot be enabled for more than $\epsilon$ time units
before the next $A$ step occurs.  The temporal 
\explabel{EE}existential quantifier
$:EE: t$ essentially hides the variable $t$.  Thus, the fourth
conjunct of $LSpec(g)$ asserts that, if lieutenant $g$ is loyal, then
a $Choose(g)$ step must occur within $\epsilon$ time units of when he
has received an order from the commander and from all other
lieutenants.

Finally, the module\explabel{MidCorrect} asserts the correctness of
the mid-level algorithm.
  The predicate $OneTraitor$ asserts of a state that there is at most
one traitorous general.  Theorem $MidCorrect$ asserts that, for any
behavior, if (i)~there is always at most one traitorous general and
(ii)~formula $Spec$ holds, then formula $Hi.Spec$ holds.  In other
words, this theorem asserts that, in the presence of at most one
traitor, the mid-level specification implements the high-level
specification.


%try


\subsection{The Low-Level Specification} 


In the mid-level specification, a value is transferred from the
commander to a lieutenant in a single step, and is relayed from one
lieutenant to another in a single step.  In the low-level
specification, we model the way values are transmitted over
communication channels.  This requires adding timeouts to detect if a
traitorous general fails to send a message.

The specification uses module $TimedChannel$\explabel{TimedChannel} of
Figure~\ref{fig:TimedChannel}, which provides generic definitions for
describing the transmission of values over a channel.  This module
imports module $Sequences$ to define operators on sequences.  In
\TLA+, an $n$-tuple\explabel{tuple}
  $<<v_{1}, \ldots, v_{n}>>$ is a function whose
domain is the set $\{1,\ldots,n\}$ of natural numbers, where
  $<<v_{1}, \ldots, v_{n}>>[i]$ 
equals $v_{i}$, for $1 :leq: i :leq: n$.  The $Sequences$ module
represents sequences as tuples.  The module is given without
explanation in Figure~\ref{fig:Sequences}.  It defines the usual
operators $Head$, $Tail$, and $:O:$ (concatenation) on sequences.

\begin{figure}
\begin{module}{TimedChannel\expref{TimedChannel}}
\IMPORT Sequences, Reals, RealTime
\begin{nodecls}
{\bf parameters}\s{1} \= src, dest\expref{TCvbls} : \variable \\
                      \> :tau:\expref{tau}   : \constant
\end{nodecls}
\midbar
\begin{nodecls}
{\bf assumption}\s{1} Assump == (:tau: :in: Real) /\ (0 < :tau:)
\end{nodecls}
\begin{nodecls}
% Init  ==  \begin{conj}
%             src  = <<\,<<>>\,, 0>> \\
%             dest = <<\,<<>>\,, 0>> 
%          \end{conj} \\
Send(v)\expref{TCSend} \=  == src' = << src[1] :O: <<v>>, 1 - src[2]>> \\
Rcv(v)\expref{TCSend}  \> ==  
    \begin{conj}
      (dest[1] # <<>>) \, /\ \, (v = Head(dest[1])) \\
      dest' = <<Tail(dest[1]), 1 - dest[2]>> \vs{.2} \\
 \end{conj}\\
Tmt\expref{TCTmt}     \>  ==  
   \begin{conj}
      src[1] # <<>> \\ 
      src' = <<Tail(src[1]), src[2]>> \\ 
      dest' = <<dest[1] :O: <<Head(src[1])>>, dest[2]>> \vs{.4}
   \end{conj} \\
%
ext\expref{TCExt} \> == <<src[2], dest[2]>>\V{.4}
%
Spec\expref{TCSpec} == \begin{conj}
              (src  \s{.5} = << <<>>,\, 0>>) 
                  \;/\ \; [][Tmt \, \/ \, :E: v: Send(v)]_{src} \V{.1}
              (dest = << <<>>,\, 0>>)
                 \; /\ \; [][Tmt \, \/ \, :E: v : Rcv(v)]_{dest}  \V{.1}
              \EE t: VTimer(t, Tmt, :tau:, <<src, dest>>) 
                        /\ MaxTimer(t)\expref{tau}
          \end{conj}
\end{nodecls}
\end{module}
\vspace{-10pt}
\caption[]{Module $TimedChannel$.}
\label{fig:TimedChannel}
\end{figure}

Module $TimedChannel$ has two variable parameters:\explabel{TCvbls}
\begin{describe}{{\it dest}}
 \item[\it src] The interface at the sender's end of the channel.
   It will be a pair whose first element is a sequence of values and
   whose second element is either $0$ or $1$.
                   

 \item[\it dest] The interface at the receiver's end of the channel.
   It will be a pair whose first element is a sequence of values and
   whose second element is either $0$ or $1$.
\end{describe}
(The purpose of the second components of $src$ and $dest$ is explained
below.)  The module has a single constant parameter $\tau$, which is a
real number that represents the maximum time required to transmit one
value.

The sending\explabel{TCSend} of a value $v$ is initiated by a
$Send(v)$ step, which appends $v$ to the tail of $src[1]$ and
complements $src[2]$---changing its value from $0$ to $1$ or
vice-versa.  Receipt of the value $v$ occurs with a $Rcv(v)$ step,
which is enabled iff $v$ is the head of the sequence $dest[1]$.  A
$Rcv(v)$ step removes $v$ from the head of $dest[1]$ and complements
$dest[2]$.

The transmission\explabel{TCTmt} of a value from one end of the
channel to the other is modeled by a $Tmt$ step, which moves an
element from the head of $src[1]$ to the tail of $dest[1]$.

Formula $Spec$\explabel{TCSpec} is the specification of the timed
channel.  A behavior satisfies this formula iff the variables $src$
and $dest$ behave the way they should for a timed channel.  The
formula has three conjuncts.  The first describes the sequence of
values assumed by $src$.  Initially, $src[1]$ is the empty sequence
and $src[2]$ equals $0$; every step that changes $src$ is a $Tmt$
step or a $Send(v)$ step, for some $v$.  The second conjunct similarly
describes the sequence of values assumed by $dest$.  The third
conjunct asserts the real-time requirement.  As explained in
Section~\ref{sec:MidLevelSpec}, the conjunct asserts that $Tmt$ cannot
remain enabled for more than $\tau$\explabel{tau} 
time units before the next $Tmt$
step occurs.  Thus, this conjunct asserts that, when $src[1]$ is
nonempty, values are moved from it to $dest[1]$ at the rate of at
least one every $\tau$ time units.

We now come to \explabel{TCExt}$ext$, the pair consisting of the
second components of $src$ and $dest$, and the explanation of what
those second components are for.  The channel specification $Spec$
allows arbitrary values to be sent ``spontaneously'', and it allows
those values to be received at arbitrary times.  This specification is
used by conjoining it with specifications of a sender and receiver
that constrain when $Send$ and $Rcv$ actions occur.  The sender's
specification will describe when $Send$ actions can occur and what
values they can send; the receiver's specification will describe when
$Rcv$ actions can occur.  The sender's and receiver's specifications
must also allow the channel's internal $Tmt$ steps.  They allow such
steps by allowing any step that leave $ext$ unchanged; $Spec$ implies
that any such step must be a $Tmt$ step.

Module $LowLevelParams$ in Figure~\ref{fig:low-level-params} begins
the specification of the low-level algorithm itself.  The module
imports the two higher-level $\ldots{}Params$ modules and declares
three new variable parameters:
%
\begin{figure}
\begin{module}{LowLevelParams}
\IMPORT SpecParams, MidLevelParams, Reals \\
\EXPORT SpecParams, MidLevelParams, Reals, LowLevelParams, Hi, 
  Mid, TC\expref{LowExport}
\begin{nodecls}
{\bf parameters} \s{1} \= in, out, sent\expref{LowLevelVbls} : \variable\\
                       \> \tau\expref{LowParamTau} : \constant
\end{nodecls}
\midbar
\begin{nodecls}
{\bf assumption} \s{1} 
   LowAssump == (:tau: :in: Real) /\ (0 < :tau:) 
                       /\ (:tau: + 3 * :epsilon: :leq: :delta:)
\end{nodecls}
\midbar
\INCLUDE HiLevel  \AS Hi\\
\INCLUDE MidLevel \AS Mid\\
\INCLUDE TimedChannel \AS $TC(g,h)$ \WITH $src <- out[g][h]$, 
  $dest <- in[h][g]$\expref{param.include}
\midbar
\begin{nodecls}
AllBut(func, g)  h) \= \kill
%
AllBut(func, g)\expref{AllBut}  \> == [h :in: Lt :\: \{g\} |-> func[h]] \\
NotSent(g, h) \> == sent[g][h] = "No" \\
ext(g)\expref{LowExp}        \> == [h :in: Lt |-> TC(g, h).ext]
\end{nodecls}
\end{module}
\vspace{-5pt}
\caption[]{Module $LowLevelParams$.}
\label{fig:low-level-params}
\end{figure}
%
\begin{describe}{$sent$}
\item[$in$]  The\explabel{LowLevelVbls} 
state function $in[h][g]$ represents the 
receiver's end ($dest$) of the channel from $g$ to $h$.

\item[$out$] The state function $out[g][h]$ represents the
sender's end ($src$) of the channel from $g$ to $h$.

\item[$sent$] The value of $sent[g][h]$, which will be either $"Yes"$
or $"No"$, records whether or not general $g$ has sent a value to
lieutenant $h$.  For each general $g$, $sent[g]$ will be a function
with domain $Lt$.
\end{describe}
The constant parameter $\tau$\explabel{LowParamTau} 
has the same meaning as in module
$TimedChannel$.  

The module next asserts assumption $LowAssump$, which relates $\tau$
to $\delta$ and $\epsilon$.  The module also asserts assumptions
$HiAssump$ and $MidAssump$, which are imported with modules
$SpecParams$ and $MidLevelParams$, respectively.

Module $LowLevelParams$ then includes modules $HiLevel$ and
$MidLevel$, and includes a parameterized copy of module
\explabel{param.include}$TimedChannel$.  The latter {\bf include}
statement incorporates all the definitions from module $TimedChannel$
prefixed with ``$TC(g,h).$'', and with the indicated instantiations of
the parameters $src$ and $dest$.  For example, it includes the
definition
 \[ TC(g,h).Tmt \> ==
   \begin{conj}
      out[g][h][1] # <<>> \\ 
      out[g][h]' = <<Tail(out[g][h][1]), out[g][h][2]>> \\ 
      in[h][g]' = 
        <<in[h][g][1] :O: <<Head(out[g][h][1])>>, in[h][g][2]>> \vs{.4}
   \end{conj} 
 \] 
The {\bf export}\explabel{LowExport} statement exports all these
included definitions, as well as the ones from the imported modules and
the definitions made in the $LowLevelParams$ module itself.

Finally, the module makes three definitions.  If
\explabel{AllBut}$func$ is a function with domain $Lt$, then
$AllBut(func, g)$ is the restriction of $func$ to the domain $Lt :\:
\{g\}$, the set of all lieutenants other than~$g$.  The state function
\explabel{LowExp}$ext(g)$ is the array of $ext$ tuples for each
channel interface at lieutenant~$g$.  Thus, a step that leaves
$ext(g)$ unchanged allows $Tmt$ steps for all the channels to and from
$g$, but allows no $Send$ or $Rcv$ actions on those channels.


The definitions of the predicates and actions used in the final
specification appear in module $LowLevelActions$ of
Figure~\ref{fig:low-level-actions}.  (Normally, one would combine this
module with module $LowLevel$; we have split the specification to keep
each module less than one page long.)

\begin{figure}
\begin{module}{LowLevelActions}
\IMPORT\ LowLevelParams, RealTime
\midbar
\begin{nodecls}
CSend(g) \= \kill
%
CInit \> == \begin{conj}
              Hi.CInit \\ 
              \OK(Cmdr) => (sent[Cmdr] = [h :in: Lt |-> "No"])
            \end{conj} 
%
\rightcomment{The commander.\expref{LowCommander}}\V{.4}
% 
 CSend(g) \> == 
    \begin{conj}
       \OK(Cmdr) /\ NotSent(Cmdr, g)\\ 
       TC(Cmdr, g).Send(ord[Cmdr])\\
       sent'[Cmdr] = [sent[Cmdr] \except ![g] = "Yes"] \\
       \unchanged <<\begin{noj}
                     in[Cmdr], AllBut(out[Cmdr], g), ord[Cmdr], \\
                       __status[Cmdr]>> \vs{.4}
                   \end{noj}
     \end{conj}
\\
%
  CNext \> == Hi.Fail(Cmdr) _.\/_. :E: g :in: Lt : CSend(g)
%
%
\end{nodecls}
\midbar
\begin{nodecls}
% 
%  \comment{\s{-.5}Lieutenant $g$.}\\
Relay(g,h) \=\kill
%
  LInit(g) \> == \begin{conj}
                   Mid.LInit(g) \\
                   \OK(g) => (sent[g] = [h :in: Lt |-> "No"])
                 \end{conj}
\rightcomment{Lieutenant $g$.\expref{LowLt}}\\
%
  Issue(g) \> == \begin{conj}
              \OK(g) /\ (rcvd[g][g] = "?") \\
              :E: o :in: Order :
                 \begin{conj}
                    TC(Cmdr, g).Rcv(o)\\
                    rcvd'[g] = [rcvd[g] \except ![g] = o]
                 \end{conj} \\
               \unchanged <<ord[g], AllBut(in[g], Cmdr), out[g], 
                            status[g], sent[g]>>
             \end{conj}
\\
%
  Send(g, h) \> == \begin{conj}
                    \OK(g) /\ (rcvd[g][g] # "?") /\ NotSent(g, h)\\
                    TC(g, h).Send(rcvd[g][g])\\
                    sent'[g] = [sent[g] \except ![h] = "Yes"]\\
                    \unchanged <<ord[g], rcvd[g], in[g], AllBut(out[g], h), 
                                 status[g]>>                        \vs{.4}
                  \end{conj} \\
%
  Relay(g,h) \> == \begin{conj}
                  \OK(g) /\ (rcvd[g][h] = "?") \\
                  :E: o :in: Order : 
                     \begin{conj}
                       TC(h, g).Rcv(o)\\
                       rcvd'[g] = [rcvd[g] \except ![h] = o]
                     \end{conj}\\
                  \unchanged <<ord[g], AllBut(in[g], h), 
                                  out[g], status[g], sent[g]>> \vs{.4}
                \end{conj} \\
%
 Choose(g) \> == Mid.Choose(g) /\ \unchanged<<in[g], out[g]>>
%
%
\end{nodecls}
\midbar
\begin{nodecls}
RelayTimeout(g,h) \=\kill
% 
 IssueTimeout(g) \> == \begin{conj}
                    \OK(g) /\ (rcvd[g][g] = "?")\\
                    Now_0+:tau:+ 2*:epsilon: < now \\
                    :E: o :in: Order : rcvd'[g] = [rcvd[g] \except ![g] = o]\\
                    \unchanged <<ord[g], in[g], out[g], status[g], sent[g]>> 
                               \vs{.4}
                  \end{conj}
\rightcomment{Timeout actions.\expref{Timeout}}
\\
%
 RelayTimeout(g,h) \> ==  
    \begin{conj}
       \OK(g) /\ (rcvd[g][h] = "?") \\
       Now_0 + 2*:tau: +  5 * :epsilon: < now \\
       :E: o :in: Order : rcvd'[g] = [rcvd[g] \except ![h] = o] \\
       \unchanged <<ord[g], in[g], out[g], status[g]>>                \vs{.4}
     \end{conj}
%
\end{nodecls}
\midbar
\begin{nodecls}
%
  LNext(g)\expref{LNext}  ==  
    \begin{disj}
      Issue(g) \/ Choose(g) \/ IssueTimeout(g)                    \\
      :E: h :in: Lt :\: \{g\} :                             
          Send(g,h) \/ Relay(g, h) \/ RelayTimeout(g, h)    \\
      Hi.Fail(g)    % \s{3}\fbox{\comment{Added $Hi.Fail(g)$}}
    \end{disj}      \vs{.4}
\end{nodecls}
%
\end{module}
\vspace{-5pt}
\caption[]{Module $LowLevelActions$.}
\label{fig:low-level-actions}
\end{figure}

The section following\explabel{LowCommander} the {\bf import}
statement specifies the initial predicate $CInit$ and next-state
action $CNext$ of the commander.  (The heading is a comment,
distinguished by its upright font.)  The commander can either do a
$Hi.Fail$ step (any step that ends with $status[Cmdr]="Traitor"$) or
send her order to some lieutenant $g$ with a $CSend(g)$ step.  A
$CSend(g)$ step is enabled iff the commander is loyal and has not yet
sent her order to $g$; it sends the order and changes $sent[g]$ to
indicate that the order was sent.

The next section\explabel{LowLt} defines the initial condition and the
normal actions for a lieutenant.  The $Issue$ and $Relay$ actions
represent the receipt of an order from the commander or another
lieutenant, respectively.  The $Send$ action is the one in which a
lieutenant sends an order on a channel.

The following section\explabel{Timeout} gives the definitions of a
lieutenant's two timeout actions.  An $IssueTimeout(g)$ step can occur
if lieutenant $g$ has not received an order from the commander by time
$Now_0+\tau+2*\epsilon$.  A $RelayTimeout(g,h)$ step can occur if $g$
has not received a relayed order from lieutenant $h$ by time
$Now_0+2*\tau+5*\epsilon$.  These timeouts are needed to ensure
progress if a traitorous general fails to send an order.

Action $LNext(g)$\explabel{LNext} is the next-state action of
lieutenant~$g$.

Finally, module $LowLevel$ in Figure~\ref{fig:low-level} imports the
preceding two modules and defines the complete low-level specification
$Spec$.  



\begin{figure}
\vspace*{10pt}

\begin{module}{LowLevel}
\IMPORT LowLevelParams, LowLevelActions
\midbar
\begin{nodecls}
lvar(g) \=\kill
%
cvar    \> == <<ord[Cmdr], ext(Cmdr), status[Cmdr], sent[Cmdr]>> 
\rightcomment{State functions.\expref{cvarAndlvar}}
\\
%
lvar(g) \> == <<ord[g], rcvd[g], ext(g), status[g], sent[g]>> 
\end{nodecls}
\midbar
\begin{nodecls}
%
EMax(g, A)\expref{EMax} == 
        :EE: t : VTimer(t, A, :epsilon:, lvar(g))  /\ MaxTimer(t) 
\rightcomment{Temporal formulas.}
\V{.4}
%
CSpec\expref{LowCSpec} == 
  \begin{conj}
     CInit /\ [][CNext]_{cvar}           \\
     :A: g :in: Lt : EMax(Cmdr, CSend(g))   \vs{.4}
  \end{conj}\\
%
LSpec(g)\expref{LowLSpec} ==
  \begin{conj}
    LInit(g) /\ [][LNext(g)]_{lvar(g)} \\
    EMax(g, Issue(g)) \\ EMax(g, IssueTimeout(g)) \\  EMax(g, Choose(g)) \\
    :A: h :in: Lt :\: \{g\} : 
      \begin{conj}
        EMax(g, Send(g,h)) \\ 
        EMax(g, Relay(g,h)) \\ 
        EMax(g, RelayTimeout(g, h))                               \vs{.4}
      \end{conj}
  \end{conj} \\
%
Spec\expref{LowSpec} == 
  \begin{conj}
     CSpec \\
     :A: g :in: Lt : LSpec(g)\\
     :A: g, h :in: Gen : TC(g, h).Spec\\
     now = Now_0 \\
     RT(<<ord, rcvd, in, out, status, sent>>)\vs{.4}
  \end{conj}
\end{nodecls}
%
\midbar
%
\begin{nodecls}
{\bf theorem} \s{1} LowCorrect == Spec => Mid.Spec
\end{nodecls}
\end{module}
\vspace{-5pt}
\caption[]{Module $LowLevel$.}
\label{fig:low-level}

\vspace*{10pt}
\end{figure}

The \explabel{cvarAndlvar}state functions $cvar$ and $lvar(g)$ are the
tuples of variables of the commander and lieutenant $g$, respectively.

The formula $EMax(g,A)$\explabel{EMax} asserts that action $A$ cannot
be enabled for more than $\epsilon$ time units before the next $A$
step occurs (assuming that an $A$ step changes $lvar(g)$).

Formula $CSpec$\explabel{LowCSpec} is the commander's specification.
The second conjunct asserts that, for every lieutenant $g$, a
$CSend(g)$ step must occur within $\epsilon$ seconds of when it
becomes enabled.  If the commander is loyal, then action $CSend(g)$ is
enabled initially and remains enabled until she sends $g$ her order.
Thus, the second conjunct asserts that a loyal commander must send her
order to every lieutenant within $\epsilon$ time units of the start of
the algorithm.

Formula $LSpec(g)$\explabel{LowLSpec} is the specification of
lieutenant~$g$.  The last four conjuncts express the requirements
that, if loyal, he must execute each of his actions within $\epsilon$
time units of when he can.

Finally, the complete\explabel{LowSpec} specification $Spec$ has five
conjuncts: (i)~the specification of the commander, (ii)~the
specifications of the lieutenants, (iii)~the specifications of all the
communication channels, (iv)~the specification of the
starting time,  and (v)~the usual $RT$ formula.

%try


\section{The Proofs} \label{sec:proofs}

We now describe how the theorems asserted in the specifications above
are proved.  The key to moving proofs from the realm of mathematics
into engineering practice is hierarchical structuring.  We use the
method of structuring proofs introduced in~\cite{lamport:howtoprove}.
The conventions used in this method are described as they appear.

A hierarchically structured proof is a sequence of steps, each with a
proof.  The proof of a step is either a short paragraph or
calculation, or else a hierarchically structured proof.  The idea is
to make the unstructured ``leaf'' proofs sufficiently easy to check
that they are highly unlikely to be wrong.  We indicate how proofs of
our theorems are carried down to the level at which each leaf proof
consists of simple expansion of definitions and propositional logic.
Such simple proofs are easy to check mechanically; most steps in our
proofs can be checked with the TLP verification
system~\cite{engberg:mechanical}.


\subsection{Proof of Theorem {\it SpecGood}}

Figure~\ref{fig:SpecGoodHi} is the high-level proof of theorem
$SpecGood$, consisting of the level-one steps and the proof of the
final step.  The {\sc Let} construct introduces definitions local to
the proof.  We use a hierarchical numbering convention for denoting
parts of formulas, adding numbers to bulleted lists of conjuncts and
disjuncts.  Thus, $Inv(g,h).3$ is the formula
  $Loyal(g) /\ (ord[g] \ldots \Delta)$.
We extend this convention to quantified formulas, so if $F$ is the
formula $:E: x : P(x)$, then $F(y)$ denotes the formula $P(y)$.  We
use this convention for formulas defined in the specifications even
when the conjuncts and disjuncts are not explicitly numbered.  Thus,
with the definition if $Issue$ from module $MidLevel$
(Figure~\ref{fig:MidLevel}), $Issue(h).2(p).1$ denotes 
the formula
 $rcvd'[h] = [rcvd[h] \except ![h] = p]$.

\begin{figure}
\pflet{$Good(g) == 
  \begin{noj}
    \OK(g) /\ (Now_0 + :Delta: < now )\\
    __=> \begin{conj}
           ord[g] :in: Order \\
           :A: h :in: Gen : \OK(h) => (ord[g] = ord[h])
         \end{conj}
   \end{noj}$}

\noindent
${\bf Theorem}\s{1} Spec => [](:A: g :in: Gen : Good(g))$
\begin{proof}
\setlength{\stepsep}{.5ex}
\pflet{$Inv(g,h) ==
         \begin{conj*}
         \OK(g) => ord[g] :in: Order :cup: \{"?"\} \\
         \begin{noj}
           \OK(g) /\ \OK(h) /\ (ord[g] # "?") /\ (ord[h] # "?") \\
           __ => (ord[g] = ord[h]) 
         \end{noj}  \\
         \OK(g) /\ (ord[g] = "?") => (now :leq: Now_0 + :Delta:)
         \end{conj*}$\\
%
         $CInv == \OK(Cmdr) => (ord[Cmdr] :in: Order)$}

\step{<1>1}{\assume{$g, h  :in: Lt$}
         \prove{$LSpec(g) /\ LSpec(h) => [] Inv(g,h)$}}

\step{<1>2}{\assume{$g :in: Lt$}
         \prove{$LSpec(g) /\ CSpec => []Inv(g,Cmdr)$}}

\step{<1>3}{$CSpec => [] CInv$}

\step{<1>4}{$CInv /\ (:A: g :in: Lt : :A: h :in: Gen : Inv(g,h)) =>
                      (:A: g :in: Gen : Good(g))$}

%\step{<1>5}{Q.E.D.\expref{qedstep}}
\qedstep
  \begin{proof}
    \pf\ 
     $\begin{noj3}
         Spec & => &  \comment{\{By the definition of $Spec$.\}}\\
              &    & CSpec /\ (:A: g, h :in: Lt : 
                                LSpec(g) /\ LSpec(h))\\
              & => & 
               \comment{\{By \stepref{<1>1}, \stepref{<1>2}, and \stepref{<1>3}.\}}\\
              &    & []CInv 
                       /\ (:A: g, h :in: Lt : [] Inv(g,h) /\ []Inv(g,Cmdr)) \\
             & :equiv: & \comment{\{By the temporal logic rule that $\Box$
                                distributes over conjunction.\}} \\
             &     & [](CInv /\ (:A: g, h :in: Lt :  Inv(g,h) /\ Inv(g,Cmdr))\\
             & => & \comment{\{\stepref{<1>4}, the definition of $Gen$,
                       and the temporal logic rule} \\
             &    & __\tlacomment{$(P => Q) \vdash ([]P => []Q)$.\}}\\
             &    & [](:A: g :in: Gen : Good(g)) ___\qed 
          \end{noj3}$
 \end{proof}

\end{proof}

%\rule{\textwidth}{1pt}
\caption[]{The high-level structure of the proof of theorem $SpecGood$}
\label{fig:SpecGoodHi}
\end{figure}


Theorem $SpecGood$ is of the form $Spec => []P$, for a state predicate
$P$.  If $Spec$ were of the canonical form $Init /\ [][N]_v$, then
this would be a completely standard proof using the method first
described by Ashcroft~\cite{ashcroft:proving}: find a state predicate
$I$ (the {\em invariant\/}) such that (i)~$Init$ implies $I$, (ii)~$I$
implies $P$, and (iii)~$I /\ [N]_v$ implies $I'$.  (This TLA
formulation of the proof method is more transparent than its original
description as a method for reasoning about programs.)  Since $Spec$
is written as the conjunction of formulas in canonical form, along
with formulas of the form $[]Q$, our proof involves a simple
generalization of Ashcroft's method.

The
  %\explabel{qedstep}%
Q.E.D. in step $<<1>>5$ stands for the goal to be proved---in this
case, the theorem itself.  In the proof, curly braces enclose the
justification of the implication or equivalence.  Each step in this
chain of implications and equivalence follows from simple substitution
and application of standard rules.

To finish the proof, we must now prove statements $<<1>>1$--$<<1>>4$.
The proof of $<<1>>4$ involves simple predicate logic and will not be
discussed.  The proofs of $<<1>>1$, $<<1>>2$, and $<<1>>3$ are similar;
we consider only $<<1>>1$.



The first-level proof of $<<1>>1$ appears in
Figure~\ref{fig:HiStep1.1}.  The rule that underlies the proof is that
proving $I /\ A => I'$ allows us to infer $I /\ []A => []I$, where $I$
is a predicate and $A$ an action.  This is an
RTLA~\cite{lamport:newtla} rule, where RTLA is a logic that is like
TLA except that $[]A$ is an RTLA formula for any action $A$, not just
for actions $A$ of the form $[N]_v$.  In RTLA, temporal quantification
(the operator $\EE$) can be applied only to a TLA formula, not to an
arbitrary RTLA formula.  All TLA proof rules are valid for RTLA\@.


\begin{figure}
\begin{proof}
\setlength{\stepsep}{.5ex}
\step{<1>1}{\assume{$g, h  :in: Lt$}
         \prove{$LSpec(g) /\ LSpec(h) => [] Inv(g,h)$}}
\begin{proof}
\pflet{$T(g) == \OK(g) /\ (ord[g] = "?") => (now :leq: Now_0 + :Delta:)$}
\step{<2>1}{$LInit(g)/\ LInit(h) /\ T(g) => Inv(g,h)$}

\step{<2>2}{$\begin{conj}
               Inv(g,h) \\
               [Choose(g) \/ Fail(g)]_{var(g)}    
                 /\ [Choose(h) \/ Fail(h)]_{var(h)} \\
               T(g)'
             \end{conj}\\
            => Inv(g,h)'$}

\qedstep
\begin{proof}
\pf\\
$__\begin{noj3}
   \lefteqn{LSpec(g) /\ LSpec(h)}__ \\
    & => & \tlacomment{\{By definition of $LSpec$ and $T$.\}} \\
    & &  \begin{conj}
          LInit(g) /\ LInit(h) \\         
          [][Choose(g) \/ Fail(g)]_{var(g)} 
               /\ [][Choose(h) \/ Fail(h)]_{var(h)} \\
          [] T(g) \vs{.1}
         \end{conj}\\
    & => & \tlacomment{\{Using the RTLA rule $\vdash []P :equiv: P /\ []P'$, 
                         for any predicate $P$.\}} \\
    & &  \begin{conj}
          LInit(g) /\ LInit(h) /\ T(g)\\         
          [][Choose(g) \/ Fail(g)]_{var(g)} 
               /\ [][Choose(h) \/ Fail(h)]_{var(h)} \\
          [] T(g)' \vs{.1}
         \end{conj}\\
    & => & \tlacomment{\{By $<<2>>1$.\}} \\
    & &  \begin{conj}
          Inv(g,h) \\
          [][Choose(g) \/ Fail(g)]_{var(g)} 
               /\ [][Choose(h) \/ Fail(h)]_{var(h)} \\
          [] T(g)' \vs{.1}
         \end{conj}\\
    & => & \tlacomment{\{Using the rule that $[]$ distributes over $/\ $.\}} \\
    & &  \begin{conj}
          Inv(g,h) \\
          []([Choose(g) \/ Fail(g)]_{var(g)} 
               /\ [Choose(h) \/ Fail(h)]_{var(h)} /\ T(g)') \vs{.2}
         \end{conj}\\
    & => & \tlacomment{\{By $<<2>>2$ and the RTLA Rule 
              $(I /\ A => I')\vdash(I /\ []A => []I)$,
             for}\\
    & & \tlacomment{__any predicate $I$ and action $A$.\}} \\
    & & []Inv(g,h)___\qed
 \end{noj3}$
\end{proof}
\end{proof}
\end{proof}
\caption[]{The high-level structure of the proof of step $\langle1\rangle1$
from Figure~\ref{fig:SpecGoodHi}.}
\label{fig:HiStep1.1}
\end{figure}

To complete the proof of $<<1>>1$, we must prove $<<2>>1$ and
$<<2>>2$.  Step $<<2>>1$ follows from the definitions by simple
predicate logic.  The proof of $<<2>>2$ is shown in
Figure~\ref{fig:HiStep2.2}.  The proof goal is first transformed into
an {\sc Assume}/{\sc Prove} form, so the new goal becomes simply
$Inv(g,h)'$.  Inside the proof, these four assumptions are referred to
as assumption $<<2>>$:1--$<<2>>$:4.

Since $Inv(g,h)$ is the conjunction of the formulas
$Inv(g,h).1$, $Inv(g,h).2$, and $Inv(g,h).3$, the next level of the
proof (steps $<<3>>1$--$<<3>>4$) is immediate.  The proof of $<<3>>1$
is given; the proofs of $<<3>>2$ and $<<3>>3$ are analogous.

The goal, $Inv(g,h).1'$ is deduced from assumptions $<<2>>$:1 and
$<<2>>$:2.  Since assumption $<<2>>$:2 is a disjunction, we do a
proof by cases.  The statement \mbox{{\sc Case}: S} is equivalent to
\mbox{{\sc Assume}: S}, \mbox{{\sc Prove}: Q.E.D.}


\begin{figure}
\begin{proof}
\setlength{\stepsep}{.5ex}
\nostep{<1>1}
\begin{noproof}
\nostep{<2>1}
\step{<2>2}{$\begin{conj}
               Inv(g,h) \\
               [Choose(g) \/ Fail(g)]_{var(g)}    
                 /\ [Choose(h) \/ Fail(h)]_{var(h)} \\
               T(g)'
             \end{conj}\\
            => Inv(g,h)'$}
\begin{proof}
\pf\ By propositional logic, it suffices to:
\assume{\begin{enumerate}
                 \item $Inv(g,h)$                           %1
                 \item $[Choose(g) \/ Fail(g)]_{var(g)}$    %3
                 \item $[Choose(h) \/ Fail(h)]_{var(h)}$    %4
                 \item $T(g)'$                              %2
                 \end{enumerate}}
\prove{$Inv(g,h)'$}
  \step{<3>1}{$Inv(g,h).1'$}
  \begin{proof}
     \pf\ By definition of $Inv(g,h).1'$ and propositional logic, it 
     suffices to:
     \assume{$\OK(g)'$}
     \prove{$ord'[g] :in: Order :cup: \{"?"\}$}
     \setlength{\stepsep}{0pt}
     \step{<4>1}{\case{$\unchanged var(g)$}}
     \begin{proof}
       \pf\ Assumption \levelref{<2>2}:1, Case Assumption
       \levelref{<4>1}, and the definition of $Inv$, since 
       $\unchanged var(g)$ implies
       $ord'[g]=ord[g]$.~\qed
     \end{proof}
     \step{<4>2}{\case{$Choose(g)$}}
     \begin{proof}
       \pf\ Case Assumption \levelref{<4>2}, since
           \raisebox{0pt}[0pt]{$Choose(g).2 \;\deq\; ord'[g] \in Order$}.~\qed
     \end{proof}
     \step{<4>3}{\case{$Fail(g)$}}
     \begin{proof}
       \pf\ Case Assumption \levelref{<4>3} and Assumption \levelref{<3>1}
       lead to a contradiction, since $Fail(g)$ implies $~Loyal(g)'$
        by definition of $Fail$ and $Loyal$.~\qed
     \end{proof}
     \qedstep
     \begin{proof}
       \pf\ By propositional logic from 
       \stepref{<4>1}, \stepref{<4>2}, \stepref{<4>3}, and 
       Assumption \levelref{<2>2}:2,
       since $[A]_v \deq A \/ (\unchanged v)$.~\qed
     \end{proof}     
  \end{proof}
  \step{<3>2}{$Inv(g,h).2'$}
  \step{<3>3}{$Inv(g,h).3'$}
  \qedstep
  \begin{proof}
    \pf\ \stepref{<3>1}, \stepref{<3>2}, \stepref{<3>3}, and
    the definition of $Inv$.~\qed
  \end{proof}
\end{proof}

\end{noproof}
\end{proof}
%\rule{\textwidth}{1pt}
\caption[]{The proof of step $\langle2\rangle2$ from
Figure~\ref{fig:HiStep1.1}.}
\label{fig:HiStep2.2}
\end{figure}


%try



%\pfhidelevel{2}

\subsection{Proof of Theorem {\it MidCorrect}}


Theorem $MidCorrect$ asserts that $([] OneTraitor) /\ Spec$ implies
$Hi.Spec$.  It is trivial to prove that $Spec$ implies $Hi.Spec.1$ and
$Hi.Spec.3$, so the problem is proving $Hi.Spec.2$ and $Hi.Spec.4$.
Proving $Hi.Spec.2$ requires proving $Hi.LSpec(g).1$ and
$Hi.LSpec(g).2$ for each lieutenant~$g$.  

The high-level structure of the proof of theorem $MidCorrect$ appears
in Figure~\ref{fig:MidCorrectHi}.  Steps $<<1>>2$ and $<<1>>4$ prove
$Hi.LSpec(g).1$ and $Hi.LSpec(g).2$, respectively, and $<<1>>5$ proves
$Hi.Spec.4$.  Steps $<<1>>1$ and $<<1>>3$ establish useful invariants.

\begin{figure}

{\bf Theorem}\s{1}$([] OneTraitor) /\ Spec => Hi.Spec$ 
\begin{proof}
\setlength{\stepsep}{.5ex}
\pflet{$\begin{noj3}
   Inv(g,l) & \deq &
      \begin{noj}
        \OK(g) => \\
        __\begin{conj*}
            (\domain{rcvd[g]} = Lt)  \\  %1
             (rcvd[g][l] \neq "?") => (rcvd[g][l] \in Order) \\  %2
             \begin{noj}
               \OK(Cmdr) /\  (rcvd[g][g] \in Order)\\
                 __=> (rcvd[g][g] = ord[Cmdr]) 
             \end{noj} \\ %3
           \OK(l) /\ (rcvd[g][l] \in Order) => (rcvd[g][l] = rcvd[l][l]) \\  %4
           (ord[g] \neq "?") =>           %5
              \begin{conj}
                ord[g] = Majority(rcvd[g]) \\
                \A h \in Lt: rcvd[g][h] \neq "?"
              \end{conj} 
        \end{conj*} 
      \end{noj}\\
%
     TInv(g) & \deq &
       \begin{conj*}
         now \in Real \\
         \begin{noj}
           \OK(g) /\ (ord[g] = "?") /\ (\A h \in Lt: rcvd[g][h] \neq "?") \\
           __ => (now \leq Now_0 + 2\delta + \epsilon)
         \end{noj}
       \end{conj*}
  \end{noj3}$}

\step{<1>1}{\assume{$g,l \in Lt$}
            \prove{$Hi.CSpec /\ LSpec(g) /\ LSpec(l) => [] Inv(g,l)$}}


\step{<1>2}{\assume{$g \in Lt$}
            \prove{$[] OneTraitor \,/\ \, 
                   LSpec(g) \,/\ \, (:A: h,l :in: Lt: []Inv(h,l))
                    => Hi.LSpec(g).1$}}

\step{<1>3}{\assume{$g \in Lt$}
\prove{$(now = Now_0) /\ RT(<<ord,rcvd,status>>) /\ LSpec(g)$\\
       $__/\ \,(:A: h :in: Lt: []Inv(g,h)) => [] TInv(g)$ }}

\step{<1>4}{%
  \assume{$g :in: Lt$}
  \prove{$LSpec(g) /\ [] TInv(g) => Hi.LSpec(g).2$}}

\step{<1>5}{$RT(<<ord,rcvd,status>>) => RT(<<ord,status>>)$}

\qedstep
\begin{proof}
  \setlength{\stepsep}{0ex}
  \step{<2>1}{$([] OneTraitor) /\ Spec => Hi.Spec.1$}
  \begin{proof}
    \pf\ Trivial, since $Spec.1$ is the same as $Hi.Spec.1$.~\qed
  \end{proof}
  \step{<2>2}{$([] OneTraitor) /\ Spec => Hi.Spec.2$}
  \begin{proof}
     \pf\ By \stepref{<1>1}--\stepref{<1>4} and the definitions
     of $Spec$ and $Hi.Spec$, since $Spec.2$ equals 
     $:A: l :in: Lt : LSpec(l)$, and $Hi.Spec.2$ equals
     $:A: g :in: Lt : Hi.LSpec(g)$.~\qed
  \end{proof}

  \step{<2>3}{$([] OneTraitor) /\ Spec => Hi.Spec.3$}
  \begin{proof}
    \pf\ Trivial, since $Spec.3$ is the same as $Hi.Spec.3$.~\qed
  \end{proof}
  
  \step{<2>4}{$([] OneTraitor) /\ Spec => Hi.Spec.4$}
  \begin{proof}
    \pf\ By \stepref{<1>5} and the definitions of $Spec$ and $Hi.Spec$.~\qed
  \end{proof}

  \qedstep
  \begin{proof}
    \pf\ \stepref{<2>1}--\stepref{<2>4} and the definition of $Hi.Spec$.~\qed
  \end{proof}
\end{proof}
\end{proof}

\caption[]{The high-level structure of the proof of theorem $MidCorrect$}
\label{fig:MidCorrectHi}
\end{figure}


Step $<<1>>1$ is an invariance proof of the kind we have already
seen in the proof of theorem $SpecGood$.  Its proof is omitted.

We consider now the proof of $<<1>>2$, which appears in
Figure~\ref{fig:MidStep1.2}.  The key step is $<<2>>2$, whose proof is
in Figure~\ref{fig:MidStep2.2}.  Since $Hi.var(g)$ is a subtuple of
$var(g)$, it is obvious that $\unchanged <<var(g)>>$ implies
$\unchanged <<Hi.var(g)>>$.  The proof demonstrates that every step of
the mid-level specification, which is a $Next(g)$ step, is a
$[Hi.Choose(g) \/ Hi.Fail(g)]_{Hi.var(g)}$ step---that is, a step
allowed by the high-level specification.  (This is sometimes called
proving {\em step simulation}.)  


\begin{figure}
\begin{proof}
\nostep{<1>1}
\step{<1>2}{\assume{$g \in Lt$}
            \prove{$([] OneTraitor) \,/\ \, 
                   LSpec(g) \,/\ \, (:A: h,l :in: Lt: []Inv(h,l))$\\
                    $__=> Hi.LSpec(g).1$}}
\begin{proof}
\setlength{\stepsep}{.5ex}
  \step{<2>1}{$LInit(g) => Hi.LInit(g)$}
  \begin{proof}
    \pf\ By definition of $LInit(g)$.~\qed
  \end{proof}

  \step{<2>2}{$OneTraitor' 
      /\ (:A: h,l :in: Lt : Inv(h,l) /\ Inv(h,l)')
      /\ [Next(g)]_{var(g)}$ \\
    $__ => [Hi.Choose(g) \/ Hi.Fail(g)]_{Hi.var(g)}$}
   \begin{proof}
     \ldots
   \end{proof}

  \qedstep
   \begin{proof}
     \pf\\ 
      $__\begin{noj3}
         \lefteqn{([] OneTraitor) \,/\ \, 
                   LSpec(g) \,/\ \, (:A: h,l :in: Lt: []Inv(h,l))}\\
          & => &  \comment{\{By definition of $LSpec(g)$.\}} \\
          &    &  ([] OneTraitor) /\ LInit(g) /\ [][Next(g)]_{var(g)}
                    /\ (:A: h,l :in: Lt: []Inv(h,l)) \\
          & => &  \comment{\{By simple RTLA reasoning.\}} \\
          &    &  LInit(g) /\ [](
                   \begin{noj}
                     OneTraitor' \\
                      __/\ \,(:A: h,l :in: Lt : Inv(h,l) /\ Inv(h,l)')
                        /\ [Next(g)]_{var(g)})
                   \end{noj}\\
          & => &  \comment{\{By \stepref{<2>1}, \stepref{<2>2} and
                    simple RTLA reasoning.\}} \\
          &    &  Hi.LInit(g) /\ [][Hi.Choose(g) \/ Hi.Fail(g)]_{Hi.var(g)}
\\
          & => &  \comment{\{By definition of $Hi.LSpec(g)$\}} \\
          &    & Hi.LSpec(g).1.___\qed
      \end{noj3}$
   \end{proof}
\end{proof}%%%{<1>2}
\end{proof}%%% of theorem 

\caption[]{The proof of step $\langle1\rangle2$ from 
Figure~\ref{fig:MidCorrectHi}, with the proof of $\langle2\rangle2$ elided.}
\label{fig:MidStep1.2}
\end{figure}


Formally, the first level in the proof of $<<2>>2$ is a case split on
the disjuncts of $[Next(g)]_{var(g)}$.  The only hard case is
$Choose(g)$, which we prove implies $Hi.Choose(g)$.  (In other words,
we prove that a mid-level $Choose(g)$ step implements a high-level
$Hi.Choose(g)$ step.)  The next-level proof of this case is obtained
by separately proving $Hi.Choose(g).1$, \ldots\,, $Hi.Choose(g).4$.
The only hard parts are steps $<<4>>2$ and $<<4>>3$.  The proof of
$<<4>>2$ is given in Figure~\ref{fig:MidStep4.2}; the proof of
$<<4>>3$ is omitted.

\begin{figure}
\begin{proof}
\nostep{<1>1}
\nostep{<1>2}
\begin{proof}
\nostep{<2>1}
\step{<2>2}{$OneTraitor' 
      /\ (:A: h,l :in: Lt : Inv(h,l) /\ Inv(h,l)')
      /\ [Next(g)]_{var(g)}$ \\
    $__ => [Hi.Choose(g) \/ Hi.Fail(g)]_{Hi.var(g)}$}  
\begin{proof}
\pf\ By propositional logic, it suffices to:
\assume{%
    \begin{enumerate}
      \item $OneTraitor'$
      \item $:A: h,l :in: Lt : Inv(h,l) /\ Inv(h,l)'$
      \item $[Next(g)]_{var(g)}$
    \end{enumerate}}
    \prove{$[Hi.Choose(g) \/ Hi.Fail(g)]_{Hi.var(g)}$}
  \step{<3>1}{\case{$Issue(g)$}}
  \begin{proof}
    \pf\ By definition, $Issue(g).3$ equals $\unchanged Hi.var(g)$.~\qed
  \end{proof}
  \step{<3>2}{\case{$:E: h :in: Lt :\: \{g\} : Relay(g, h)$}}
  \begin{proof}
  \pf\ By propositional logic, it suffices to prove that
     $(h :in: Lt) /\ Relay(g, h)$ implies $\unchanged Hi.var(g)$,
%     \[(h :in: Lt) /\ Relay(g, h) => \unchanged Hi.var(g)\]
  which follows from the definitions of $Relay(g,h)$
   and $Hi.var(g)$.~\qed
  \end{proof}
  \step{<3>3}{\case{$Choose(g)$}}
  \begin{proof}
    \step{<4>1}{$\OK(g)  /\ (ord[g] = "?")$}
    \begin{proof}
      \pf\ $Choose(g).1$, which holds by
       Case Assumption \levelref{<3>3}.~\qed
    \end{proof}
    \step{<4>2}{$ord'[g] :in: Order$}
    \begin{proof}
      \ldots
    \end{proof}
    \step{<4>3}{$:A: h :in: Gen : \OK(h)' /\ (ord'[h] # "?") 
                 => (ord'[g] = ord'[h])$}
    \begin{proof}
      \ldots
    \end{proof}
    \step{<4>4}{$\unchanged status[g]$}
    \begin{proof}
      \pf\ $Choose(g).4$, which holds by
       Case Assumption \levelref{<3>3}.~\qed
    \end{proof}
    \qedstep
    \begin{proof}
      \pf\ \stepref{<4>1}--\stepref{<4>4} imply $Hi.Choose(g)$.~\qed
    \end{proof}
  \end{proof}

  \step{<3>4}{\case{$Hi.Fail(g)$}}
  \begin{proof}
    \pf\ Immediate.~\qed
  \end{proof}
  \step{<3>5}{\case{$\unchanged var(g)$}}
  \begin{proof}
    \pf\ By definition, $Hi.var(g)$ is a subsequence of $var(g)$.~\qed
  \end{proof}
  \qedstep
  \begin{proof}
     \pf\ \stepref{<3>1}--\stepref{<3>5} and the
      definition of $Next(g)$.
  \end{proof}
\end{proof}%%%{<2>2}

\end{proof} %%%{<1>2}
\end{proof} %%% of theorem

\caption[]{The proof of step $\langle2\rangle2$ from
Figure~\ref{fig:MidStep1.2}, with the proofs of 
  $\langle4\rangle2$ and $\langle4\rangle3$ elided.}
\label{fig:MidStep2.2}

\end{figure}



\begin{figure}

\begin{proof}
\nostep{<1>1}
\nostep{<1>2}
\begin{noproof}
\nostep{<2>1}
\nostep{<2>2}
\begin{noproof}
\nostep{<3>1}
\nostep{<3>2}
\nostep{<3>3}
\begin{noproof}
\nostep{<4>1}
\step{<4>2}{$ord'[g] :in: Order$}
\begin{proof}
  \step{<5>1}{$rcvd[g] \in [Lt -> Order]$}
    \begin{proof}
      \step{<6>1}{$\domain{rcvd[g]} = Lt$}
      \begin{proof}
        \pf\ \stepref{<4>1} and $Inv(g,g).1$, which holds by 
        Assumption \levelref{<1>2} and Assumption 
        \levelref{<2>2}:2.~\qed
      \end{proof}

      \step{<6>2}{$\A h \in Lt: rcvd[g][h] \neq "?"$}
      \begin{proof}
        \pf\ $Choose(g).2$, which holds by  Assumption 
        \levelref{<3>3}.~\qed
      \end{proof}

      \step{<6>3}{$\A h \in Lt: rcvd[g][h] \in Order$}
      \begin{proof}
        \pf\ \stepref{<6>2} and $Inv(g,h).2$, which holds by 
             \stepref{<4>1}, Assumption \levelref{<1>2}, and 
        Assumption \levelref{<2>2}:2.~\qed
      \end{proof}

      \qedstep
      \begin{proof}
        \pf\ \stepref{<6>1} and \stepref{<6>3}.~\qed
      \end{proof}
   \end{proof}
  \qedstep
  \begin{proof}
    \pf\ $Choose(g).3$ (which holds by  Assumption 
        \levelref{<3>3}), \stepref{<5>1}, and Assumption
    $MidAssump.2$.~\qed
  \end{proof}
\end{proof}%%%{<4>2}
\end{noproof}
\end{noproof}%%%{<2>2}
\end{noproof}%%%{<1>2}
\end{proof}%%% theorem

\caption[]{The proof of step $\langle4\rangle2$ from 
Figure~\ref{fig:MidStep2.2}.}
\label{fig:MidStep4.2}

\end{figure}


Step $<<1>>3$ is a property of the same form as theorem~$SpecGood$.
However, there is a temporal quantifier $:EE:$ in $LSpec(g)$.
Figure~\ref{fig:MidCorrect1.3} indicates how this quantifier is
handled.  We first define $LSpecT(g,t)$ to be $LSpec(g)$ with the
quantifier removed, and define the invariant $TInvT(g,t)$.\footnote{If
  $r$ and $s$ are elements of $Real$, then $r\leq t\leq s$ means $(t\in
  Real)\land (r\leq t)\land (t\leq s)$.} 
The heart of the proof, step $<<2>>1$, asserts an ordinary invariance
property with no temporal quantifiers; its proof is omitted.  Steps
$<<2>>3$ and $<<2>>4$ show how the quantifier is ``put back into the
formula'' using simple reasoning.  Formally, we are using the
following two rules, which are valid if $x$ does not occur free in
$G$: \notla
 \[ \begin{array}[t]{@{}c@{}}
     F(x) \implies G  \\[.3ex] \hline 
    \raisebox{.3ex}{\strut}(\EE x : F(x)) \implies G 
    \end{array}  \s{2}      
  \vdash (\EE  x : F(x) \land G) \equiv (\EE x : F(x)) \land G
 \] \tla
This proof strategy will be familiar to anyone who has done rigorous
proofs in ordinary first-order logic.

\begin{figure}
\begin{proof}
\nostep{<1>1}
\nostep{<1>2}
\step{<1>3}{\assume{$g \in Lt$}
\prove{$(now = Now_0) /\ RT(<<ord,rcvd,status>>) /\ LSpec(g)$\\
       $__/\ \,(:A: h :in: Lt: []Inv(g,h)) => [] TInv(g)$ }}

\begin{proof}
  \pflet{$LSpecT(g, t) ==
      LSpec(g).1  /\ LSpec(g).2  /\ LSpec(g).3  /\ LSpec(g).4(t)$\\
       $TInvT(g,t) ==$ \\
        $__\begin{conj*}
         now \in Real \\
         \begin{noj}
           \OK(g) /\ (ord[g] = "?") /\ (\A h \in Lt: rcvd[g][h] \neq "?") \\
           __ => (now \leq t \leq Now_0 + 2\delta + \epsilon)
         \end{noj}
       \end{conj*}$}
  \step{<2>1}{$(now = Now_0) /\ RT(<<ord,rcvd,status>>) /\ LSpecT(g,t)$\\
       $__/\ \,(:A: h :in: Lt: []Inv(g,h)) => [] TInvT(g,t)$}
  \begin{proof}
  \ldots
  \end{proof}

  \step{<2>2}{$(now = Now_0) /\ RT(<<ord,rcvd,status>>) /\ LSpecT(g,t)$\\
       $__/\ \,(:A: h :in: Lt: []Inv(g,h)) => [] TInv(g)$}
  \begin{proof}
   \pf\ \stepref{<2>1} and simple temporal reasoning, since 
   $TInvT(g,t)$ implies $TInv(g)$.~\qed
  \end{proof}

  \step{<2>3}{$(:EE: t : (now = Now_0) /\ RT(<<ord,rcvd,status>>) 
                /\ LSpecT(g,t)$\\
              $__/\ \,(:A: h :in: Lt: []Inv(g,h))) => [] TInv(g)$}
   \begin{proof}
     \pf\ \stepref{<2>2}, since $t$ does not occur free in 
     $[]TInv(g)$.~\qed
   \end{proof}

  \qedstep
  \begin{proof}
   \pf\ \stepref{<2>3}, since\\
   $__\begin{noj3}
   \lefteqn{ :EE: t : \begin{conj}
             (now = Now_0) /\ RT(<<ord,rcvd,status>>) \\
              LSpecT(g,t)\\
              :A: h :in: Lt: []Inv(g,h))            
             \end{conj}}\\
   & :equiv: & \comment{\{By definition of $LSpecT$.\}}\\
   &         & :EE: t :  \begin{conj}
                          (now = Now_0) /\ RT(<<ord,rcvd,status>>) \\
                          LSpec(g).1  
                            /\ LSpec(g).2  /\ LSpec(g).3  /\ LSpec(g).4(t)\\
                          :A: h :in: Lt: []Inv(g,h)
               \end{conj}\\
   & :equiv: & \comment{\{Because $t$ occurs free only in $LSpecT(g).4$.\}}\\
   &         & \begin{conj}
                          (now = Now_0) /\ RT(<<ord,rcvd,status>>) \\
                           LSpec(g).1 /\ LSpec(g).2  /\ LSpec(g).3  
                       /\ :EE: t : LSpec(g).4(t) \\
                          :A: h :in: Lt: []Inv(g,h)
               \end{conj}\\
   & :equiv: & \comment{\{By definition of $LSpec$.\}}\\
   &         & \begin{conj}
                          (now = Now_0) /\ RT(<<ord,rcvd,status>>) \\
                         LSpec(g) \\
                          :A: h :in: Lt: []Inv(g,h)___\qed
               \end{conj}
   \end{noj3}$
\end{proof}
\end{proof}

\end{proof}

\caption[]{The proof of $\langle1\rangle3$ from
Figure~\ref{fig:MidCorrectHi}, with the proof of $\langle2\rangle1$ elided.}
\label{fig:MidCorrect1.3}
\end{figure}

The proof of step $<<1>>4$ is a simple matter of deducing
 $([]P_1) /\ ([]P_2) /\ ([]P_3) => []Q$ 
from 
  $P_1 /\ P_2 /\ P_3 => Q$, 
where $[]P_1$ and $[]P_2$ are $LSpec(g).2$ and $LSpec(g).3$,
respectively.  The proof of step $<<1>>5$ uses the same basic strategy
as the proof of $<<1>>2$, but is much simpler.  The formal proofs of
these steps are omitted.


%try

\subsection{Proof of Theorem {\it LowCorrect}}

%\noindent
%\rule{\textwidth}{1pt}

The high-level proof of theorem $LowCorrect$ appears in
Figure~\ref{fig:LowCorrectHi}.  As in the proof of theorem
$MidCorrect$, we first prove the implication with the quantifiers
removed from the hypothesis, and then add the quantifiers in the final
step.  

The proof of the final step, $<<1>>6$, is shown in
Figure~\ref{fig:LowCorrect1.6}.  To prove step $<<2>>2$, we 
use the same reasoning as before to add the quantifiers.  The proof
of step $<<2>>3$ makes use of a TLA proof rule that is analogous to
the rule
  \[ |- (:A: y : :E: x : F(x)) :equiv: (:E: x : :A: y : F(x(y)))\]
of higher-order logic.  In a formalism like \TLA+ that includes set
theory, functions are ordinary values, and this rule can be stated in
first-order logic as
  \[ |- (:A: y :in: S : :E: x : F(x)) :equiv: 
     (:E: x : :A: y :in: S : F(x[y]))
 \]
(The range $S$ is needed because the domain of a function must be a
set.)  If the ordinary existential quantifier $:E:$ is replaced by the
temporal quantifier $:EE:$, the rule remains sound in general only if
$S$ is finite.\footnote{The rule is unsound for an infinite set $S$
  because $\EE$ is defined so $\EE x:F$ is invariant under stuttering.
  It is sound for the operator $\EE$ of Manna and
  Pnueli~\cite{manna:temporal}, which does not preserve invariance under
  stuttering.}

\begin{figure}
{\bf Theorem}\s{1}$Spec => Mid.Spec$
\begin{proof}
\pflet{$
\begin{noj}
qt, ct, t_1, t_2, t_3, t_4, t_5, t_6 : \variable\\
%
    TEMax(t, g, A) == VTimer(t, A, \epsilon, lvar(g)) /\ MaxTimer(t)\\
%
CSpecT ==
        \begin{conj*}
        CInit /\ [] [CNext]_{cvar} \\
        \A g \in Lt: TEMax(ct[g], Cmdr, CSend(g))
        \end{conj*}\\
%
LSpecT(g) ==
        \begin{conj*}
        LInit(g) /\ [] [LNext(g)]_{lvar(g)} \\
        TEMax(t_1[g], g, Issue(g))  \\
        TEMax(t_2[g], g, IssueTimeout(g)) \\
        TEMax(t_3[g], g, Choose(g))  \\
        \begin{noj}
        \A h \in Lt \setminus \{g\}: \\
           __\begin{conj}
               TEMax(t_4[g][h], g, Send(g,h)) \\
               TEMax(t_5[g][h], g, Relay(g,h)) \\
               TEMax(t_6[g][h], g, RelayTimeout(g,h))
             \end{conj}
        \end{noj}
        \end{conj*}\\      
%
TCSpecT(g,h) == 
 \begin{noj}
   TC(g,h).Spec.1\, /\ \,TC(g,h).Spec.2 \\
   __/\ \, TC(g,h).Spec.3(qt[g][h]) 
  \end{noj}\\
%
CInv(g) == \ldots\\
LInv(g, h) == \ldots
\end{noj}$}
\step{<1>1}{$CSpec => Mid.Hi.CSpec$}

\step{<1>2}{
   \assume{$g \in Lt$}
   \prove{$\begin{noj}
           \begin{conj}
             CSpecT   /\ LSpecT(g) \\
             TCSpecT(Cmdr,g) \\
             (now = Now_0) /\ RT(<<ord, rcvd, in, out, status, sent>>)
           \end{conj} \\
           => [] CInv(g)
           \end{noj}$}}

\step{<1>3}{
   \assume{\begin{enumerate}
       \item $g, h \in Lt$
       \item $g # h$
       \end{enumerate}}
   \prove{$\begin{noj}
           \begin{conj}
             LSpecT(g)   /\ LSpecT(h) \\
             TCSpecT(g,h) \\
             (now = Now_0) /\ RT(<<ord, rcvd, in, out, status, sent>>) \\
             [] CInv(g)
           \end{conj} \\
           => [] LInv(g,h)
           \end{noj}$}}

\step{<1>4}{%
  \assume{$g \in Lt$}
  \prove{$LSpec(g) \, /\ \, [] CInv(g) \, /\ \, 
           [](\A h \in Lt :\: \{g\}: LInv(h,g)) \\
          __=> Mid.LSpec(g)$}}

\step{<1>5}{$RT(<<ord,rcvd,in,out,status>>) => RT(<<ord,rcvd,status>>)$}

\qedstep
\end{proof}
\caption[]{The high-level proof of theorem $LowCorrect$.}
\label{fig:LowCorrectHi}
\end{figure}

\begin{figure}
\begin{proof}
\nostep{<1>1}
\nostep{<1>2}
\nostep{<1>3}
\nostep{<1>4}
\nostep{<1>5}
\qedstep
\begin{proof}
  \step{<2>1}{$\begin{conj}
     CSpec \\
     CSpecT\\
     :A: g :in: Lt : LSpecT(g)\\
     :A: g, h :in: Gen : TCSpecT(g, h)\\
     RT(<<ord, rcvd, in, out, status, sent>>)\\
     now = Now_0 
    \end{conj}$\\
    $=> Mid.Spec$}
  \begin{proof}
    \pf\ \stepref{<1>1}--\stepref{<1>5} and the definition of
    $Mid.Spec$.~\qed
  \end{proof}
\step{<2>2}{$
  \begin{conj}
    CSpec \\
     :EE: ct : CSpecT\\
     :EE: t_1, t_2, t_3, t_4, t_5, t_6 : :A: g :in: Lt : LSpecT(g)\\
     :EE: qt : :A: g, h :in: Gen : TCSpecT(g, h)\\
     RT(<<ord, rcvd, in, out, status, sent>>)\\
     now = Now_0 
  \end{conj}$\\
    $=> Mid.Spec$}
  \begin{proof}
    \pf\ \stepref{<2>1}, since $ct$ occurs only in $CSpecT$,
    $t_1$, $t_2$, $t_3$, $t_4$, $t_5$, and $t_6$ occur only in
     $LSpecT(g)$, and
     $qt$ occurs only in $TCSpecT(g, h)$.~\qed
  \end{proof}

\step{<2>3}{\begin{enumerate}
   \item $(:EE: ct : CSpecT) :equiv: CSpec$            
   \item $(:EE: t_1, t_2, t_3, t_4, t_5, t_6 : :A: g :in: Lt : LSpecT(g))
            :equiv: :A: g :in: Lt : LSpec(g)$
   \item $(:EE: qt : :A: g, h :in: Gen : TCSpecT(g, h)) :equiv: 
               :A: g, h :in: Gen : TC(g, h).Spec$
  \end{enumerate}}
  \begin{proof}
    \pf\ $Lt$ is finite
      by assumption $HiAssump.1$ from module $SpecParams$
      (imported via module $MidLevel$), and 
      $:EE: x : :A: v :in: S : F(x[v])$ is equivalent to
      $:A: v :in: S : :EE: x : F(x)$, for any finite
      set $S$ and temporal operator $F(:?:)$.~\qed
  \end{proof}
  \qedstep
   \begin{proof}
   \pf\ \stepref{<2>2}, \stepref{<2>3}, and the definition of
   $Spec$.~\qed
   \end{proof}
\end{proof}
\end{proof}

\caption[]{The proof of step $\langle1\rangle6$ from 
Figure~\ref{fig:LowCorrectHi}.}
\label{fig:LowCorrect1.6}
\end{figure}

We now return to the high-level proof of the theorem.  The proof of
step $<<1>>1$ is simple and is omitted.  The proofs of $<<1>>2$ and
$<<1>>3$ are straightforward invariance arguments.  The invariants,
$CInv(g)$ and $LInv(g,h)$, are defined in Figure~\ref{fig:LowInv}.
Because the invariants are a bit long, the proofs of $<<1>>2$ and
$<<1>>3$ are rather tedious; they are omitted.


\begin{figure}
\begin{proof}
\pflet{$
\begin{noj}
r(g,h) == \IF{rcvd[g][h] = "?"} \THEN <<>>
                                \ELSE <<rcvd[g][h]>> \FI \\
%
c(g,h) == in[h][g][1] :circ: out[g][h][1]\\
%
cOrd(g) == r(g,g) :circ: c(Cmdr,g)\\
%
lOrd(g,h) == r(g, h) :circ: c(h,g)\\
%
CInv(g) == \\
   __\begin{conj*}
       \begin{noj}
       \OK(Cmdr) /\ \OK(g) =>\\       %1
        __\begin{disj}
            (cOrd(g) = <<>>) /\ NotSent(Cmdr,g)  \\
            (cOrd(g) = <<ord[Cmdr]>>) /\ ~NotSent(Cmdr,g)
          \end{disj} 
       \end{noj}\\
     \OK(g) /\ (rcvd[g][g] = "?") => \A h \in Lt: NotSent(g,h)  \\ %2
     \OK(Cmdr) /\ NotSent(Cmdr,g) 
         => (now \leq ct[g] \leq Now_0 + \epsilon) \\ %3
     \begin{noj}
       \OK(g) /\ \OK(Cmdr) /\ (out[Cmdr][g][1] \neq <<>>)    \\ %4
         __ => (now \leq qt[Cmdr][g] \leq Now_0 + \tau + \epsilon)
     \end{noj}   \\ 
     \begin{noj}
       \OK(g) /\ \OK(Cmdr) /\ (in[g][Cmdr][1] \neq <<>>)    \\     %5
         __ => (now \leq t_1[g] \leq Now_0 + \tau + 2*\epsilon)  
     \end{noj} \\
     \begin{noj}
       \OK(g)    /\ (rcvd[g][g] = "?") 
             /\ (Now_0 + \tau + 2*\epsilon < now)      \\    %6
        __ => (now \leq t_2[g] \leq Now_0 + \tau + 3*\epsilon)
      \end{noj}  \\
      now \in Real                               %7
    \end{conj*} \\
%
LInv(g,h) == \\
__\begin{conj*}
    \begin{noj}
       \OK(g) /\ \OK(h) \\  %1
       __=> \begin{disj}
               (lOrd(h,g) = <<>>) /\ NotSent(g,h) \\
               (lOrd(h,g) = <<rcvd[g][g]>>) /\ ~NotSent(g,h)
            \end{disj}     
    \end{noj} \\
   \begin{noj}
     \OK(g) /\ (rcvd[g][g] \neq "?") /\ NotSent(g,h)  \\    %2
     __ => (now \leq t_4[g][h] \leq Now_0 + \tau + 4*\epsilon) 
   \end{noj}  \\
   \begin{noj}
     \OK(g) /\ \OK(h) /\ (out[g][h][1] # <<>>)     \\ %3
     __ => (now \leq qt[g][h] \leq Now_0 + 2*\tau + 4*\epsilon) 
   \end{noj}  \\ 
   \begin{noj}
     \OK(g) /\ \OK(h) /\ (in[h][g][1] # <<>>)     \\  %4
     __ => (now \leq t_5[h][g] \leq Now_0 + 2*\tau + 5*\epsilon)
   \end{noj}    \\
   \begin{noj}
     \OK(h)    /\ (rcvd[h][g] = "?") 
           /\ (now > Now_0 + 2*\tau + 5*\epsilon)  \\ %5
     __ => (now \leq t_6[h][g] \leq Now_0 + 2*\tau + 6*\epsilon)
   \end{noj}
   \end{conj*}\\
%
\end{noj}$}
\end{proof}

\caption[]{The invariants for the proof of theorem {\it LowCorrect}.}
\label{fig:LowInv}
\end{figure}

Step $<<1>>4$ introduces a new problem---proving an implication whose
conclusion contains a $:EE:$.  We now examine its proof, which is
outlined in Figure~\ref{fig:LowCorrect1.4}.

Step $<<2>>1$ is an implication of the form we've seen before.  The
major part of its proof consists of proving step simulation.  The
proof is straightforward but tedious, taking about two pages.  

Steps $<<2>>2$ and $<<2>>3$ have the form $[]P => []Q$, which is
proved by showing that $P$ implies $Q$.  These proofs are easy.

Step $<<2>>4$ is where the $\EE$ appears in the conclusion.  In
first-order logic, one proves that $F(x)$ implies
 $:E: y : G(x, y)$ by instantiating $y$---that is, finding
an expression $h(x)$ such that $F(x)$ implies $G(x, h(x))$.  The same
technique is used with the temporal quantifier $:EE:$, where the
instantiation is called a {\em refinement
mapping\/}~\cite{abadi:existence}.  To prove $<<2>>4$, we must
instantiate the timer variable $t$ used to express the timing
constraint on $Mid.Choose$.  The instantiation is simple---we
instantiate $t$ with the timer variable for the low-level $Choose$
action.  Step $<<3>>1$ has a familiar form, since $VTimer(\ldots)$ has
the form $Init /\ [][Next]_v$; its proof is simple.

\begin{figure}
\begin{proof}
\nostep{<1>1}
\nostep{<1>2}
\nostep{<1>3}
\step{<1>4}{%
  \assume{$g \in Lt$}
  \prove{$LSpec(g)\, /\ \,[] CInv(g)\, /\ \,
            [](\A h \in Lt :\: \{g\}: LInv(h,g))\\__ => Mid.LSpec(g)$}}

\vspace{.5ex}
\begin{proof}
  \step{<2>1}{$LSpec(g).1\, /\ \,[] CInv(g) 
            \, /\ \,[](\A h \in Lt :\: \{g\}: LInv(h,g)) \\
          __=> Mid.Init(g) /\ [][Mid.Next(g)]_{Mid.var(g)}$}
  \begin{proof}
    \ldots
  \end{proof}

  \step{<2>2}{$[] CInv(g) => 
          [] (\OK(g) /\ (rcvd[g][g] = "?") => (now \leq Now_0 + \delta))$}

  \begin{proof}
    \ldots
  \end{proof}

  \step{<2>3}{$[] LInv(h,g) => 
                 [] (\OK(g) /\ (rcvd[g][h] = "?") => 
                       (now \leq Now_0 + 2*\delta))$}

  \begin{proof}
    \ldots
  \end{proof}

  \step{<2>4}{$\begin{noj}
               [][LNext(g)]_{lvar(g)} /\ EMax(g,Choose(g))  \\
               __ => \EE t: VTimer(t, Mid.Choose(g), \epsilon, Mid.var(g)) 
                            /\ MaxTimer(t)
               \end{noj}$}
  \begin{proof}
    \step{<3>1}{$[] [LNext(g)]_{lvar(g)} 
                  /\ VTimer(t, Choose(g), \epsilon, lvar(g)) \\
                     __=> VTimer(t, Mid.Choose(g), \epsilon, Mid.var(g))$}
     \begin{proof}
       \ldots
     \end{proof}

    \step{<3>2}{$
        \begin{conj}
           [] [LNext(g)]_{lvar(g)} \\
           VTimer(t, Choose(g), \epsilon, lvar(g)) /\ MaxTimer(t)
        \end{conj}\\
        =>\, :EE: t : VTimer(t, Mid.Choose(g), \epsilon, Mid.var(g))
                      /\ MaxTimer(t)$}
    \begin{proof}
      \pf\ \stepref{<3>1}.~\qed
    \end{proof}

    \step{<3>3}{$
        \begin{conj}
           [] [LNext(g)]_{lvar(g)} \\
           :EE: t : VTimer(t, Choose(g), \epsilon, lvar(g)) /\ MaxTimer(t)
        \end{conj}\\
        =>\, :EE: t : VTimer(t, Mid.Choose(g), \epsilon, Mid.var(g))
                        /\ MaxTimer(t)$}
    \begin{proof}
      \pf\ \stepref{<3>2}, since $t$ does not occur free in
       $[] [LNext(g)]_{lvar(g)}$ or $:EE: t : \ldots$\,.~\qed
    \end{proof}

    \qedstep
     \begin{proof}
       \pf\ \stepref{<3>2} and the definition of $EMax(g,Choose(g))$.~\qed
     \end{proof}
  \end{proof}
  

  \qedstep
  \begin{proof}
    \pf\ \stepref{<2>1}--\stepref{<2>4} 
    and the definition of $Mid.LSpec(g)$.~\qed
  \end{proof}
\end{proof}
\end{proof}
\caption[]{The proof of step $\langle1\rangle4$ from
Figure~\ref{fig:LowCorrectHi}, with most steps elided.}
\label{fig:LowCorrect1.4}
\end{figure}

The one remaining step in the high-level proof of the theorem is
$<<1>>5$.  It is easy, and is omitted.

%try
\section{Discussion} \label{sec:discussion}

Because the algorithm and its informal specification were well
understood, writing the formal specifications was a straightforward
exercise.  As expected, we discovered small mistakes in the initial
versions while writing the proofs.  Our specifications were not
subject to mechanical checking, so they probably still contain
typographical errors.  We would like to say that any such errors are
minor, but with modern text editors and typesetting systems, one
careless keystroke can produce major mistakes.


We have used a specification style different from our customary one.
We usually write {\em interleaving\/} specifications, in which events
in different processes are represented by separate
steps~\cite{abadi:conjoining}.  Here, we have written {\em
noninterleaving\/} specifications that allow individual steps which 
represent actions in two or more processes.  For example, the formula
$Spec$ of module $MidLevel$ allows behaviors in which a single step is
both an $Issue(g)$ step of lieutenant $g$ and a $Relay(h,g)$ step of
a different lieutenant $h$.  Writing noninterleaving specifications
introduced no new problems.

Writing the proofs was also a straightforward exercise.  As is typical
when reasoning about real time, our specifications are safety
properties; there are no liveness properties.  When proving safety
properties, creativity is required only in finding the invariants.
With practice, writing invariants becomes second nature.  The rest of
the proof is a standard process of applying simple TLA proof rules and
using the structure of the formulas to decompose the resulting proof
obligations.

Writing this kind of proof is an exercise in organizing a complex
structure.  It is very much like programming; it is completely
different from what mathematicians do when they write proofs.  All the
steps in our proof are mathematically trivial.  Hierarchically
structured proofs are long and tedious, but they are the only kind of
hand proofs that can be trusted.  There are no shortcuts.  Short
proofs are short because they gloss over details that have to be
checked to avoid errors.

These proofs are amenable to mechanical verification.  Most steps can
be checked with the TLP verification system~\cite{engberg:mechanical}.
However, for this type of reasoning, which cannot be checked by
finite-state methods, mechanical theorem proving still seems to be
considerably more work than writing a hand proof.  The hierarchical
proof style makes it possible to reduce the probability of errors in
hand proofs to an acceptable level.

Our specifications are written in \TLA+.  The flexibility of \TLA+ is
indicated by the ease with which real-time properties are expressed,
even though the language has no special primitives for time.  We use
the same $RealTime$ module for specifying Byzantine generals that was
used in~\cite{lamport:hybrid} for specifying a gas burner.  This kind
of flexibility and modularity are characteristic of an engineering
discipline.

Our proofs use the logic TLA\@.  They are completely formal.  Although
most of the lower-level steps were omitted, the parts that we did
present in detail show that all the proofs can be carried out to the
level of simple propositional reasoning.  The proofs are seamless.
The theorems to be proved are mathematical formulas, and at each step
we are proving a mathematical formula.  There is no switching from
programs to logic; there is no appeal to semantic understanding.
Hierarchically decomposing a large problem into smaller ones by the
use of simple mathematical rules is characteristic of an engineering
discipline.

We believe that formal specification and proof is now feasible for
high-level designs of real systems.  They are not yet feasible for
reasoning at the level of executable code, except in special
applications or for small parts of a system.  It may appear that it is
difficult to reason about code because our specifications are logical
formulas rather than programs.  However, the primary issue is not one
of language but of complexity.  It is hard to reason about real
programs because they are complicated.  Formal reasoning is generally
applied only to concurrent programs written in toy languages like
CSP~\cite{hoare:csp-book} and Unity~\cite{chandy:parallel}.  A program
in a toy language is no closer to a real program than is a TLA
formula.  Further work is needed before formal reasoning about
executable code becomes routine.


\bibliographystyle{plain}
%\bibliography{mybib}

\begin{thebibliography}{10}

\bibitem{abadi:existence}
Mart\'{\i}n Abadi and Leslie Lamport.
\newblock The existence of refinement mappings.
\newblock {\em Theoretical Computer Science}, 82(2):253--284, May 1991.

\bibitem{abadi:old-fashioned}
Mart\'{\i}n Abadi and Leslie Lamport.
\newblock An old-fashioned recipe for real time.
\newblock Research Report~91, Digital Equipment Corporation, Systems Research
  Center, 1992.
\newblock An earlier version, without proofs, appeared in \cite[pages
  1--27]{debakker:real-time}.

\bibitem{abadi:conjoining}
Mart\'{\i}n Abadi and Leslie Lamport.
\newblock Conjoining specifications.
\newblock Research Report 118, Digital Equipment Corporation, Systems Research
  Center, 1993.
\newblock To appear in {\em ACM Transactions on Programming Languages and
  Systems}.

\bibitem{ashcroft:proving}
E.~A. Ashcroft.
\newblock Proving assertions about parallel programs.
\newblock {\em Journal of Computer and System Sciences}, 10:110--135, February
  1975.

\bibitem{chandy:parallel}
K.~Mani Chandy and Jayadev Misra.
\newblock {\em Parallel Program Design}.
\newblock Addison-Wesley, Reading, Massachusetts, 1988.

\bibitem{debakker:real-time}
J.~W. de~Bakker, C.~Huizing, W.~P. de~Roever, and G.~Rozenberg, editors.
\newblock {\em Real-Time: Theory in Practice}, volume 600 of {\em Lecture Notes
  in Computer Science}.
\newblock Springer-Verlag, Berlin, 1992.
\newblock Proceedings of a REX Real-Time Workshop, held in The Netherlands in
  June, 1991.

\bibitem{engberg:mechanical}
Urban Engberg, Peter Gr\o{}nning, and Leslie Lamport.
\newblock Mechanical verification of concurrent systems with {TLA}.
\newblock In {\em Computer-Aided Verification}, Lecture Notes in Computer
  Science, Berlin, Heidelberg, New York, June 1992. Springer-Verlag.
\newblock Proceedings of the Fourth International Conference, CAV'92.

\bibitem{hoare:csp-book}
C.~A.~R. Hoare.
\newblock {\em Communicating Sequential Processes}.
\newblock Series in Computer Science. Prentice-Hall International, London,
  1985.

\bibitem{kurki-suonio:operational}
Reino Kurki-Suonio.
\newblock Operational specification with joint actions: Serializable databases.
\newblock {\em Distributed Computing}, 6(1):19--37, 1992.

\bibitem{lam:protocol}
Simon~S. Lam and A.~Udaya Shankar.
\newblock Protocol verification via projections.
\newblock {\em IEEE Transactions on Software Engineering}, SE-10(4):325--342,
  July 1984.

\bibitem{lam:specifying}
Simon~S. Lam and A.~Udaya Shankar.
\newblock Specifying modules to satisfy interfaces: A state transition system
  approach.
\newblock {\em Distributed Computing}, 6(1):39--63, 1992.

\bibitem{lamport:specifying}
Leslie Lamport.
\newblock Specifying concurrent program modules.
\newblock {\em ACM Transactions on Programming Languages and Systems},
  5(2):190--222, April 1983.

\bibitem{lamport:newtla}
Leslie Lamport.
\newblock The temporal logic of actions.
\newblock Research Report~79, Digital Equipment Corporation, Systems Research
  Center, December 1991.
\newblock To appear in {\em ACM Transactions on Programming Languages and
  Systems}.

\bibitem{lamport:howtoprove}
Leslie Lamport.
\newblock How to write a proof.
\newblock Research Report~94, Digital Equipment Corporation, Systems Research
  Center, February 1993.
\newblock To appear in {\em American Mathematical Monthly}.

\bibitem{lamport:hybrid}
Leslie Lamport.
\newblock Hybrid systems in {TLA}$^{+}$.
\newblock In Robert~L. Grossman, Anil Nerode, Anders~P. Ravn, and Hans Rischel,
  editors, {\em Hybrid Systems}, volume 736 of {\em Lecture Notes in Computer
  Science}, pages 77--102, Berlin, Heidelberg, 1993. Springer-Verlag.

\bibitem{lamport:byzantine}
Leslie Lamport, Robert Shostak, and Marshall Pease.
\newblock The {Byzantine} generals problem.
\newblock {\em ACM Transactions on Programming Languages and Systems},
  4(3):382--401, July 1982.

\bibitem{lynch:hierarchical}
Nancy Lynch and Mark Tuttle.
\newblock Hierarchical correctness proofs for distributed algorithms.
\newblock In {\em Proceedings of the Sixth Symposium on the Principles of
  Distributed Computing}, pages 137--151. ACM, August 1987.

\bibitem{manna:temporal}
Zohar Manna and Amir Pnueli.
\newblock {\em The Temporal Logic of Reactive and Concurrent Systems}.
\newblock Springer-Verlag, New York, 1991.

\bibitem{misra:proofs}
Jayadev Misra and K.~Mani Chandy.
\newblock Proofs of networks of processes.
\newblock {\em IEEE Transactions on Software Engineering}, SE-7(4):417--426,
  July 1981.

\bibitem{neumann:highly-dependable}
Peter~G. Neumann and Leslie Lamport.
\newblock Highly dependable distributed systems.
\newblock Technical report, SRI International, June 1983.
\newblock Contract Number DAEA18-81-G-0062, SRI Project 4180.

\end{thebibliography}

\newpage
%try


\begin{figure}
\begin{module}{FiniteSets\expref{Reals}}
\IMPORT Naturals\\
\midbar
\begin{nodecls}
HasCardinality(n, S) == 
  \LET Q == \{i :in: Nat : i < n\}
  \IN \begin{conj}      
      n :in: Nat \\
      \begin{noj}
        :E: f :in: [Q -> S] : \\
         __\begin{conj}
            :A: s :in: S : :E: q :in: Q : f[q] = s \\
            :A: q1, q2 :in: Q : (f[q1] = f[q2]) => (q1 = q2)
           \end{conj}
      \end{noj}
      \end{conj}
   \NI \\
IsFiniteSet(S) == :E: n :in: Nat : HasCardinality(n, S)
\end{nodecls}
\end{module}

\vspace{-12.5pt}

\begin{module}{Sequences\expref{tuple}}
\IMPORT Naturals
\midbar
\begin{nodecls}
OneTo(n) == \{ i :in: Nat : (1 :leq: i) /\ (i :leq: n)\}\\
Len(s) == \choose n : (n :in: Nat) /\ (\domain s) = OneTo(n)\\
Head(s) == s[1]\\
Tail(s) == [i :in: OneTo(Len(s)-1) |-> s[i+1]]\\
(s) :O: (t) == [i :in: OneTo(Len(s)+Len(t)) |->
                 \IF{i :leq: Len(s)} \THEN s[i] \\
                                        \ELSE t[i - Len(s)] ] \FI
\end{nodecls}
\end{module}

\vspace{-12.5pt}

\begin{module}{RealTime}
\IMPORT Reals
\begin{nodecls}
{\bf parameters} \s{1}
  \= now  : \variable\\
  \> :oo: : \constant
\end{nodecls}
\midbar
\begin{decls}{assumption}
  InfinityUnReal == :oo: :notin: Real
\end{decls}
\midbar
\begin{nodecls}
  RT(v)\expref{RT} ==
     \begin{conj}
      now :in: Real\\
      :Box: [ \begin{conj}
               now' :in: \{r :in: Real : now < r \}\\
               v' = v \s{.5}]_{now}
            \end{conj}
     \end{conj} \V{.4}
%
VTimer(x, A, :delta:, v )  ==
   \begin{conj}
       x =  \IF{\enabled <<A>>_v} \THEN now + :delta:       
                                  \ELSE :oo:           \FI      \\
%
      :Box: [x' = 
         \IF{(\enabled <<A>>_v)'}  \\
            \THEN \IF{\suggest{<<A>>_v \/ ~\enabled <<A>>_v}{<<A>>_v}} 
                        \THEN now' + :delta:        \\
                        \ELSE x             \FI    \\
            \ELSE :oo:__]_{<<x, v>>}          \FI
   \end{conj}                                                \V{.8}
%
MaxTimer(x) == 
       :Box:[(x :neq: :oo:) => (now' :leq:  x)]_{now}\V{.4}
%
MinTimer(x,A, v) == 
  :Box:[\suggest{A}{<<A>>_v} => (now :geq: x)]_{v}
\end{nodecls}  

\end{module}

\vspace{-5pt}

\caption[]{The modules $FiniteSets$, $Sequences$, and $RealTime$.}% 
\label{fig:FiniteSets}%
\label{fig:Sequences}%
\label{fig:RealTime}
\end{figure}
%try

\begin{figure}
\begin{description}

\item[assumption]
  %\mbox{}\\
Begins a sequence of assumptions that must be true of the constant
parameters when the module is included in another
module.\expref{assumption}

\vspace{.5\baselineskip}
  

\item[\constant]
  %\mbox{}\\
  Specifies a parameter's sort.\expref{constant}

\vspace{.5\baselineskip}

\item[definitions]
  %\mbox{}\\
Begins a sequence of definitions.  This keyword may be omitted or
replaced by one of the keywords {\bf action}, {\bf boolean}, {\bf
constant}, {\bf predicate}, {\bf state function}, {\bf temporal}, or
{\bf transition function} to denote the sort of the symbols being
defined.  
 

\vspace{.5\baselineskip}

\item[export]   %\mbox{}\\
  Specifies definitions visible to importing and including
  modules.\expref{export} 

\vspace{.5\baselineskip}

\item[import]   %\mbox{}\\
  Appends parameters, assumptions, definitions, and theorems of 
              another module.\expref{import} 

\vspace{.5\baselineskip}

\item[include \ldots\ as $\ldots\;$with]   %\mbox{}\\
  Appends definitions, assumptions (as theorems), and theorems of
   another module, with instantiations for its 
parameters.\expref{IncludeHi}\,\expref{param.include}

\vspace{.5\baselineskip}

\item[module]    %\mbox{}\\
  Begins a module.\expref{module}

\vspace{.5\baselineskip}

\item[parameters]   %\mbox{}\\
  Declares the free parameters of a module.\expref{parameter}

\vspace{.5\baselineskip}

\item[theorem] %\mbox{}\\
  Begins a sequence of theorems.  (They must be provable from the
  module's assumptions and the rules of first-order logic, set theory, and 
  TLA.)

\vspace{.5\baselineskip}

\item[\variable]
  %\mbox{}\\
  Specifies a parameter's sort.\expref{constant}

\vspace{.5\baselineskip}

\item[$\deq$]
  %\mbox{}\\
  Defines an operator.\expref{==} 

\vspace{.5\baselineskip}


\makeatletter
\item[%
{\makeatletter\@computerule\makebox[4.5em][l]{\s{.5}\midbar\s{1}}}]
  %\mbox{}\\
  A mostly meaningless decoration that ends the scope of an
  {\bf assumption} or {\bf theorem} section.\expref{midbar}

\vspace{.5\baselineskip}

\item[{\makeatletter
    \@computerule\raisebox{-.5ex}{\makebox[4.5em]{\s{.5}\tlabotline\s{1}}}}]%
  %\mbox{}\\
  Marks the end of a module.\expref{tlabotline}
\end{description}

\vspace{-\baselineskip}

\caption[]{The syntactic keywords and symbols of \TLA+.}
\label{fig:keywords}
\end{figure}


\begin{figure}
\centering
\begin{tabbing}
\hspace*{1em}\=\+\kill
\bf \hspace*{-1em}Predicate and Action Operators\\
$\unchanged e$ \hspace{.5em} \=\kill
$p'$       \>     \small [$p$ true in final state of step] \\
$[A]_e$    \>    \small [$A \/ (e'=e)$]\expref{SquareSub} \\
$<<A>>_e $ \>    \small [$A /\ (e' \neq e)$] \\
$\enabled A$ \>  \small [An $A$ step is possible] \\
$\unchanged e$ \> \small [$e'=e$]\expref{unchanged} \\
$A\cdot B$   \>  \small [Composition of actions]\\[.5\baselineskip]
%
\bf \hspace*{-1em}Temporal Operators\\
$F ~> G$ \hspace{.5em} \=\kill
$[]F$    \> \small [$F$ is always true]\expref{Box} \\
$<>F$    \> \small  [Eventually: $~[]~F$] \\
WF$_{e}(A)$ \> \small [Weak fairness:
                           $[]<><<A>>_e \/ []<>~\enabled A$]\\
SF$_{e}(A)$ \> \small [Strong fairness:
                           $[]<><<A>>_e \/ <>[]~\enabled A$]\\
$F ~> G$ \> \small [Leads to: $[](F => <>G)$] \\ 
%
$:EE: x : F$ \>
    \small [Temporal existential quantification (hiding).]\expref{EE}
\end{tabbing}
\vspace{-\baselineskip}

\caption[]{The nonconstant operators of \TLA+.}
\label{fig:conconstant-ops}
\end{figure}


\begin{figure}[tp]
% \renewcommand{\bnf}[1]{\mbox{\small $\langle\mbox{\it #1\/}\rangle$}}
\centering
\begin{tabbing}
\hspace*{1em}\=\+\kill
\bf \hspace*{-1em}Logic\\
%$\forall\, x : \mbox{\small $[\gram{BOOL} | \ldots | \gram{TEMPORAL}]$} 
%   \,:\, p$   \hspace{.5em}\=\kill
%
\true \ \ \false \ \ $\land$ \ \ $\lor$ 
  \ \ $\lnot$ 
  \ \ $\implies$ \ \ $\equiv$ \\
$\forall\, x : p$  \ \ \ \ $\exists\, x : p$  \ \ \ \ 
$\forall\, x \in S : p$  \ \ \ \ $\exists\, x \in S : p$\\ 
% \ \ \ \ 
 \choose $x : p$
   \hspace{.5em} \small [Equals some $x$ satisfying $p$] 
\\[.5\baselineskip]
%
{\bf \hspace*{-1em}Sets}\\
$=$ \ \ $\neq$ \ \ $\in$ \ \ $\notin$ 
  \ \ $\cup$ \ \ $\cap$ \ \ $\subseteq$ \ \ 
  $:\:$ {\small [set difference]}\\
$\{e_1, \ldots , e_n\}$ \hspace{.5em}\= \kill
%
$\{e_1, \ldots , e_n\}$     
  \> \small [Set consisting of elements $e_i$] \\
$\{x \in S : p\}$       
  \> \small [Set of elements $x$ in $S$ satisfying $p$] \\
$\{e : x \in S \}$       
  \> \small [Set of elements $e$ such that $x$ in $S$] \\
\SUBSET $S$
  \> \small [Set of subsets of $S$] \\
$\union S$
  \> \small [Union of all elements of $S$]\\[.5\baselineskip]
%
{\bf \hspace*{-1em}Functions}\\
{[}$f \except ![e_{1}]\,=\,e_{2}$]
  \hspace{.5em}\= \kill
$f$[$e$] \>
  {\small [Function application]\expref{OK}  }\\
\domain $f$ \> \small [Domain of function $f$] \\
{[}$x \in S$~$\mapsto$\ $\!e$]
  \> \small [Function $f$ such that $f[x]=e$ for $x\in S$]\expref{MidLInit}\\
{[}$S$ $\rightarrow$ $T$]
  \> \small [Set of functions $f$ with $f[x]\in T$ for 
             $x\in S$]\expref{FcnSet}            \\
{[}$f \except ![e_{1}]\,=\,e_{2}$]
  \> \small [Function $\widehat{f}$ equal to $f$ except 
             $\widehat{f}[e_{1}]=e_{2}$]\expref{MidIssue}\\
{[}$f \except ![e] :in: S$]
  \> \small [Set of functions $\widehat{f}$ equal to $f$ except 
             $\widehat{f}[e]\in S$]\\[.5\baselineskip]
%
{\bf \hspace*{-1em}Records}\\
$[ x_1 \mapsto e_1, \ldots , x_n \mapsto e_n ]$
  \hspace{.5em}\= \kill
 %
$e.x$     
\> \small [The $x$-component of record $e$] \\
 %
$[ x_1 \mapsto e_1, \ldots , x_n \mapsto e_n ]$
  \> \small [The record whose $x_i$ component is $e_i$]\\
 %
$[ x_1 : S_1, \ldots , x_n : S_n ]$ 
 \> \small [Set of all records with $x_i$ component in $S_i$]\\
$[ r \except  !.x=e]$
  \> \small [Record $\widehat{r}$ equal to $r$ except 
             $\widehat{r}.x=e$]\\
$[ r \except !.x  :in: S]$
  \> \small [Set of records $\widehat{r}$ equal to $r$ except 
             $\widehat{r}.x\in S$]\\[.5\baselineskip]
%
{\bf \hspace*{-1em}Tuples}\\
 $S_1 \X \ldots \X S_n$ 
 \hspace{.5em}\= \kill
%
$e[i]$  \>   \small [The $i^{\rm th}$ component of tuple $e$]\\
$<<e_1, \ldots , e_n>>$
  \> \small [The $n$-tuple whose $i^{\rm th}$ component is 
            $e_i$]\expref{tuple}\\
$S_1 \X \ldots \X S_n$
   \> \small [The set of all $n$-tuples with $i^{\rm th}$ component in $S_i$]
 \\[.5\baselineskip]
%
{\bf \hspace*{-1em}Miscellaneous} \\
{\bf let} $x_{1}\deq e_{1}$ \ldots\ $x_{n}\deq e_{n}$ {\bf in} $e$
  \hspace{.5em}\= \kill
 %
\str{$c_1 \ldots c_n$}
   \> \small [A literal string of $n$ characters]\expref{SpecVariables}   \\
 %
{\bf if} $p$ {\bf then} $e_1$ {\bf else} $e_2$
  \> \small [Equals $e_1$ if $p$ true, else $e_2$]\\
 %
{\bf case} $p_1 \rightarrow e_1$, \ldots\,,\ $p_n \rightarrow e_n$
  \> \small [Equals $e_i$ if $p_i$ true]
 \\
{\bf let} $x_{1}\deq e_{1}$ \ldots\ $x_{n}\deq e_{n}$ {\bf in} $e$
  \> \small [Equals $e$ in the context of the definitions] \\
$\begin{noj2}
  /\ & p_{1}  \\
     & \ldots \\
  /\ & p_{n}
 \end{noj2}$\hspace{.5em}%
 {\small [the conjunction $p_{1} /\ \ldots /\ p_{n}$]}
 \hspace{1em}
$\begin{noj2}
  \/ & p_{1}\\
     & \ldots \\
  \/ & p_{n}
 \end{noj2}$\hspace{.5em}%
\small [the disjunction $p_{1} \/ \ldots \/ p_{n}$]\expref{conjNotation}
\end{tabbing}
\vspace{-\baselineskip}
\caption[]{The constant operators of \TLA+.}
\label{fig:TLA+operators}
\end{figure}

\end{document}
   
