\documentstyle[11pt,titlepage,twoside]{article}
%\documentstyle[11pt,titlepage,tla,twoside]{article}

%%%% For people using obsolete versions, this fixes a LaTeX bug 
%%%% that was corrected 17 Oct 91.
\makeatletter
\def\@tfor#1:=#2\do#3{\def\@fortmp{#2}\ifx\@fortmp\@empty \else
    \@tforloop#2\@nil\@nil\@@#1{#3}\fi}

%%%%%%%%%%%%% file tla.sty
%%  TLA DOCUMENT STYLE
%%  (c) 1994 by Leslie Lamport
%
%   Changes:
%     27 Dec 95 : Removed bug that caused error on blank line inside
%                 \assume or \prove argument.
%      1 Mar 95 : Made \V work with negative argument.
%     14 Oct 94 : Made equation and eqnarray environments use TLA mode
%                 Also redefined \label and \ref so they work with
%                 arbitrary labels inside TLA mode.
%
%   Last modified on Tue Jan 16 17:36:07 PST 1996 by lamport
%
%   This style calls the pf style, and the abbrev style.  These other 
%   styles should not be loaded separately.
%
%   This 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.  (See below for how to customize the abbreviations.)
%  
%    ==   :  equals by definition (\deq)
%    =>   : \Rightarrow
%    :\:  : \backslash
%    []   : \Box 
%    <>   : \Diamond
%    ~>   : \leadsto
%    ~    : \lnot
%    -+-> : the TLA "while-plus" operator: an arrow with a "+" over it.
%    <--  : \longleftarrow
%    <-   : \leftarrow
%    <<   : \langle
%    >>   : \rangle
%    -->  : \longrightarrow
%    ->   : \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 ... }
%  
%  WARNING: In tla mode, $ is fragile, so it must be \protect'ed if
%  it appears in a moving argument.
%  
%  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
%
%    For splitting a module across figures, there is the nomodule
%    environment, which is like the module environment but does
%    not produce the top and bottom module lines.  These lines are 
%    produced by the commands \topbar{MODULE-NAME} and \bottombar.
%
%    The following commands produce the obvious keywords:
%
%       \IMPORT       \VARIABLE      \UNCHANGED      \UNION  
%       \EXPORT       \CONSTANT      \EXCEPT         \SUBSET  
%       \INCLUDE      \BOOLEAN       \ENABLED        \TRUE      
%       \AS           \ACTION        \CHOOSE         \FALSE  
%                     \STATEFCN      \DOMAIN         
%       
%    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).
%
%
% CUSTOMIZING THE ABBREVIATIONS
% ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
%  You can create a new set of abbreviations.  However, it is advisable
%  to keep the current ones and just add to them.  You do this with
%  a tlabbrev environment, which is just like an abbreviate environment
%  except without the first argument.  (See abbrev.sty for documentation
%  on the abbreviate environment.)  The following tlabbrev environment
%  creates the standard abbreviations.  Modify it to add your own
%  abbreviations.
%
% \begin{tlabbrev}{:[=<-/|#"_!>}{:[=<-/|#"_!\:>}
%   \x ==   {\ensuremath{\;\;\deq\;\;}}
%   \x =>   {\ensuremath{\Rightarrow}}
%   \x =    {=}
%   \x :\:  {\ensuremath{\,\backslash}}
%   \x ::   {::}
%   \x :    {\tlacolon}
%   \x []   {\ensuremath{\Box}}
%   \x [    {[}
%   \x <>   {\ensuremath{\Diamond}}
%   \x <--  {\ensuremath{\longleftarrow}}
%   \x <-   {\ensuremath{\leftarrow}}
%   \x <<   {\ensuremath{\langle\tlathin}}
%   \x <    {\ensuremath{<}}
%   \x >>   {\ensuremath{\tlathin\rangle}}
%   \x >    {\ensuremath{>}}
%   \x -->  {\ensuremath{\longrightarrow}}
%   \x --   {--}
%   \x -+-> {\ensuremath{\tlawhilep}}
%   \x -+-  {-+-}
%   \x -+   {-+}
%   \x ->   {\ensuremath{\rightarrow}}
%   \x -    {\ensuremath{-}}
%   \x |->  {\ensuremath{\mapsto}}
%   \x |-   {\ensuremath{\vdash}}
%   \x |=   {\ensuremath{\models}}
%   \x |    {\ensuremath{|}}
%   \x #    {\ensuremath{\neq}}
%   \x ~>   {\ensuremath{\leadsto}}
%   \x ~    {\ensuremath{\lnot}}
%   \x /    {\tlaslash}
%   \x "    {\ensuremath{\tlaquote}}
%   \x _.   {\,}
%   \x __   {\tlaunder}
%   \x _    {\tlasubscript}
%   \x !    {\ensuremath{\tlathin!\tlathin}}
% \end{tlabbrev}
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%\input{abbrev.sty}
%%%%%%% file abbrev.sty
%% File abbrev.sty

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                      DOCUMENTATION                             %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% This file defines the abbreviate environment, which allows you to do
% things like typing $=>$ instead of $\Rightarrow$.  It also defines
% a few useful commands, including one to make math-mode use ordinary
% italic characters.
%
%
% THE abbreviate ENVIRONMENT
% ~~~~~~~~~~~~~~~~~~~~~~~~~~
% This environment is explained in terms of the following example:
% 
%    \begin{abbreviate}{FOO}{=#(}{=#(}
%      \x ==>  {\Longrightarrow}
%      \x ==   {==}
%      \x =>  {\Rightarrow}
%      \x =   {=}
%      \x #   {\neq}
%      \x (+) {\oplus}
%      \x (+  {(+}
%      \x (   {(}
%    \end{abbreviate}
% 
% This defines the declaration \FOO that does the following:
%   * Makes the three characters  
%           =  #  ( 
%     active--so they are commands like the character ~ (tilde).
% 
%   * Defines these characters in such a way that 
%       ==> is an abbreviation for  \Logrightarrow, 
%       ==  does what it normally does 
%       =   does what it normally does
%       #   is an abbreviation for \neq
%       etc.
% 
% It also defines the declaration \noFOO to undo the effects of the
% declaration \FOO.  Here are the rules
% 
%    * The following characters can appear as the first character
%      of an abbreviation:
% 
%         ! @ # $ % ^ & * ( ) _ - + = ~ ` | [ ] : ; " ' < > , . ? /
% 
%    * The other characters in an abbreviation can be anything except
%      the three characters  \  {  } .  They can contain % only if
%      %  appears in the last two arguments of the abbreviate environment.
%
%    * The second and third arguments of the abbreviate environment consist 
%      of the first characters that appear in abbreviations.  However,
%      ~ (tilde) does not appear in these arguments, even if it's
%      used as the first character of an abbreviation. [As a NOTE below
%      explains, the second and third arguments need not always have
%      the same characters.]
% 
%    * An abbreviation definition consists of \x followed by
%      the abbreviation, followed by one or more spaces, followed
%      by its definition, enclosed in braces.
%
%    * The sequence of abbreviations being defined must obey the following 
%      rules:
%
%         - The first abbreviation is arbitrary.
%
%         - Every subsequent abbreviation must be obtained by deleting
%           the last character from the previous abbreviation and adding
%           any (possibly empty) string of characters.
%
%         - The last abbreviation defined must be a single character.
%
%      It is a consequence of these rules that, to define an abbreviation,
%      It is necessary to define every prefix of that abbreviation.
%
%
%   NOTE: You can have multiple abbreviate environments to define
%   different sets of abbreviations.  
%
%   WARNING: When a character is active, it doesn't behave like it normally
%   does.  In particular, if  [  or  ]  is active, then [ ] cannot be
%   used to enclose optional arguments.   Use something like
%
%           \noFOO \command[arg] \FOO   or  {\noFOO \command[arg]}
%
%   if you need a command with optional arguments.
%
%   NOTE: In the example above, the command \FOO both activates the
%   characters  = # ( and defines their active versions appropriately.
%   The abbreviate environment also defines the command \FOOact, 
%   which just activates the characters.  Since the definitions 
%   aren't changed by \noFOO, the sequence of commands
%
%      \FOO \noFOO \FOOact 
%
%   is equivalent to \FOO.  If you're writing macros that do a lot
%   of messing around, you may want to take advantage of this.
%
%   NOTE: You can use commands of the form \<single-letter>, such
%   as \: in an abbreviation, as long as it's not the first letter.
%   If you use such a command, it must go in the third argument (but
%   NOT the second) of the abbreviate environment.
%
%
%   USEFUL COMMANDS
%   ~~~~~~~~~~~~~~~
%
% \ensuremath{FORMULA}
%    Typesets FORMULA in math mode, regardless of current mode.
%    (This is a standard LaTeX-2e command.)
%
% \noTeXmath
% \TeXmath   
%    In math mode, TeX normally typesets characters in math italic,
%    which makes $different$ look like $d$ time $i$ times $f$ times ...
%    and not like {\it different}.  The \noTeXmath causes TeX to use
%    ordinary italic, so $different$ is the same as {\it different}.
%    This makes it easier to use multi-letter identifiers in formulas.
%    The \TeXmath command reverts to TeX's normal behavior
%
% \makeactive{CHARS} : 
%    CHARS should be a string of characters, not containing any of the
%    three characters "\", "{", or "}".  This activates all the characters
%    (sets their catcode to active [catcode = 13]).
%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                THE abbreviate ENVIRONMENT                      %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% DEFINE COUNTERS
%
\newcounter{abr@ctr}
\newcounter{abr@level} \setcounter{abr@level}{0}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% THE abbreviate ENVIRONMENT
%
% \abbreviate{PREFIX}{ACTIVECHARS}{ACTIVECHARS}
%
\def\abbreviate#1{%
  \def\abr@prefix{#1}%      \abr@prefix := PREFIX
  \global\let\abr@tilde~%   \abr@tilde  := real tilde
  \gdef\abr@activechars{}%
  \let~\relax
  \abr@sanitize
  \abr@abbreva}

\def\abr@abbreva#1{%          %% \abr@activate  := catcode characters to active
  \gdef\abr@activate{}%       %% \abr@deactivate := make everything normal
  \gdef\abr@deactivate{}%
  \@tfor\i:=#1\do{%
    %%\typeout{Loop: i = \i}
    \xdef\abr@activate{\abr@activate\catcode`\i\active}%
    \xdef\abr@deactivate{\abr@deactivate\catcode`\i12\relax}}%
    \xdef\abr@deactivate{\abr@deactivate\noexpand\abr@unsanitize
                         \noexpand\let\noexpand~\noexpand\abr@tilde}%
   \abr@activate
   \abr@abbrevb}

\def\abr@abbrevb#1{%   % Let all active characters to \relax and 
   \@tfor\i:=#1\do{%   % let \x to \abr@getsub
     \expandafter\let\i\relax}%
   \let\x\abr@getsub}

\def\endabbreviate{%
  \expandafter\abr@defineactives\abr@activechars\do\abr@tempx
  \expandafter\global\expandafter\let\csname\abr@prefix\endcsname\abr@tempx
  \expandafter\global\expandafter\let
         \csname\abr@prefix act\endcsname\abr@activate
  \expandafter\global\expandafter\let
      \csname no\abr@prefix\endcsname\abr@deactivate}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% THE INVARIANT
%
% The following invariant is maintained in the body of the abbreviate
% environment, where def_i[foo] is the definition of (the macro
% expansion of) foo at \begingroup nesting level i.  (Nesting level 0 is
% the top.)
% 
% IF the last command processed was
%     c_0 ... c_n {val} 
% THEN Exists \cmd_1 ... \cmd_n :
%   LET X(i) == \abr@ifnextchar c_i{\cmd_i}{\csname def_i[abr@else]\endcsname}
%   IN  * \value{abr@level} = n
%       * current \begingroup nesting level = n
%       *   \csname \abr@prefix\string c_0] \endcsname  =g  IF n = 0 THEN val
%                                                                    ELSE X(1)
%       * For all i in {1, ... ,n-1} : 
%          \cmd_i =g c_i -> X(i+1)
%       * For all i in {1, ... , n} :
%          \csname def_i[abr@else]\endcsname is undefined at level 0.
% 
%       * \cmd_n =g c_n -> the right sequence to process c_0...c_n
%       * \prefix@activechars = ... c_0
% 

% \abr@addcmd{STRING}{VAL} 
%    The guts of the abbreviate environment. \x STRING {VAL} expands
%    to \abr@addcmd{STRING}{VAL}.  
%
%  BEGIN
%    abr@ctr := 0
%    Remaining := STRING
%    WHILE Remaining # empty
%    DO  \char     := Head(Remaining)
%        Remaining := Tail(Remaining)
%        IF abr@ctr < abr@level
%          THEN %%%  Do nothing
%          ELSE %%% Current string length >= previous one
%               IF abr@ctr = abr@level 
%                 THEN %% this is beginning of new string suffix
%                      IF abr@level = 0
%                        THEN %% new beginning char
%                              \abr@then :=g \abr@prefix \string\char
%                              \abr@activechars := 
%                                 \abr@activechars :o: \char
%                        ELSE %% have to clean up preceding char
%                             \abr@temp :=g \abr@else
%                             \abr@then :=g new_cs
%                             \abr@else := new_cs
%                             \gdef \csname \abr@temp\endcsname 
%                                  {\abr@ifnextch {\char}%
%                                       {\csname\abr@then\endcsname}%
%                                       {\csname\abr@else\endcsname}}
%                      FI
%                 ELSE %% We've gotten started on new suffix
%                      \abr@temp :=g \abr@then
%                      \abr@then :=g new_cs
%                      \begingroup
%                      \abr@else := new_cs
%                      IF abr@ctr = 1
%                        THEN %% previous char was first one
%                             \gdef \csname \abr@temp\endcsname
%                               {\abr@ifnextch {\char}%
%                                       {\csname\abr@then\endcsname}%
%                                       {\csname\abr@else\endcsname}}
%                        ELSE \gdef \csname \abr@temp\endcsname \lastchar
%                               {\abr@ifnextch {\char}%
%                                       {\csname\abr@then\endcsname}%
%                                       {\csname\abr@else\endcsname}}
%                      FI
%               FI
%               \prevchar := \char
%        FI
%        abr@ctr := abr@ctr + 1
%    OD
%    %% 
%    IF abr@ctr = abr@level
%      THEN %% Current string one char shorter than previous one.
%           \gdef \csname \abr@else \endcsname {VAL}
%           \endgroup
%      ELSE %% Current string of length >= previous one.
%           IF abr@ctr = 1
%             THEN %% just a one-char string
%                  \gdef\csname \abr@then \endcsname{VAL}
%             ELSE %% multi-char string
%                  \gdef\csname \abr@then \endcsname \prevchar{VAL}
%           FI
%    FI
%    abr@level = abr@ctr - 1
% END definition of \abr@addcmd

\def\abr@addcmd#1#2{%
\setcounter{abr@ctr}{0}%
\@tfor\char:=#1\do{%
  \ifnum \value{abr@ctr} < \value{abr@level}%
    \else \ifnum \value{abr@ctr} = \value{abr@level}%
              \ifnum \value{abr@level} = \z@
                 \xdef\abr@then{\abr@prefix \expandafter\string\char}
                  \xdef\abr@activechars{\abr@activechars\char}
                 %\typeout{ELSE THEN THEN, abr@then := \abr@then}
                \else  \xdef\abr@temp{\abr@else}%
                       \abr@gnewcs\abr@then
                       \abr@newcs\abr@else
                        %\typeout{ELSE THEN ELSE, abr@temp = \abr@temp}
                       \expandafter\xdef\csname\abr@temp\endcsname{%
                           \noexpand\abr@ifnextch\char%
                           {\expandafter\noexpand\csname\abr@then\endcsname}%
                           {\expandafter\noexpand\csname\abr@else\endcsname}}
              \fi
            \else  \xdef\abr@temp{\abr@then}
                   \abr@gnewcs\abr@then
                   \begingroup
                   \abr@newcs\abr@else
                   \ifnum \value{abr@ctr}=\@ne
                       %\typeout{ELSE ELSE THEN, abr@temp = \abr@temp}
                      \expandafter\xdef\csname\abr@temp\endcsname{%
                           \noexpand\abr@ifnextch\char%
                           {\expandafter\noexpand\csname\abr@then\endcsname}%
                           {\expandafter\noexpand\csname\abr@else\endcsname}}
                     \else                    
                       %\typeout{ELSE ELSE ELSE, abr@temp = \abr@temp}
                        \expandafter\expandafter\expandafter\xdef
                           \expandafter\csname\expandafter\abr@temp
                           \expandafter\endcsname\prevchar{%
                           \noexpand\abr@ifnextch\char%
                           {\expandafter\noexpand\csname\abr@then\endcsname}%
                           {\expandafter\noexpand\csname\abr@else\endcsname}}
                   \fi
          \fi
          \let\prevchar\char
  \fi
  \addtocounter{abr@ctr}{1}%
 }%
  \ifnum \value{abr@ctr} = \value{abr@level}%
    %\typeout{DONE THEN abr@else = \abr@else}
    \expandafter\gdef\csname \abr@else \endcsname{#2}%
     \endgroup
   \else \ifnum \value{abr@ctr}=\@ne
           %\typeout{DONE ELSE THEN abr@then = \abr@then}
            \expandafter\gdef\csname\abr@then\endcsname{#2}
          \else 
            %\typeout{DONE ELSE ELSE abr@then = \abr@then}
            \expandafter\abr@gdef\prevchar{\abr@then}{#2}%
          \fi
  \fi
  \setcounter{abr@level}{\value{abr@ctr}}
  \addtocounter{abr@level}{-1}} %% END definition of \abr@addcmd

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                      USEFUL COMMANDS                           %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% 
% \makeactive{CHARS} : 
%    CHARS should be a string of characters, not containing any of the
%    three characters "\", "{", or "}".  This \catcodes all the characters
%    to active (catcode 13).
%
\def\abr@makeactive#1{\catcode`#1\active}
\def\makeactive#1{\@tfor\i:=#1\do{\expandafter\abr@makeactive\i}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% \ensuremath{FORMULA}
%    Typesets FORMULA in math mode, regardless of current mode.
%
\def\ensuremath#1{\relax\ifmmode #1\else $#1$\fi}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% \noTeXmath
% \TeXmath   
%    The \noTeXmath causes TeX to use ordinary italic instead of math
%    italic in math mode.  The \TeXmath command reverts to TeX's normal
%    behavior.  (Modified 10 Aug to work with arbitrary \itfam.)
%    

\newcommand{\abr@c}{\c@abr@ctr\advance\c@abr@ctr\@ne}

% Let it work with LaTeX2e's native mode:
% D. Roegel, 29/8/1994
\ifx\documentclass\undefined
\else
  \DeclareSymbolFont{tlaitalics}{\encodingdefault}{cmr}{m}{it}
  \let\itfam\symtlaitalics
\fi

\newcommand{\noTeXmath}{%
\c@abr@ctr=\itfam
\multiply\c@abr@ctr"100\relax
\advance\c@abr@ctr "7061\relax
\mathcode`a=\abr@c
\mathcode`b=\abr@c
\mathcode`c=\abr@c
\mathcode`d=\abr@c
\mathcode`e=\abr@c
\mathcode`f=\abr@c
\mathcode`g=\abr@c
\mathcode`h=\abr@c
\mathcode`i=\abr@c
\mathcode`j=\abr@c
\mathcode`k=\abr@c
\mathcode`l=\abr@c
\mathcode`m=\abr@c
\mathcode`n=\abr@c
\mathcode`o=\abr@c
\mathcode`p=\abr@c
\mathcode`q=\abr@c
\mathcode`r=\abr@c
\mathcode`s=\abr@c
\mathcode`t=\abr@c
\mathcode`u=\abr@c
\mathcode`v=\abr@c
\mathcode`w=\abr@c
\mathcode`x=\abr@c
\mathcode`y=\abr@c
\mathcode`z=\abr@c
\c@abr@ctr=\itfam
\multiply\c@abr@ctr"100\relax
\advance\c@abr@ctr "7041\relax
\mathcode`A=\abr@c
\mathcode`B=\abr@c
\mathcode`C=\abr@c
\mathcode`D=\abr@c
\mathcode`E=\abr@c
\mathcode`F=\abr@c
\mathcode`G=\abr@c
\mathcode`H=\abr@c
\mathcode`I=\abr@c
\mathcode`J=\abr@c
\mathcode`K=\abr@c
\mathcode`L=\abr@c
\mathcode`M=\abr@c
\mathcode`N=\abr@c
\mathcode`O=\abr@c
\mathcode`P=\abr@c
\mathcode`Q=\abr@c
\mathcode`R=\abr@c
\mathcode`S=\abr@c
\mathcode`T=\abr@c
\mathcode`U=\abr@c
\mathcode`V=\abr@c
\mathcode`W=\abr@c
\mathcode`X=\abr@c
\mathcode`Y=\abr@c
\mathcode`Z=\abr@c}

\newcommand{\TeXmath}{%
\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}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                      AUXILIARY COMMANDS                        %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% \abr@newcs\CMD   
% \abr@gnewcs\CMD :
%    Defines \CMD to be a new string prefixed with \abr@prefix.  
%    The definition is local with \abr@newcs, and global with
%    \abr@gnewcs
%
\newcount\abr@csctr
\def\abr@newcs#1{\global\advance\abr@csctr\@ne
                 \edef#1{\abr@prefix\the\abr@csctr}}
\def\abr@gnewcs#1{\global\advance\abr@csctr\@ne
                 \xdef#1{\abr@prefix\the\abr@csctr}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% \abr@sanitize   
% \abr@unsanitize 
%    "sanitizing" catcodes $ & # ^ _ %  to "other".
%    "unsanitizing" catcodes these characters back to normal.
%
\def\abr@mkother#1{\catcode`#112\relax}
\begingroup
\abr@mkother$\abr@mkother&\abr@mkother#\abr@mkother^\abr@mkother_
\catcode`\%12\relax
\gdef\abr@sanitize{\abr@mkother$\abr@mkother&\abr@mkother#\abr@mkother
                 ^\abr@mkother_\abr@mkother%}
\gdef\abr@unsanitize{\catcode`$3\catcode`&4\catcode`#6\catcode`^7\catcode
                     `_8\catcode`%14\relax}
\endgroup

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% \abr@gdef CHAR{STRING}{DEF} 
%    CHAR must be a character.  
%    This command does \gdef\STRING CHAR{DEF}
%
\def\abr@gdef#1#2#3{\expandafter\gdef\csname#2\endcsname#1{#3}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% \abr@defineactive{CHARS}\CS
%    CHARS must be a string of active characters.
%    Defines \CS to do a \let c=\csname \abr@prefix\string c,
%    For all characters c in the string CHARS.

\def\abr@defineactive#1#2{\gdef#2{}%
  \let\abr@temp\relax
  \@tfor\char:=#1\do{%
    \xdef#2{#2\expandafter\abr@temp\char}}%
    \def\abr@temp##1{%
        \noexpand\let\noexpand##1\expandafter\noexpand
        \csname\abr@prefix\string##1\endcsname}%
  %\show#2
   \xdef#2{#2}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% \abr@getsub STRING \do {VAL}
%   Expands to \abr@addcmd{STRING}{VAL}, where
%   STRING is evaluated with the special characters activated,
%   and VAL is evalued with them deactivated.  
%   It assumes that the characters are activated, and it
%   leaves them activated.
%
\def\abr@getsub#1 {\def\abr@temp{#1}\abr@deactivate\abr@getsuba}
\def\abr@getsuba#1{%
  \abr@activate 
  \let~\relax
  \expandafter\abr@addcmdx\abr@temp\do{#1}}
%\def\abr@addcmdx#1\do#2{\abr@addcmd{#1}{#2\relax}}  
\def\abr@addcmdx#1\do#2{\abr@addcmd{#1}{#2}}  

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% \abr@ifnextch{c}{TRUE}{FALSE}
%   If the immediately following character is c, then TRUE, else FALSE.
%   This should be at the end of whatever macro is looking ahead.

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

% \abr@defineactives\do\CS
%    CHARS must be a string of active characters.
%    Defines \CS to do \abr@activate followed by a 
%       \let c=\csname \abr@prefix\string c, 
%    for all characters c in the string.
%
\def\abr@defineactives#1\do#2{\gdef#2{}%
  \let\abr@temp\relax
  \@tfor\char:=#1\do{%
    \xdef#2{#2\expandafter\abr@temp\char}}%
    \def\abr@temp##1{%
        \noexpand\let\noexpand##1\expandafter\noexpand
        \csname\abr@prefix\string##1\endcsname}%
   \xdef#2{\abr@activate#2}}

%%%%%%%%%%%%%%%%%%%%%%%
%  DEBUGGING
%
%  \@show{FOO} : \show\FOO
\newcommand{\@show}[1]{\expandafter\show\csname#1\endcsname}

%%%%%%% end file abbrev.sty

%% Have to redefine \abr@sanitize  and \abr@unsanitize so they
%% don't muck with $.  For efficiency, remove the mucking about
%% with  &  and %  as well
\gdef\abr@sanitize{\abr@mkother##\abr@mkother^\abr@mkother_}
\gdef\abr@unsanitize{\catcode`##6\catcode`^7\catcode`_8\relax}

%% \noTeXmath
%% \TeXmath
%%   The \noTeXmath 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. \TeXmath resets to normal.

% 
%%
%% Redefine Math Mode commands to use \tla@everymath
%%  Changed 14 Oct 94 to redefine \equation and \eqnarray as well.
%%
%%  (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\[
\let\@begeqn\equation
\let\@begeqnarray\eqnarray
\def\tla@everymath{}  %% initialization

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

%% Redefine \label and \ref

\let\@oldlabel\label
\def\label{\begingroup\notla\@xlabel}
\def\@xlabel#1{\@oldlabel{#1}\endgroup}

\let\@oldref\ref
\def\ref{\begingroup\notla\@xref}
\def\@xref#1{\@oldref{#1}\endgroup}

\newenvironment{tlabbrev}{\begin{abbreviate}{tla@abbrev}}{\end{abbreviate}}


\begin{tlabbrev}{:[=<-/|#"_!>}{:[=<-/|#"_!\:>}
  \x ==   {\ensuremath{\;\;\deq\;\;}}
  \x =>   {\ensuremath{\Rightarrow}}
  \x =    {=}
  \x :\:  {\ensuremath{\,\backslash}}
  \x ::   {::}
  \x :    {\tlacolon}
  \x []   {\ensuremath{\Box}}
  \x [    {[}
  \x <>   {\ensuremath{\Diamond}}
  \x <--  {\ensuremath{\longleftarrow}}
  \x <-   {\ensuremath{\leftarrow}}
  \x <<   {\ensuremath{\langle\tlathin}}
  \x <    {\ensuremath{<}}
  \x >>   {\ensuremath{\tlathin\rangle}}
  \x >    {\ensuremath{>}}
  \x -->  {\ensuremath{\longrightarrow}}
  \x --   {--}
  \x -+-> {\ensuremath{\tlawhilep}}
  \x -+-  {-+-}
  \x -+   {-+}
  \x ->   {\ensuremath{\rightarrow}}
  \x -    {\ensuremath{-}}
  \x |->  {\ensuremath{\mapsto}}
  \x |-   {\ensuremath{\vdash}}
  \x |=   {\ensuremath{\models}}
  \x |    {\ensuremath{|}}
  \x #    {\ensuremath{\neq}}
  \x ~>   {\ensuremath{\leadsto}}
  \x ~    {\ensuremath{\lnot}}
  \x /    {\tlaslash}
  \x "    {\ensuremath{\tlaquote}}
  \x _.   {\,}
  \x __   {\tlaunder}
  \x _    {\tlasubscript}
  \x !    {\ensuremath{\tlathin!\tlathin}}
\end{tlabbrev}

%% -+-> : 
\def\tla@while{-\hspace{-.2em}\triangleright}
\def\tlawhilep{\stackrel
  {\mbox{\raisebox{-.3em}[0pt][0pt]{$\scriptscriptstyle+\;\,$}}}{\tla@while}}

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

\let\tlachars\tla@abbrevact
\let\notlachars\notla@abbrev



\newif\if@tlamode
\@tlamodetrue

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

\begingroup
\catcode`?6\relax
\tlachars

%% :
\gdef\tla@cmdcolon?1:{\ensuremath{\csname ?1\endcsname}}

%% "
\gdef\tlaquote?1"{\mbox{\rm``{\sf ?1}''}}



%% _ : 
  \gdef\tlaunder{\hspace*{\tla@indentspace}%
                         \@nsifnextchar{_}{\tla@spaceunder}{}}
  \gdef\tla@spaceunder_{\hspace*{\tla@indentspace}%
                         \@nsifnextchar{_}{\tla@spaceunder}{}}

\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\tlacolon{\@ifspace{\tla@realcolon}{\tla@cmdcolon}}} 
\newcommand{\nocoloncommands}{\def\tlacolon{\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{\tlathin!\tlathin}}

%% / : defines \tlaslash so \tlaslash\ expands to \land
\def\tlaslash{\@nsifnextchar{\ }{\tla@slashx}{/}}
\def\tla@slashx\ {\ensuremath{\land}}

% The following was a valiant attempt to make /\ work when
% not followed by a space.  However, it doesn't work if the /\ is
% inside a command argument, in which case the following "\..." has already
% been tokenized before the "/" gets a chance to look at what's ahead.
% (Isn't TeX wonderful?)
%   \def\@makebsother{\catcode`\\=12\relax}
%   \def\@makebsescape{\catcode`\\=0\relax}
%   \begingroup
%   \catcode`?=0\relax
%   \@makebsother
%   ?gdef?tlaslash
%         {?@makebsother?@nsifnextchar{\}{?tla@slashx}{?@makebsescape/}}
%   ?gdef?tla@slashx\{?@makebsescape?ensuremath{?land}}
%   ?endgroup



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

%%_
\def\tlasubscript#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{%
                \noTeXmath
                 \tla@abbrev
                \def\/{\lor}}%
           \tla@abbrev
           \notla@abbrev
         \ifmmode\tla@everymath\fi}

\def\notla{\def\tla@everymath{}%
  \@tlamodefalse
  \TeXmath
  \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
%
% \tlathin : a math-mode space 1/2 the width of \,
%
\def\tlathin{\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.
%

\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}

% \@nsifnextchar like \@ifnextchar, except it doesn't skip over
% space tokens.
\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 pf style}
%\input{pf.sty}
%%%%%%%% file pf.sty
% pf.sty
%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                       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                     %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%

\newenvironment{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}}
\newcommand{\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}}}}

%%%%%%%% end file pf.sty

\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}}
\newcommand{\tla@stepx}[2]{\endgroup\tla@stepy{#1}{#2}}
%% 27 Dec 95 -- changed \def to \newcommand

\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 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\topbar}[1]{\tlanameline{\ 
     {\bf module} {\it #1\@italcor} }\par}

\newenvironment{nomodule}{\begin{trivlist}\flushleft\@computerule
            \item[]\it
            \catcode`_=\active\relax
        }{\par\end{trivlist}}

\newenvironment{module}[1]{\begin{trivlist}\flushleft\@computerule
            \item[]\tlanameline{\ {\bf module} {\it #1\@italcor} }\par\it
            \catcode`_=\active\relax
        }{\par\bottombar\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\bottombar\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{\bottombar}{\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 }}
\newcommand{\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}
%%% 1 Mar 95 : Made \V work with negative argument.
\newcommand{\V}{\begingroup\notlachars\tla@V}
\def\tla@V#1{\endgroup\ifdim #1em<\z@\\[#1em]\else\vs{#1}\\\fi} 


%%%%%%%%%%%%% end file tla.sty


\makeatother

\raggedbottom
% 5 December 94: Corrected a typo and made minor changes to prose.
% 6 December 94: Minor changes to prose. 
% 22 December 94: Minor changes based on comments by Ted Wobber.
% 16 January 96: Made revisions for TCS version

% FOR SRC Report--
    \oddsidemargin   .47in     %   Left margin on odd-numbered pages.
    \evensidemargin 1.06in     %   Left margin on even-numbered pages.


   \topmargin       .47in    %    Nominal distance from top of page to top of
   \headheight        0pt    %    Height of box containing running head.
   \headsep           0pt    %    Space between running head and text.
%  \topskip = 10pt           %    '\baselineskip' for first line of page.
% Bottom of page:
   \footheight       12pt  %    Height of box containing running foot.
   \footskip        1.5cm    %    Distance from baseline of box containing 


\newcommand{\tcsformat}[1]{#1}
                             %    foot to baseline of last line of text.
%\batchmode
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                 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{%                                                       %
%                                                                 %
%                                                                 %
  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}}              %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% Needed to fix bug/feature in LaTeX2e
\def\ensuremath#1{\relax\ifmmode #1\else $#1$\fi}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                      TITLE                             %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%

\title{Processes are in the Eye of the Beholder}
\author{Leslie Lamport}
%\date{\moddate}
\date{22 December 1994 \\ revised 15 January 1996}
% Cleared by Sam, 5 Dec 94

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                    STYLE HACKING                       %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
\setlength{\abovedisplayskip}{\topsep}%
\setlength{\belowdisplayskip}{\topsep}%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                    ENVIRONMENTS                        %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
\newtheorem{lemma}{Lemma}
\newcounter{pfdepthctr}
\setcounter{pfdepthctr}{0}
\newenvironment{prooflist}[1]{\par\small
   \begin{list}{}{\settowidth{\labelwidth}{#1}%
                  \setlength{\leftmargin}{\labelwidth}
                  \setlength{\partopsep}{0em}%%%%%%%%%%%%% label sep
                  \setlength{\labelsep}{.5em}%%%%%%%%%%%%% label sep
                  \addtolength{\leftmargin}{\labelsep}%
                  \setlength{\itemsep}{\ifcase \value{pfdepthctr}%
                       .1em \or .1em \else 0em\fi}%
                  \setlength{\parsep}{\ifcase \value{pfdepthctr}%
                       .1em \else .2em\fi}%
                  \setlength{\topsep}{\ifcase \value{pfdepthctr}%
                       \topsep \else 0em \fi}%
                  \renewcommand{\makelabel}[1]{##1\hfil}}%
   \addtocounter{pfdepthctr}{1}%
   \setlength{\abovedisplayskip}{\parsep}%
   \setlength{\belowdisplayskip}{\parsep}%
   \setlength{\abovedisplayshortskip}{\parsep}%
   \setlength{\belowdisplayshortskip}{\parsep}%
}{\addtocounter{pfdepthctr}{-1}\end{list}}
\newcommand{\extraitem}[1]{\par\addvspace{-\parsep}%
                            \makebox[0pt][r]{#1\hspace{\labelsep}}%
                            \begingroup\tlachars\tlaargpar}
\newcommand{\pfitem}[1]{\item[#1]\begingroup\tlachars\tlaargpar}
\newcommand{\tlaargpar}[1]{#1\endgroup\par}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                  NOTATION FOR THIS DOCUMENT                    %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% \ZN == {0, ... , N-1}
% \Z2 == {0, 1}
% \Z{i} == {0, ... , i}
% \Nat == {0, 1, ... }
%% \df{i}{j}{k} == ...
% \act{A} ==  Action A (A in \cal font)
% \minus  == a narrow minus
% \plus   == a narrow plus
% \cn == a colon without the extra space around it
% \equivby{step} ==  \equiv with step over it.
\newcommand{\ZN}{\ensuremath{{\cal Z}_{N}}}
\newcommand{\Z}[1]{\ensuremath{{\cal Z}_{#1}}}
\newcommand{\Nat}{\ensuremath{{\cal N}}}
%\newcommand{\df}[3]{#2=_{#1}#3}
\newcommand{\act}[1]{\ensuremath{{\cal #1}}}
%% For program notation
\newcommand{\ceq}{:=}
\newcommand{\keywd}[1]{{\bf #1}}
\makeatletter
\newcommand{\minus}{\@ifnextchar{1}%
    {\mskip-1.1\thinmuskip-\mskip-1.1\thinmuskip}%
    {\mskip-.25\thinmuskip-\mskip-.25\thinmuskip}}
\newcommand{\plus}{\@ifnextchar{1}%
    {\mskip-.75\thinmuskip+\mskip-.75\thinmuskip}%
    {\mskip-.25\thinmuskip+\mskip-.25\thinmuskip}}
\newcommand{\cn}{\mskip -.5\thinmuskip : \mskip -.5\thinmuskip}
\makeatother
\newcommand{\provable}[1]{\ensuremath{\vdash #1}}
\newcommand{\proofrule}[2]{\setlength{\arrayrulewidth}{.6pt}%
  {\ensuremath{\begin{array}[t]{@{}c@{}}%
       \begin{array}[t]{@{}l@{}} #1\raisebox{-.1em}{\strut}\end{array}\\
       \hline \raisebox{.1em}{\strut}#2\end{array}}}}
\newcommand{\negspace}{\s{-.5}}
%\newcommand{\equivby}[1]{\stackrel{\rm #1\rule[-2pt]{0pt}{0pt}}{\;\equiv\;}}
\newcommand{\equivby}[1]{\;\equiv\;}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                TEMPORAL FORMULA NAMES                  %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
\newcommand{\PiTwo}{\ensuremath{\Pi_{2}}}
\newcommand{\PiTwoni}{\ensuremath{\Pi_{2}^{\rm ni}}}
\newcommand{\PhiTwo}{\ensuremath{\Phi_{2}}}
\newcommand{\PhiTwoni}{\ensuremath{\Phi_{2}^{\rm ni}}}
\newcommand{\PhiTwou}{\ensuremath{\Phi_{2}^{\rm u}}}
\newcommand{\PhiTwob}{\ensuremath{\Phi_{2}^{\rm b}}}
\newcommand{\PhiTwoh}{\ensuremath{\Phi_{2}^{\rm h}}}
\newcommand{\PhiTwohS}{\ensuremath{\Phi_{2}^{\rm hS}}}
\newcommand{\PiN}{\ensuremath{\Pi_{\rm N}}}
\newcommand{\PiNni}{\ensuremath{\Pi_{N}^{\rm ni}}}
\newcommand{\PhiN}{\ensuremath{\Phi_{\rm N}}}
\newcommand{\PhiNni}{\ensuremath{\Phi_{N}^{\rm ni}}}
\newcommand{\PhiNu}{\ensuremath{\Phi_{\rm N}^{\rm u}}}
\newcommand{\PhiNb}{\ensuremath{\Phi_{\rm N}^{\rm b}}}
\newcommand{\PhiNh}{\ensuremath{\Phi_{\rm N}^{\rm h}}}
\newcommand{\PhiNhS}{\ensuremath{\Phi_{\rm N}^{\rm hS}}}
\newcommand{\InvN}{\ensuremath{InvN}}
\newcommand{\InvH}{\ensuremath{Inv}}


\begin{document}
%try
%try
%\maketitle

%\thispagestyle{empty}
\pagenumbering{roman}
\thispagestyle{empty}
\vspace*{2.23cm}

\noindent
{\Large \bf Processes are in the Eye of the Beholder}

\vspace{.5cm}

{\large
\noindent 
Leslie Lamport\\[.25cm]
December 25, 1994\\
revised January 16, 1996}


\cleardoublepage

\mbox{}

\vfill

\noindent
{\bf \copyright Digital Equipment Corporation 1994}\\[\baselineskip]
This work may not be copied or reproduced in whole or in part for 
any commercial purpose. Permission to copy in whole or in part
without payment of fee is granted for nonprofit educational and
research purposes provided that all such whole or partial copies
include the following: a notice that such copying is by permission
of the Systems Research Center of Digital Equipment Corporation
in Palo Alto, California; an acknowledgment of the authors and
individual contributors to the work; and all applicable portions
of the copyright notice. Copying, reproducing, or republishing for
any other purpose shall require a license with payment of fee to
the Systems Research Center. All rights reserved.

\cleardoublepage
\thispagestyle{empty}



\subsubsection*{Author's Abstract} 
\vspace{-2pt} 


A two-process algorithm is shown to be equivalent to an $N$-process
one, \mbox{illustrating} the insubstantiality of processes.  A 
formal equivalence proof in TLA (the Temporal Logic of Actions) is
sketched.


\cleardoublepage
\thispagestyle{empty}
%\newpage
%try
\thispagestyle{empty}

\tableofcontents

\cleardoublepage
\pagenumbering{arabic}
%\newpage
%\setcounter{page}{1}

%try
\section{Introduction}

Processes are often taken to be the fundamental building blocks of
concurrency.  A concurrent algorithm is traditionally represented as
the composition of processes.  We show by an example that processes
are an artifact of how an algorithm is represented.  The difference
between a two-process representation and a four-process representation
of the same algorithm is no more fundamental than the difference
between $2+2$ and $1+1+1+1$.


Our example is a fifo ring buffer, pictured in
Figure~\ref{fig:ring-buffer}.
%
\begin{figure}[b]
\centering
\begin{picture}(0,80)
\thicklines
\put(-60,0){\framebox(120,80){\thinlines
    \begin{tabular}{rl}
      $buf[0]$ & \framebox{\rule{0pt}{.6em}\hspace{3em}}\\[.3em]
      $buf[1]$ & \framebox{\rule{0pt}{.6em}\hspace{3em}}\\
      \multicolumn{2}{c}{\vdots} \\
      $buf[N\minus1]$ & \framebox{\rule{0pt}{.6em}\hspace{3em}}
    \end{tabular}}}
\put(-120,40){\vector(1,0){60}}
\put(-120,42){\makebox(60,0)[b]{$in$}}
\put(60,40){\vector(1,0){60}}
\put(60,42){\makebox(60,0)[b]{$out$}}
\end{picture}
\caption{A ring buffer.} \label{fig:ring-buffer}
\end{figure}
%
The $i$th input value received on channel $in$ is stored in
$buf[i\minus1\bmod N]$, until it is sent on channel $out$.  Input and
output may occur concurrently, but input is enabled only when the
buffer is not full, and output is enabled only when the buffer is not
empty.

Figure~\ref{fig:2-process-pgm} shows a representation of the ring
buffer as a two-process program in a CSP-like
language~\cite{hoare:csp}.  (We ignore CSP's termination convention;
the loops are assumed never to terminate.)
%
\begin{figure}%[t]
\centering
\begin{minipage}{\textwidth}
\begin{tabbing}
$in$, $out$ : \keywd{channel of} $Value$\\
$buf$ \keywd{array} $0 \;.\,.\; N\minus1$ \keywd{of} $Value$ \\[.2em]
$p$, $g$ : \keywd{internal} $Natural$ \keywd{initially} 0\\[.4em]
$Receiver\,$:: \= \kill
$Receiver\,$:: \> $\mbox{\Large$*$}\notlachars\left[\tlachars
   \begin{array}{@{}lll@{}}
    p \minus g #N & -> & in\,?\,buf[p \,mod\, N] ; \\
              &    & p :ceq: p\plus1
   \end{array}\right]$\\
%
\s{1}$||$ \\
$Sender\,$:: \>  
   $\mbox{\Large$*$}\notlachars\left[\tlachars\begin{array}{@{}lll@{}}
     p \minus g # 0 & -> & out\,!\,buf[g \,mod \,N]; \\
               &    & g :ceq: g\plus1
   \end{array}\right]$
\end{tabbing}
\end{minipage}
\caption{The ring buffer, represented in a CSP-like language.}
\label{fig:2-process-pgm}
\end{figure}
The variables $p$ and $g$ record the number of values received on
channel $in$ by the {\em Receiver\/} process and sent on channel $out$
by the {\em Sender\/} process, respectively.  Declaring $p$ and $g$ to
be internal means that their values are not externally visible, so a
compiler is free to implement them any way it can, or to eliminate
them entirely.  

The intuitive meaning of this program should be clear to readers
acquainted with CSP\@.  We will not attempt to give a rigorous meaning
to the program text.  Programming languages evolved as a method of
describing algorithms to compilers, not as a method for reasoning
about them.  We do not know how to write a completely formal proof
that two programming-language representations of the ring buffer are
equivalent.  In Section~\ref{sec:specs}, we represent the program
formally in TLA, the Temporal Logic of Actions~\cite{lamport:newtla}.
Figure~\ref{fig:2-process-pgm} will serve only as an intuitive
description of the TLA formula.


Figure~\ref{fig:n-process-pgm} shows another representation of
%
\begin{figure}%[t]
\centering
\begin{minipage}{\textwidth}
\begin{tabbing}
\strut$in$, $out$ : \keywd{channel of} $Value$\\
$buf$ \keywd{array} $0 \;.\,.\; N\minus1$ \keywd{of} $Value$ \\[.2em]
$pp$, $gg$ : \keywd{internal} \keywd{array} $0 \;.\,.\; N\minus1$ 
                     \keywd{of} $\{0,\,1\}$ \keywd{initially} 0 \\[.4em]
$Buffer(i: 0 \,.\,.\, N\minus1)\,$::\\[.2em]
\s{.75}$ 
  \mbox{\normalsize$\mbox{\LARGE$*$}$}\notlachars
         \left[\tlachars\begin{array}{@{}r@{\;}lll@{}}
   empty\!\!: &
    IsNext(pp,i)     
    % \df{i}{pp[i\minus1 \,mod\,N]}{pp[i]}
                & -> & in\,?\,buf[i]; \\
    &           &    & pp[i] :ceq: 1 - pp[i] \,;\V{.2}
   full\!\!: &
     IsNext(gg,i)
     %\df{i}{gg[i\minus1 \,mod\,N]}{gg[i]} 
                & -> & out\,!\,buf[i]; \\
    &           &    & gg[i] :ceq: 1 - gg[i]
   \end{array}\right]$
% \\
% \s{1}\raisebox{.75em}{\strut}where $\df{i}{j}{k}$ $\;\equiv\;$
%   \keywd{if} $i = 0$ \keywd{then} $j = k$ 
%   \keywd{else} $j\neq k$ \keywd{fi}\\
\end{tabbing}
\end{minipage}
\caption{Another representation of the ring buffer.}
\label{fig:n-process-pgm}
\end{figure}
%
the ring buffer,  where $IsNext$
is defined by
% \[ IsNext(r,i) == {\bf if\;\ }i = 0 {\bf\;\ then\;\ } r[0] = r[N\minus1]
%                                {\bf\;\ else\;\ } r[i] # r[i\minus1] \]
 \[ IsNext(r,i) == \IF{i = 0}\THEN r[0] = r[N\minus1] \\
                             \ELSE r[i] # r[i\minus1] \FI \]
%
This is as an $N$-process program; the $i$th process, $Buffer(i)$,
reads and writes $buf[i]$.  Variables $p$ and $g$ of the two-process
program are replaced by arrays $pp$ and $gg$ of bits.  Array
elements $pp[i]$ and $gg[i]$ are read and written by process
$Buffer(i)$, and are read by process $Buffer(i\plus1\bmod N)$.

The two programs are equivalent because the values assumed by $pp$ and
$gg$ in the $N$-process program correspond directly to the values
assumed by $p$ and $g$ in the two-process one.  The correspondence
between $pp$ and $p$ is shown in Figure~\ref{fig:pp-implements-p} for
$N=4$.  A boxed number in the $pp[i]$ column indicates that
$IsNext(pp,i)$ equals \TRUE\@.  The correspondence between $gg$ and $g$ 
is the same.

\begin{figure}
\centering
\begin{tabular}{c@{\hspace{2.5em}}cccc}
  \relax{$p$} & \relax{$pp[0]$} & \relax{$pp[1]$} 
                & \relax{$pp[2]$} & \relax{$pp[3]$} \\[.3em]
  0 & \fbox{0} & 0        & 0        & 0        \\
  1 & 1        & \fbox{0} & 0        & 0        \\
  2 & 1        & 1        & \fbox{0} & 0        \\
  3 & 1        & 1        & 1        & \fbox{0} \\
  4 & \fbox{1} & 1        & 1        & 1        \\
  5 & 0        & \fbox{1} & 1        & 1        \\
  6 & 0        & 0        & \fbox{1} & 1        \\[-.4em]
  $\vdots$ & $\vdots$ & $\vdots$ & $\vdots$ & $\vdots$ 
\end{tabular}
\caption[]{The correspondence between values of $pp$ and $p$, for $N=4$.}
\label{fig:pp-implements-p}
\end{figure}

It is not hard to argue informally that the two programs are
equivalent.  Formalizing this argument should be as straightforward as
proving formally that $222+222$ equals $111+111+111+111$.  But, even
if straightforward, a completely formal proof of either result from
first principles is not trivial.  In Section~\ref{sec:proof}, we
sketch a formal TLA proof that the two versions of the ring buffer are
equivalent.


%try
\section{The Algorithm in TLA} \label{sec:specs}

We now write the TLA formulas that describe the programs of Figures
\ref{fig:2-process-pgm} and~\ref{fig:n-process-pgm}.  The program
texts do not tell us what liveness properties are assumed.  To make
the example more interesting, we assume no liveness properties for sending
values on the $in$ channel, but we require that every value received
in the buffer be eventually sent on the $out$ channel.  For the
two-process program, this means assuming fairness for the $Sender$,
but not for the $Receiver$.  For the $N$-process program, it means
assuming fairness for the $full$ action of each process, but not for
the $empty$ action.

The program texts also do not determine the grain of atomicity.  For
simplicity, we assume that an entire guarded command is a single
atomic operation.  Thus, evaluating a guard and executing the
subsequent communication and assignment statements is taken to be an
indivisible step.

We give an interleaving representation of the ring buffer---one in which
sending and receiving are represented by distinct atomic actions.
In Section~\ref{sec:discussion}, we describe how the specifications and
proofs could be written in terms of a noninterleaving representation
that allows values to be sent and received simultaneously.

We use the following notation:
 $\Nat$ is the set of natural numbers; 
 $\Z{m}$ is the set \mbox{$\{0, \ldots, m\minus1\}$}; 
  square brackets
  denote function application;
 \hbox{$[S -> T]$} is the set of functions with domain $S$
  and range a subset of $T$;
\hbox{$[i\in S |-> e]$} is the function $f$ with domain
  $S$ such that $f[i]=e$ for all $i\in S$;
 \hbox{$[f \EXCEPT ![i]=e]$\hspace{-0.64304pt}} %%%%% overfull hbox ok
is the function $\widehat{f}$ that
  is the same as $f$ except $\widehat{f}[i]=e$;
angle brackets enclose tuples; 
  $t[i]$ is the $i$th component of tuple $t$, so $<<v, w>>[2] = w$;
and $S:\:T$ is the set of elements in $S$ that are not in $T$.

A TLA formula is an assertion about {\em behaviors\/}, which are
sequences of states.  Steps (pairs of successive states) in a behavior
are described by {\em actions\/}, which are boolean-valued expressions
containing primed and unprimed variables; unprimed variables refer to
the old state and primed variables refer to the new state.  To
describe CSP-style communication, we represent a channel by a variable
and represent the sending of a value by a change to that variable.  We
define $Channel(V)$ to be the set of legal values of a channel of type
$V$, and $Comm(v,c)$ to be the action that represents communicating a
value $v$ on channel $c$.  The actual definitions, given below, are
irrelevant; we require only that a $Comm(v,c)$ action changes $c$, if
$v\in V$ and $c\in Channel(V)$.

 \[ \begin{noj3}
      Channel(V) & \deq & V :X: \Z2\V{.1}
      Comm(v, c) & \deq & c' = <<v, 1-c[2]>>
    \end{noj3}
 \]
The TLA formula $\PiTwo$ that represents the two-process program is
defined in Figure~\ref{fig:Pi2}. We now explain that definition.
%
\begin{figure}
\centering
$\begin{noj3}
  Type2 &\;\deq\;& \begin{conj}
            p, g :in: \Nat\\
            buf :in: [\ZN -> Value] \\
            in, out :in: Channel(Value)
          \end{conj}\\
%
 UnB(i) &\;\deq\;& [j :in: \ZN :\: \{i\} |-> buf[j]] \\
%
 Rcv &\;\deq\;& \begin{conj}
          p-g # N \\ 
          p' = p+1 \\
          Comm(buf'[p \bmod N], in) \\ 
          \UNCHANGED <<g, out, UnB(p \bmod N)>> 
        \end{conj}\\
%
 Snd &\;\deq\;& \begin{conj}
          p-g # 0 \\
          g' = g+1 \\
          Comm(buf[g \bmod N], out) \\
          \UNCHANGED <<p, buf, in>>
        \end{conj} \\
%
 \PhiTwo &\;\deq\;& \begin{conj}
            []Type2 \\
            (p=0) /\ [][Rcv]_{<<p, buf, in>>} \\
            (g=0) /\ [][Snd]_{<<g, out>>} /\ \WF_{<<g, out>>}(Snd)
          \end{conj}\\
%
 \PiTwo &\;\deq\;& :EE: p, g : \PhiTwo 
 \end{noj3}$
\caption[]{The TLA formula $\PiTwo$ representing the two-process program.}
\label{fig:Pi2}
\end{figure}
%

A list of expressions bulleted by $\land$ denotes their conjunction;
indentation is used to eliminate parentheses.  If formula $F$ is
written as such a list, then $F.i$ is its $i$th conjunct---for
example, $Rcv.2$ is $p'=p\plus1$.  A similar convention is used for
disjunctions.

The state predicate $Type2$ asserts that each variable has the correct
type.  (The array variable $buf$ of the programming language
representation becomes a variable whose value is a function.)  The
type declarations of the two-process program are represented by the
TLA formula $[]Type2$, which asserts that $Type2$ equals \TRUE\ in all
states of the behavior.

Action $Snd$ describes a step of the $Sender$ process; it can occur
only when $p-g#0$, and it increments $g$ by 1, communicates $buf[g\bmod N]$
on channel $out$, and leaves $p$, $buf$, and $in$ unchanged
($\UNCHANGED v$ is defined to equal $v'=v$).  Similarly, action $Rcv$
describes a step of the $Receiver$ process.  The conjunct $Rcv.3$
asserts that the value $buf'[p\bmod N]$ (the new value of $buf[p \bmod
N]$) is communicated on channel $in$.  The state function $UnB(i)$ is
defined so that, if it is unchanged, then $buf[j]$ is unchanged for
all $j#i$.  Thus, $Rcv$ asserts that the new value of $buf[p \bmod N]$
is the value communicated on channel $in$, and that $buf[j]$ remains
unchanged for all $j # p\bmod N$.


Formula $\PhiTwo.2$ describes the $Receiver$ process.  It asserts that
$p$ is initially $0$, and that every step is a $Rcv$ step or leaves
$p$, $buf$, and $in$ unchanged ($[A]_v$ is defined to equal $A \/
(v'=v)$).  Steps that leave $p$, $buf$, and $in$ unchanged represent
steps of the $Receiver$'s environment---either steps of the
$Sender$ or steps of the entire program's environment.  The
conjunct $\PhiTwo.3$ similarly represents the $Sender$ process.  The
formula $\WF_{<<g, out>>}(Snd)$ asserts weak fairness of the $Snd$
action.  In general, $\WF_{v}(A)$ asserts that if action $<<A>>_v$
(defined to equal $A /\ (v'#v)$) remains continuously enabled, then an
$<<A>>_v$ step must eventually occur.

Formula $\PhiTwo$ is the conjunction of the specifications of the two
processes with the formula asserting type correctness.  It describes
the two-process program with $p$ and $g$ visible.  The complete
program specification $\PiTwo$ is obtained by hiding $p$ and $g$.  In
logic, hiding means existential quantification; in temporal logic,
flexible variables (distinct from rigid variables like $N$) are hidden
with the temporal existential quantifier $:EE:$.

The conjunct $[]Type2$ of $\PhiTwo$ makes type correctness an explicit
part of the specification.  We put type-correctness assumptions in our
specifications to make them as much like Figures
\ref{fig:2-process-pgm} and \ref{fig:n-process-pgm} as possible.
However, to avoid errors, it is usually better to let type correctness
be a consequence of the specification.  We could rewrite $\PhiTwo$ as
follows to eliminate the conjunct $[]Type2$.  The conjunct $[]Type2.1$
is already redundant because it is implied by
 $\PhiTwo.2 /\ \PhiTwo.3$.  We can eliminate $[]Type2.3$
by making $Type2.3$ part of the initial condition, since 
 $Type2.3 /\ \PhiTwo.2 /\ \PhiTwo.3$ implies $[]Type2.3$.  
(The proof requires the fact that $c\in Channel(V)$ and $Comm(v,c)$
imply $c'\in Channel(V)$.)  We can eliminate $[]Type2.2$ in the same
way, if we modify $Rcv$ so it leaves the domain of $buf$ unchanged.

The TLA formula $\PiN{}$ that represents the $N$-process program 
is defined in Figure~\ref{fig:PiN}.
%
\begin{figure}
\centering
$\begin{noj3}
  TypeN &\;\deq\;& \begin{conj}
            pp, gg :in: [\ZN  -> \Z2] \\
            ctl :in: [\ZN -> \{"empty", "full"\}]\\
            buf :in: [\ZN -> Value] \\
            in, out :in: Channel(Value)
          \end{conj}\\
%
 Fill(i) &\;\deq\;& \begin{conj}
              ctl[i] = "empty" \\
              IsNext(pp,i) \\
              ctl' = [ctl \EXCEPT ![i] = "full"]\\
              pp' = [pp \EXCEPT ![i] = 1 - pp[i]] \\
              Comm(buf'[i], in) \\
              \UNCHANGED <<gg, out, UnB(i)>>
            \end{conj} \\
%
 Empty(i) &\;\deq\;& \begin{conj}
               ctl[i] = "full" \\ 
               IsNext(gg,i)\\
               ctl' = [ctl \EXCEPT ![i] = "empty"] \\
               gg'=[gg \EXCEPT ![i] = 1- gg[i]]\\
               Comm(buf[i], out) \\
               \UNCHANGED <<pp, in, buf>>
             \end{conj} \\
%
 NotProc(i) &\;\deq\;& \begin{conj}
                   \UNCHANGED <<pp[i], gg[i], ctl[i], buf[i]>>\\
%                   (\df{i}{pp[i\minus1 \,mod\,N]}{pp[i]}) =>
                     IsNext(pp,i) => \UNCHANGED in \\
%                    (\df{i}{gg[i\minus1 \,mod\,N]}{gg[i]}) =>
                     IsNext(gg,i) => \UNCHANGED out
                 \end{conj}\\
%
 varN{} &\;\deq\;& <<pp, gg, ctl, buf, in, out>>\\
%
 \PhiN{} &\;\deq\;& \begin{conj}
          []TypeN \\
          :A: i :in: \ZN : 
             \begin{conj}
                (pp[i] = gg[i] = 0) /\ (ctl[i] = "empty") \\
                [][Fill(i) \/ Empty(i) \/ NotProc(i)]_{varN} \\
                \WF_{varN}(Empty(i))
             \end{conj}
          \end{conj} \\
 %
 \PiN{} &\;\deq\;& :EE: pp, gg, ctl : \PhiN{}
 \end{noj3}$
\caption[]{The TLA formula $\PiN$ representing the $N$-process program.}
\label{fig:PiN}
\end{figure}
%
There are two things in this definition that merit further
explanation.  First, we introduce an array $ctl$ to represent the
control state.  The value of $ctl[i]$ equals $"empty"$ if control in
process $Buffer(i)$ is at the point labeled $empty$, and it equals
$"full"$ if control is at $full$.  Second, we introduce an action
$NotProc(i)$ that has no obvious counterpart in
Figure~\ref{fig:n-process-pgm} or in $\PiTwo$.  The specifications of
the two processes in Figure~\ref{fig:2-process-pgm} are especially
simple because each variable is changed by an action of only one of
the processes.  For example, a step of the $Sender$'s environment can
be characterized as any step that leaves $g$ and $out$ unchanged.  We
can think of $g$ and $out$ as belonging to the $Sender$.  In the
$N$-process program, $pp[i]$, $gg[i]$, and $ctl[i]$ belong to
$Buffer(i)$.  However, $in$ and $out$ don't belong to any single
process; they can be changed by a step of any of the $N$ processes.
The variable $in$ belongs to $Buffer(i)$ only when $IsNext(pp,i)$
equals \TRUE, and $out$ belongs to $Buffer(i)$ only when
$IsNext(gg,i)$ equals \TRUE. Action $NotProc(i)$ characterizes steps
of $Buffer(i)$'s environment, which is allowed to change $in$ when
$IsNext(pp,i)$ equals \FALSE, and to change $out$ when $IsNext(gg,i)$
equals \FALSE. The subscript in $[][\ldots]_{varN}$ allows steps of
the entire program's environment that leave all the variables
unchanged.  It is semantically superfluous, since $NotProc(i)$ already
allows such steps, but the syntax of TLA requires some subscript.

%try
\tcsformat{\vspace{.5\baselineskip}} %%% formatting

\section{The Proof} \label{sec:proof}


We now give a hierarchically structured proof that $\PiTwo$ and $\PiN$
are equivalent~\cite{lamport:howtoprove}.  The proof is completely
formal, meaning that each step is a mathematical formula.  English is
used only to explain the low-level reasoning.  The entire proof could
be carried down to a level at which each step follows from the simple
application of formal rules, but such a detailed proof is more
suitable for machine checking than human reading.  Our complete proof,
with ``Q.E.D.''\ steps and low-level reasoning omitted, appears in 
Appendix~\ref{appendix:proof}.  

The correctness of the algorithm rests on simple properties of
integers and of the $mod$ operator.  We need the following lemma,
where the bit array $Rep(m)$ used to represent the integer~$m$ is
defined by
 \[ Rep(m) == [i :in: \ZN |-> {\bf if\ } 
                i < m :bmod: 2N :leq: i+N {\bf\ then\ } 1 {\bf\ else\ } 0 ]
 \]
The lemma is proved in Appendix~\ref{appendix:lemma}.  
We assume throughout that $N$ is
a positive integer.
\begin{lemma} \label{lemma:rep}
If $m\in\Nat$ and  $i\in\ZN$, then
\begin{enumerate}
\item $IsNext(Rep(m),i) \equiv (i=m\bmod N)$

\item $IsNext(Rep(m),i) => \V{.1}
         __Rep(m+1) = [Rep(m) \EXCEPT ![i]=1-Rep(m)[i]]$
\end{enumerate}
\end{lemma}
%
For temporal reasoning, we use the following TLA rules from Figure~5
of~\cite{lamport:newtla}.  (This version of TLA2 generalizes the one
in~\cite{lamport:newtla}.)
 \[ \mbox{\small$
     \begin{noj}
      \begin{noj2}
       {\rm STL}2.\ \provable{\Box F \,=>\, F}   &
       {\rm STL}3.\ \provable{\Box\Box F \;\equiv\;\Box F}   \V{.1}
       {\rm STL}4.\ \proofrule{F=> G}{\Box F \;=>\;\Box G\vs{.3}} &
       {\rm STL}5.\ \provable{\Box(F\land G)\;\equiv\;(\Box F)\land(\Box G)} \\
       {\rm INV}1.\ 
         \proofrule{I \land[N]_{f}=> I'}%
         {I \land\Box[N]_{f}=> \Box I\vs{.3}}  \s{1}& 
       {\rm INV}2.\ 
         \provable{\Box I \;=>\; 
           (\Box[N]_{f} \,\equiv\, \Box[N\land I\land I']_{f})}\\
     \end{noj2}\\
     {\rm TLA}2.\ 
        \proofrule{P \,/\ \,(:A: i :in: S : [A_{i}]_{f_{\!i}})
                      \;=>\; Q\land[B]_{g}}%
       {[]P \, /\ \, (:A: i :in: S : [][A_{i}]_{f_{\!i}})
                      \;=>\; []Q /\ [][B]_{g}}
   \end{noj}$} \]
The high-level structure of the proof is shown in
Figure~\ref{fig:pf-hi-level}.
%
\begin{figure}[tb]
{\bf Theorem } $\PiTwo\,\equiv\,\PiN$ 
\begin{prooflist}{1b.}
 \pfitem{1a.}{$\PhiTwo \,\,\equiv\, \PhiTwou$}
 \extraitem{b.}{$\PhiN   \,\equiv\, \PhiNu$}

 \pfitem{2a.}{$\PhiTwou \,\,\equiv\, :EE: pp, gg, ctl : \PhiTwoh$}
 \extraitem{b.}{$\PhiNu \,\equiv\, :EE: p, g : \PhiNh$}
 
 \pfitem{3.}{$\PhiTwoh \,\equiv\, \PhiNh$}

 \pfitem{4.}{Q.E.D.}
  \pf\ $\begin{noj4}
         \PiTwo & \,\equiv\, & 
                 :EE: p, g : \PhiTwou              
              & __\comment{step 1a  and the 
                           definition of $\PiTwo$}\\
              & \,\equiv\, & 
                 :EE: p, g, pp, gg, ctl : \PhiTwoh 
              & __\comment{step 2a}\\
              & \,\equiv\, & 
                 :EE: p, g, pp, gg, ctl : \PhiNh 
              & __\comment{step 3}\\
              & \,\equiv\, & 
                 :EE: pp, gg, ctl, p, g : \PhiNh 
              & __\comment{simple logic}\\
              & \,\equiv\, & :EE: pp, gg, ctl : \PhiNu    
              & __\comment{step 2b}\\
              & \,\equiv\, & \PiN{}                    
              & __\comment{step 1b and the definition of $\PiN$}
       \end{noj4}$
\end{prooflist}
\addvspace{-.6\baselineskip}
\caption[]{The high-level structure of the proof.}
\label{fig:pf-hi-level}
\end{figure}
%
The proofs of steps 1--3, and the definitions of $\PhiTwou$, $\PhiNu$,
$\PhiTwoh$, and $\PhiNh$, are given in the following sections.


\subsection{Step 1: Removing the Process Structure}

Formulas $\PhiTwou$ and  $\PhiNu$ are defined in
Figure~\ref{fig:PhiTwoa-PhiNa}.
%
\begin{figure}[tb]
\centering
$\begin{noj3}
 var2 &\;\deq\;& <<p, g, buf, in, out>>\V{.2}
 \PhiTwou &\;\deq\;& \begin{conj}
            []Type2 \\
            (p=0) /\ (g=0) \\
            [][Rcv \/ Snd]_{var2} \\
            \WF_{<<g, out>>}(Snd)\vs{.2}
          \end{conj}\\
\PhiNu &\;\deq\;& \begin{conj}
             []TypeN \\
              :A: i :in: \ZN : (pp[i] = gg[i] = 0) /\ (ctl[i] = "empty") \\
              [][:E: i :in: \ZN : Fill(i) \/ Empty(i)]_{varN} \\
             :A: i :in: \ZN : \WF_{varN}(Empty(i))
          \end{conj} 
 \end{noj3}$
\caption[]{Formulas $\PhiTwou$ and $\PhiNu$.}
\label{fig:PhiTwoa-PhiNa}
\end{figure}
%try
They can be thought of as uniprocess versions of the two algorithms.
We obtained them by rewriting $\PhiTwo$ and $\PhiN$ as formulas
with a single next-state relation, instead of as the conjunction of
processes.

Step 1a is proved as follows.
\begin{prooflist}{1a.}
\pfitem{1a.}{$\PhiTwo \equiv \PhiTwou$}
    \begin{prooflist}{1a.1.}
      \pfitem{1a.1.}{$Type2 => ([Rcv]_{<<p, buf, in>>} /\ [Snd]_{<<g, out>>} 
                         \equiv [Rcv \/ Snd]_{var2})$}
             \pf\ Given below.
%
\pagebreak
%
      \pfitem{1a.2.}{$[]Type2 => 
                        ([][Rcv]_{<<p, buf, in>>} /\ [][Snd]_{<<g, out>>}
                           \equiv [][Rcv \/ Snd]_{var2})$}
           \pf\ Step 1a.1 and rule TLA2.
%
      \pfitem{1a.3.}{Q.E.D.}
           \pf\ Step 1a.2 and the definitions
              of $\PhiTwo$ and $\PhiTwou$.
    \end{prooflist}
\end{prooflist}
Step 1a.1 is proved by showing that $Type2$ implies 
\begin{small}
\begin{tabbing}
$[Rcv]_{<<p, buf, in>>} /\ [Snd]_{<<g, out>>}$\\
\s{1}\= \+ 
 $\equiv\,$ \= \comment{by definition of $[A]_{v}$}\\
          \> $\begin{conj}
                Rcv \/ (<<p, buf, in>>' = <<p, buf, in>>) \\
                Snd \/ (<<g, out>>'=<<g, out>>)
                 \vs{.2}
              \end{conj}$ \\
 $\equiv\,$ \> \comment{by propositional logic}\\
          \> $\begin{disj}
                      Rcv /\ (<<g, out>>'=<<g, out>>) \\
                      Snd /\ (<<p, buf, in>>'=<<p, buf, in>>)\\
                      Rcv /\ Snd \\
                      (<<g, out>>'=<<g, out>>) 
                         /\ (<<p, buf, in>>'=<<p, buf, in>>)
                 \vs{.4}
                    \end{disj}$\\
 $\equiv\,$ \> $\begin{noj2}
              \/ \; Rcv & 
                 \tlacomment{$Rcv$ implies $<<g, out>>'=<<g, out>>$}\\
              \/ \; Snd & 
                 \tlacomment{$Snd$ implies 
                        $<<p, buf, in>>'=<<p, buf, in>>$}\\
              \/ \; \FALSE &
                  \tlacomment{$Type2 /\ Rcv$ implies $p'#p$, and
                              $Snd$ implies $p'=p$}\\
              \/ \; var2' = var2__ &
                   \tlacomment{$<<v_{1},\ldots,v_{m}>>' = 
                        <<v_{1},\ldots,v_{m}>>$ iff
                       $(v_{1}'=v_{1}) /\ \ldots /\ (v_{m}'=v_{m})$}
                 \vs{.4}
            \end{noj2}$ \\
 $\equiv\,$ \> $[Rcv \/ Snd]_{var2}$\s{1.5}\comment{by definition of $[A]_{v}$}
\end{tabbing}
\end{small}
All of the nontemporal steps in our proof can be reduced to this kind
of algebraic manipulation.  From now on, we just sketch such proofs
and leave the detailed calculations to the reader.

The proof of step 1b is similar to that of step 1a, but it is a bit
more difficult because it requires an invariant $\InvN$, which asserts
that the arrays $pp$ and $gg$ are representations of natural numbers.
 \[ \InvN == (:E: m :in: \Nat : pp = Rep(m)) 
               \, /\ \, (:E: m :in: \Nat : gg = Rep(m))
 \]
%The proof of step 1b is:
\begin{prooflist}{1b.}
\pfitem{1b.}{$\PhiN \equiv \PhiNu$}
\begin{prooflist}{1b.1a.}
  \pfitem{1b.1a.}{$\PhiN  => []\InvN$}
  \extraitem{b.}{$\PhiNu => []\InvN$}
                 \pf\ Described below.

  \pfitem{1b.2.}{$TypeN /\ \InvN \, =>$\V{.1}
                 \s{1}$[:E: i :in: \ZN :cn:
                         Fill(i) \/ Empty(i)]_{varN}\,\equiv$\V{.1}
                 \s{2} $:A: i :in: \ZN : [Fill(i) \/ Empty(i) 
                              \/ NotProc(i)]_{varN}$}
                 \pf\ If $i#j$, then $TypeN$ implies that
                $Fill(i) /\ Fill(j)$, $Empty(i) /\ Empty(j)$, 
                and $Fill(i) /\ Empty(j)$ are all false; and
                $TypeN /\ \InvN$ implies 
                $Fill(i)=>NotProc(j)$ and $Empty(i)=>NotProc(j)$.
                By Lemma~\ref{lemma:rep}.1, $TypeN /\ \InvN$ implies 
                $(:A: i :in: \ZN : NotProc(i))\equiv (varN'=varN)$.

  \pfitem{1b.3.}{$[]TypeN /\ []\InvN =>$\V{.1}
          \s{1}$[][:E: i :in: \ZN :cn: 
                      Fill(i) \/ Empty(i)]_{varN}\,\equiv$\V{.1}
          \s{2}$:A: i :in: \ZN : [][Fill(i) \/ Empty(i) 
                            \/ NotProc(i)]_{varN}$}

     \pf\ Step 1b.2 and rule TLA2.
  \pfitem{1b.4}{Q.E.D.}
       \pf\ Steps 1b.1 and 1b.3 and the definitions
              of $\PhiN$ and $\PhiNu$.
\end{prooflist}
\end{prooflist}
Steps 1b.1a and 1b.1b are standard invariance properties; 
1b.1a is proved as follows.
\begin{prooflist}{1b.1a}
 \pfitem{1b.1a}{$\PhiN  => []\InvN$}
 \begin{prooflist}{1b.1a.9}
   \pfitem{1b.1a.1}{$TypeN /\ (:A: i :in: \ZN : pp[i]=gg[i]=0) => \InvN$}
   \pf\ $Rep(0) = [i :in: \ZN |-> 0]$
 
   \pfitem{1b.1a.2}{$\begin{conj}
                        \InvN \\
                           [TypeN  /\ (:A: i :in: \ZN :cn: Fill(i) 
                                   \/ Empty(i) \/ NotProc(i))]_{varN}
                        \end{conj}\\
                       => \InvN'$}
     \begin{prooflist}{1b.1a.2.1.}
       \pfitem{1b.1a.2.1.}{$\InvN /\ TypeN /\ (i :in: \ZN) 
                           /\ Fill(i) => \InvN'$}
%       \pf\ If $pp = Rep(m)$, then by Lemma~\ref{lemma:rep}.2,
%        $Fill(i)$ implies $pp'=Rep(m+1)$.

       \pfitem{1b.1a.2.2.}{$\InvN  /\ TypeN /\ (i :in: \ZN)
                           /\ Empty(i) => \InvN'$}
%       \pf\ By Lemma~\ref{lemma:rep}.2, $(gg = Rep(m)) /\ Fill(i)$ 
%       implies $gg'=Rep(m+1)$.

       \pfitem{1b.1a.2.3.}{$\InvN  /\ TypeN 
                             /\ (:A: i :in: \ZN :cn: NotProc(i)) => \InvN'$}
%       \pf\  $TypeN /\ (:A: i :in: \ZN : NotProc(i))$ implies
%        $pp'=pp$ and $gg'=gg$.

        \pfitem{1b.1a.2.4.}{$\InvN /\ (varN'=varN) => \InvN'$}
%        \pf\ Immediate.

       \pfitem{1b.1a.2.5.}{Q.E.D.}
       \pf\ Steps 1b.1a.2.1--1b.1a.2.4.
     \end{prooflist}
    \pfitem{1b.1a.3.}{$
           \begin{conj}
             TypeN /\ (:A: i :in: \ZN : pp[i]=gg[i]=0) \\
             []TypeN \\
             [][:A: i :in: \ZN :cn: Fill(i)  \/ Empty(i) \/ NotProc(i)]_{varN}
           \end{conj}\\
           => []\InvN$}
      \pf\ Steps 1b.1a.1 and 1b.1a.2 and rules INV1 and INV2.

     \pfitem{1b.1a.4.}{Q.E.D.}
       \pf\ Step 1b.1a.3 and rule TLA2, since 
        $(:A: i :cn: [A_i]_v)\equiv[:A: i :cn: A_i]_v$.
 \end{prooflist}
\end{prooflist}
Steps 1b.1a.2.1 and 1b.1a.2.2 are proved using
Lemma~\ref{lemma:rep}.2; steps 1b.1a.2.3 and 1b.1a.2.4 follow because
their hypotheses imply $pp'=pp$ and $gg'=gg$.  As indicated in the
appendix, the proof of step 1b.1b is similar.

\subsection{Step 2: Adding History Variables}

Formulas $\PhiTwoh$ and $\PhiNh$ are defined in
Figure~\ref{fig:PhiTwoh-PhiNh}, which also defines their safety parts,
$\PhiTwohS$ and $\PhiNhS$.
%
\begin{figure}
\centering
 \(\begin{noj}
\begin{noj3}
 Init &\;\deq\;& \begin{conj}
              p=g=0                        \\ 
              pp = gg = [i :in: \ZN |-> 0] \\
              ctl = [i :in: \ZN |-> "empty"] \vs{.1}
            \end{conj}\\
%
 Type &\;\deq\;& Type2 /\ TypeN \V{.1}
%
 var &\;\deq\;& <<pp, gg, ctl, p, g, buf, in, out>>
\end{noj3}
\\ \hspace*{.15\textwidth}{\rule{.5\textwidth}{.4pt}}\V{.3}
\begin{noj3}
     HRcv &\;\deq\;& \begin{conj}
          Rcv\\
          pp' = [pp \EXCEPT ![p \bmod N] = 1 - pp[p \bmod N]]\\
          ctl' = [ctl \EXCEPT ![p \bmod N] = "full"]\\
          \UNCHANGED gg \vs{.1}
        \end{conj}\\
%
 HSnd &\;\deq\;& \begin{conj}
          Snd\\
          gg' = [gg \EXCEPT ![g \bmod N] = 1 - gg[g \bmod N]]\\
          ctl' = [ctl \EXCEPT ![g \bmod N] = "empty"]\\
          \UNCHANGED pp \vs{.1}
        \end{conj} 
\end{noj3}\\
%
\begin{noj3}
\PhiTwohS &\;\deq\;& \begin{conj}
             []Type                            \\
             Init                              \\
             [][HRcv \/ HSnd]_{var}   \vs{.2}           
           \end{conj}\\
 \PhiTwoh &\;\deq\;& \PhiTwohS /\ \WF_{<<g, out>>}(Snd)
\end{noj3} 
\\ \hspace*{.15\textwidth}{\rule{.5\textwidth}{.4pt}}\V{.4}
%%%%
\begin{noj3}
 HFill(i) &\;\deq\;& \begin{conj}
              Fill(i)\\
              p' = p+1 \\
              \UNCHANGED g \vs{.1}
            \end{conj} \\
%
 HEmpty(i) &\;\deq\;& \begin{conj}
               Empty(i) \\
               g'=g+1 \\
               \UNCHANGED p \vs{.1}
             \end{conj}  
\end{noj3}\\
%
 \begin{noj3}
\PhiNhS &\;\deq\;& \begin{conj}
           []Type \\
           Init \\          
           [][:E: i :in: \ZN : HFill(i) \/ HEmpty(i)]_{var} \vs{.2}
          \end{conj} \\
  \PhiNh &\;\deq\;& \PhiNhS \, /\ \,(:A: i :in: \ZN : \WF_{varN}(Empty(i)))
    \end{noj3}
   \end{noj}
 \)
\caption[]{Formulas $\PhiTwoh$ and $\PhiNh$.}
\label{fig:PhiTwoh-PhiNh}
\end{figure}
%
We obtained $\PhiTwoh$ by adding $pp$, $gg$, and $ctl$ as history
variables to $\PhiTwou$; and we obtained $\PhiNh$ by adding $p$ and
$g$ as history variables to $\PhiNu$.  In general, adding an auxiliary
variable $a$ to a formula $F$ means writing a formula $F^{a}$ such
that $F \equiv :EE: a :cn: F^{a}$.  A history variable is an auxiliary
variable that records information from previous states.  It is added
by using the following lemma, which can be deduced from the results
in~\cite{abadi:refining}.  Step 2 is easily proved by repeated
application of this lemma.
%
\begin{lemma}[History Variable] \label{thm:history-variable}
If $h$ and $h'$ do not occur in $Init$, $\act{A}_{i}$,
$\act{B}_{j}$, $v$, or f, and $h'$ does not occur in $g_{i}$,
for all $i\in I$ and $j \in J$, then 
\setlength{\abovedisplayskip}{.5\baselineskip}
   \[ \begin{noj}\;
        Init \; /\ \; [][:E: i :in: I : \act{A}_{i}]_{v} 
          \; /\ \; (:A: j :in: J : \WF_{v}(\act{B}_{j})) \\
         \s{1}\equiv \; :EE: h : 
              \begin{conj}
                 Init /\ (h = f) \\
                 [][:E: i :in: I : \act{A}_{i} /\ (h'=g_{i})]_{<<h,v>>}  \\
                 :A: j :in: J : \WF_{v}(\act{B}_{j})
              \end{conj}   
      \end{noj} \]
\end{lemma}
%try
\subsection{Step 3: Equivalence of \protect\PhiTwoh\ and \protect\PhiNh}

In the two-process algorithm, $p$ and $g$ are the actual internal
variables, while $pp$, $gg$, and $ctl$ are history variables.  The
situation is reversed in the $N$-process algorithm.  Step~3 involves
showing that the history variables of one algorithm behave like the
internal variables of the other.  Its proof uses the following
formulas, where $\InvH$ will be shown to be an invariant of both
$\PhiTwoh$ and~$\PhiNh$.
 \[ \begin{noj}
     IsFull(g, p, i) == 
        :E: m :in: \Nat : (g \leq m < p) /\ (i = m \bmod N)\V{.4}
     \InvH == \begin{conj}
                pp = Rep(p) \\
                gg = Rep(g) \\
                ctl = [i :in: \ZN |-> {\bf if\ } IsFull(g, p, i)
                                {\bf\ then\ } "full" {\bf\ else\ } "empty"]\\
                0\leq p-g \leq N 
              \end{conj} 
    \end{noj}
\]
The high-level structure of the
proof is:
\begin{prooflist}{3.}
 \pfitem{3.}{$\PhiTwoh \,\equiv\, \PhiNh$}
 \begin{prooflist}{3.1a.}
   \pfitem{3.1a.}{$Type /\ \InvH => (HRcv \equiv :E: i :in: \ZN : HFill(i))$}
   \extraitem{b.}{$Type /\ \InvH => (HSnd \equiv :E: i :in: \ZN : HEmpty(i))$}

   \pfitem{3.2.}{$[Type /\ \InvH /\ (HRcv \/ HSnd)]_{var} \equiv \V{.1}
                       __[Type /\ \InvH /\ (:E: i :in: \ZN :  
                           HFill(i) \/ HEmpty(i))]_{var}$}

   \pfitem{3.3a.}{$\PhiTwohS => []\InvH$}
   \extraitem{b.}{$\PhiNhS => []\InvH$}

   \pfitem{3.4.}{$\PhiTwohS \equiv \PhiNhS$}

   \pfitem{3.5.}{$[]\InvH /\ \PhiNhS \,=>\,% \\
                   (\WF_{<<g, out>>}(Snd) \,\equiv\, 
                        (:A: i :in: \ZN :cn: \WF_{varN}(Empty(i))))$}
   \pfitem{3.6.}{Q.E.D.}
   \pf\ Immediate from steps 3.3--3.5.
 \end{prooflist}
\end{prooflist}
Steps 3.1 and 3.2 are (nontemporal) action formulas.  They make it
intuitively clear why the two transformed formulas are equivalent.
Step 3.1a is proved as follows.
 \begin{prooflist}{3.1a.}
   \pfitem{3.1a.}{$Type /\ \InvH => (HRcv \equiv :E: i :in: \ZN : HFill(i))$}
%  \extraitem{b.}{$Type /\ \InvH => (HSnd \equiv :E: i :in: \ZN : HEmpty(i))$}
     \begin{prooflist}{3.1a.1.}
      \pfitem{3.1a.1}{$Type /\ \InvH => (HRcv \equiv HFill(p :bmod: N))$}
         \begin{prooflist}{3.1a.1.1.}
           \pfitem{3.1a.1.1.}{$Type /\ \InvH => 
                             ((p-g # N) \equiv (ctl[p :bmod: N] = "empty"))$}
             \pf\ Arithmetic reasoning and the definition of $IsFull$.
           \pfitem{3.1a.1.2.}{$Type /\ \InvH => IsNext(pp,p :bmod: N)$}
             \pf\ Lemma~\ref{lemma:rep}.1.
           \pfitem{3.1a.1.3.}{Q.E.D.}
            \pf\ Steps 3.1a.1.1 and 3.1a.1.2, and the definitions of $HRcv$ and 
            $HFill$.
         \end{prooflist}
      \pfitem{3.1a.2}{$Type /\ \InvH => (HFill(p :bmod: N) \equiv 
                         (:E: i :in: \ZN : HFill(i)))$}
      \pf\ By Lemma~\ref{lemma:rep}.1, 
      $Type /\ \InvH$
      implies $IsNext(pp,p :bmod: N)$ and $~IsNext(pp,i)$,
      if $i :in: \ZN$ and 
       $i # (p :bmod: N)$.
      \pfitem{3.1a.3}{Q.E.D.}
      \pf\ Steps 3.1a.1 and 3.1a.2.
     \end{prooflist}
\end{prooflist}
As indicated in the appendix, the proof of 3.1b is analogous.  Step
3.2 follows easily from step 3.1.

Step 3.3 asserts that $Inv$ is an invariant of both formulas; its
proof is a standard invariance argument.
\begin{prooflist}{3.3a.}
   \pfitem{3.3a.}{$\PhiTwohS => []\InvH$}
   \extraitem{b.}{$\PhiNhS => []\InvH$}
   \begin{prooflist}{3.3.1a.}
     \pfitem{3.3.1.}{$Init => \InvH$}
     \pf\ $Rep(0)$ equals $[i :in: \ZN |-> 0]$ and
     $IsFull(0,0,i)\equiv\FALSE$, for all $i :in: \ZN$.
    
     \pfitem{3.3.2a.}{$\InvH /\ [Type /\ (HRcv \/ HSnd)]_{var} => \InvH'$}
     \extraitem{b.}{$\InvH /\ [Type /\ (:E: i :in: \ZN :  
                           HFill(i) \/ HEmpty(i))]_{var} => \InvH'$}
     \pf\ Given below.

     \pfitem{3.3.3.}{Q.E.D.}
     \pf\ Steps 3.3.1 and 3.3.2, and rules INV1 and INV2.
   \end{prooflist}
\end{prooflist}
Step 3.3.2 asserts that the next-state actions leave $Inv$ invariant.
The proof of 3.3.2a is:
\begin{prooflist}{3.3.2a.}
     \pfitem{3.3.2a.}{$\InvH /\ [Type /\ (HRcv \/ HSnd)]_{var} => \InvH'$}
      \begin{prooflist}{3.3.2a.1}
        \pfitem{3.3.2a.1}{$\InvH /\ Type /\ HRcv => \InvH'$}
         \pf\ Assume $\InvH /\ Type /\ HRcv$.  Then $\InvH.1'$
         is immediate because $p'=p$ and $pp'=pp$;
         $\InvH.2'$ follows from Lemma~\ref{lemma:rep}.2; 
         $\InvH.4'$
         follows from $\InvH.4$, since $HRcv$ implies 
         $p'=p+1$, $g'=g$, and $p-g#N$;
         and
         $\InvH.3'$ holds because
          \[\begin{noj3}
             IsFull(g',p',i) 
              &\equiv& \comment{by definition of $HRcv$}\\
              &      & IsFull(g,p+1,i) \\
              &\equiv& \comment{by definition of $IsFull$} \\
              &      & :E: m :in: \Nat : (g :leq: m < p+1) /\ (i = m \bmod N)\\
              &\equiv& \tlacomment{by $Rcv.1$ and $\InvH.4$}\\
              &      & {\bf if\ } i = p \bmod N 
                            {\bf\ then\ } \TRUE 
                            {\bf\ else\ } IsFull(g,p,i)
           \end{noj3}\]
        \pfitem{3.3.2a.2}{$\InvH /\ Type /\ HSnd => \InvH'$}
         \pf\ Similar to the proof of 3.3.2a.1.
        \pfitem{3.3.2a.3}{$\InvH /\ (var'=var) => \InvH'$}
        \pf\ Immediate.
        \pfitem{3.3.2a.4}{Q.E.D.}
        \pf\ Steps 3.3.2a.1--3.3.2a.3.
      \end{prooflist}
\end{prooflist}
Step 3.3.2b follows from steps 3.3.2a and 3.2.  This completes
the proof of step~3.3.

Steps 3.4 and 3.5, assert the equivalence of the safety and liveness
parts of the formulas, respectively.  Step 3.4 follows from 3.3
and
 \[ \begin{noj}
     []Type /\ []\InvH => \V{.1}
      __[][HRcv \/ HSnd]_{var} \equiv
             [][:E: i :in: \ZN : HFill(i) \/ HEmpty(i)]_{var}
    \end{noj}
 \]
which follows from step 3.2 and rule TLA2.  Step 3.5 has the
following high-level proof.
\begin{prooflist}{3.5.}
   \pfitem{3.5.}{$[]\InvH /\ \PhiNhS \,=> \,
                   (\WF_{<<g, out>>}(Snd) \,\equiv\, 
                        (:A: i :in: \ZN :cn: \WF_{varN}(Empty(i))))$}

   \begin{prooflist}{3.5.1.}
    \pfitem{3.5.1.}{$[]\InvH /\ \PhiNhS \,=> \\
                    __(:A: i :in: \ZN :cn: \WF_{varN}(Empty(i)))
                      \,\equiv\, \WF_{varN}(:E: i :in: \ZN : Empty(i))$}
    
     \pfitem{3.5.2.}{$[]\InvH /\ []Type /\ [][HRcv \/ HSnd]_{var} \,=> \\
                     __\WF_{<<g, out>>}(Snd)\,\equiv\,
                       \WF_{varN}(:E: i :in: \ZN :cn: Empty(i))$}

     \pfitem{3.5.3.}{Q.E.D.}
     \pf\ Steps 3.5.1 and 3.5.2.
   \end{prooflist}
\end{prooflist} 
We first consider step 3.5.1.  When writing TLA specifications, one
often has to choose between asserting fairness of 
 $A_{1} \/ \ldots \/ A_{m}$ 
and asserting fairness of each action $A_{i}$.  The choice becomes a
matter of taste when the resulting specifications are equivalent.
This is the case if, whenever one of the $A_{i}$ becomes enabled, a
step of no other $A_{j}$ can occur before the next $A_{i}$ step.  For
weak fairness, the equivalence is a consequence of the following
result, which can be derived from the TLA proof rules
of~\cite{lamport:newtla}.
\begin{lemma} \label{thm:WF-of-disjunct}
If
 \[ \ENABLED <<\act{A}_{i}>>_{v}
      \, /\ \, []Inv /\ [][\act{N} /\ ~\act{A}_{i}]_{v}
      \; => \; []~\ENABLED <<\act{A}_{j}>>_{v}
 \]
for all $i, j\in S$ with $i\neq j$, then
 \[ []Inv \, /\ \, [][\act{N}]_{v} \; => \;
         (\WF_{v}(:E: i :in: S : \act{A}_{i})
           \,\equiv\, (:A: i :in: S :  \WF_{v}(\act{A}_{i})))
  \]
\end{lemma}
We use this lemma to prove step 3.5.1.
\begin{prooflist}{3.5.1.}
     \pfitem{3.5.1.}{$[]\InvH /\ \PhiNhS => \\
                   __(:A: i :in: \ZN :cn: \WF_{varN}(Empty(i)))
                     \equiv \WF_{varN}(:E: i :in: \ZN :cn: Empty(i)))$}
      \begin{prooflist}{3.5.1.1.}
        \pfitem{3.5.1.1.}{$\PhiNhS => 
           [][:E: i :in: \ZN : Fill(i) \/ Empty(i)]_{varN}$}
        \pf\ TLA2, since $HFill(i)=> Fill(i)$ and 
        $HEmpty(i)=> Empty(i)$.\negspace

       \pfitem{3.5.1.2.}{$\begin{conj}
                               i\in\ZN\\
                               IsNext(gg,i) \\
                               [](\InvH /\ Type)\\
                               [][(:E: j :in: \ZN : Fill(j) \/ Empty(j)) 
                                         /\ ~Empty(i)]_{varN}
                              \end{conj}$\\
                          $=> []IsNext(gg,i)$}
      \pf\ By rules INV1 and INV2, since
           \[ \InvH /\ Type /\ (Fill(j) \/ Empty(j)) /\ ~Empty(i) \]
           implies $gg'=gg$, for all $i,j\in\ZN$.

       \pfitem{3.5.1.3.}{$\begin{conj}
                             (i,j\in\ZN) /\ (i#j)\\
                             \ENABLED<<Empty(i)>>_{varN}\\
                             [](\InvH /\ Type)\\
                             [][(:E: k :in: \ZN : Fill(k) \/ Empty(k)) 
                                  /\ ~Empty(i)]_{varN}
                          \end{conj}$\\
                          $=> []~\ENABLED<<Empty(j)>>_{varN}$}
        \pf\ Step 3.5.1.2 and rule STL4, since
        $\ENABLED<<Empty(i)>>_{varN}$ implies $IsNext(gg,i)$, and
        Lemma~\ref{lemma:rep}.1 implies 
        \[\InvH /\ Type /\ IsNext(gg,i) => ~IsNext(gg,j)\]
        for all $i,j\in\ZN$ with $i#j$.
        \pfitem{3.5.1.4.}{Q.E.D.}
        \pf\ Steps 3.5.1.1 and 3.5.1.3, and Lemma~\ref{thm:WF-of-disjunct}.
      \end{prooflist}
\end{prooflist}
Finally, we prove 3.5.2, which completes the proof of the theorem.
\begin{prooflist}{3.5.2}
      
     \pfitem{3.5.2.}{$[]\InvH /\ []Type /\ [][HRcv \/ HSnd]_{var}\,=> \\
                     __\WF_{<<g, out>>}(Snd)\,\equiv\,
                       \WF_{varN}(:E: i :in: \ZN :cn: Empty(i))$\vs{.1}}
     \begin{prooflist}{3.5.2.1.}
       \pfitem{3.5.2.1.}{$\InvH /\ Type /\ [HRcv \/ HSnd]_{var} => \\
                    __<<Snd>>_{<<g, out>>} \equiv
                     <<:E: i :in: \ZN :cn: Empty(i)>>_{varN}$}
       \pf\ By steps 3.1b and 3.2, since 
      $\InvH /\ Type /\ [HRcv \/ HSnd]_{var}$ implies 
      $<<Snd>>_{<<g, out>>} \equiv HSnd$, and
       \[ \InvH /\ Type /\ [:E: i :in: \ZN :  
                           HFill(i) \/ HEmpty(i)]_{var}\]
      implies $<<:E: i :in: \ZN :cn: Empty(i)>>_{varN} \equiv
                   (:E: i :in: \ZN :cn: HEmpty(i))$.

       \pfitem{3.5.2.2.}{$[]\InvH /\ []Type /\ [][HRcv \/ HSnd]_{var}=> \\
                    __[]<><<Snd>>_{<<g, out>>} \equiv
                      []<><<:E: i :in: \ZN : Empty(i)>>_{varN}$}
       \pf\ $[]\InvH /\ []Type /\ [][HRcv \/ HSnd]_{var}$\\
        $__\begin{noj2}
          =>\; & \tlacomment{by 3.5.2.1 and rules STL5 and TLA2,
                      since $<<A>>_v \equiv~[~A]_v$}\\
               & [][~Snd]_{<<g, out>>} \equiv
                    [][~\,:E: i :in: \ZN :cn: Empty(i)]_{varN} \\
          =>\; & ~[][~Snd]_{<<g, out>>} 
                 \equiv ~[][~\,:E: i :in: \ZN :cn: Empty(i)]_{varN} \\
          =>\; & \comment{by rules STL3, STL4, and STL5} \\
               &  []~[][~Snd]_{<<g, out>>} 
                     \equiv []~[][~\,:E: i :in: \ZN :cn: Empty(i)]_{varN} \\
          =>\; & \tlacomment{since $<> \equiv ~[]~$} \\
               & []<>~[~Snd]_{<<g, out>>} 
                     \equiv []<>~[~\,:E: i :in: \ZN :cn: Empty(i)]_{varN} \\
          =>\; & \tlacomment{since $<<A>>_v \equiv~[~A]_v$}\\
               & []<><<Snd>>_{<<g, out>>} \equiv
                      []<><<:E: i :in: \ZN :cn: Empty(i))>>_{varN}
         \end{noj2}$
      \pfitem{3.5.2.3}{$[]\InvH /\ []Type  /\ [][HRcv \/ HSnd]_{var}=> \\
                    __[]<>~\ENABLED<<Snd>>_{<<g, out>>} \equiv\\
                    ___[]<>~\ENABLED<<:E: i :in: \ZN :cn: Empty(i))>>_{varN}$}
      \pf\ Rules STL2 (which implies $F => <>F$),
      STL4, STL5, and TLA2, since by  3.5.2.1, 
      $\InvH /\ Type /\ [HRcv \/ HSnd]_{var}$ implies
        \[ \ENABLED<<Snd>>_{<<g, out>>} \equiv
                      \ENABLED<<:E: i :in: \ZN :cn: Empty(i))>>_{varN}
        \]

      \pfitem{3.5.2.4}{Q.E.D.}
      \pf\ Steps 3.5.2.2 and 3.5.2.3, since $\WF_v(A)$ is defined to equal
      $[]<>~\ENABLED <<A>>_v \, \/ \,[]<><<A>>_v$.
     \end{prooflist}
\end{prooflist}


%try
\section{Further Remarks} \label{sec:discussion}

We have proved the equivalence of two different representations of the
ring buffer.  This is not just an intellectual exercise; the ability
to transform an algorithm into a completely different form is
important for applying formal methods to real systems.  Going from the
two-process version to the $N$-process one reduces the internal state
of each process from an unbounded number ($p$ or $g$) to three bits
($pp[i]$, $gg[i]$, and $ctl[i]$).  As explained
in~\cite{kurshan:multiplier}, such a transformation enables us to
apply model checking to unbounded-state systems.

In retrospect, it is not surprising that programs with different
numbers of processes can be equivalent.  Multiprocess programs are
routinely executed on single-processor computers by interleaving the
execution of their processes.  The transformation of $\PhiTwo$ and
$\PhiN$ to $\PhiTwou$ and $\PhiNu$ can be viewed as a formal
description of this interleaving.

Using an interleaving representation makes the proof of equivalence a
bit simpler, but it is not necessary.  The equivalence of
noninterleaving representations can be proved as follows.  Let $RcvNI$
and $SndNI$ be the actions obtained from $Rcv$ and $Snd$ by removing
the \UNCHANGED conjuncts and adding the conjunct $\UNCHANGED\!
UnB(p\bmod N)$ to $RcvNI$.  Replacing $Rcv$ and $Snd$ with $RcvNI$ and
$SndNI$ in the definition of $\PiTwo$ yields a noninterleaving
representation of the two-process program.  Similarly, we get a
noninterleaving representation of the $N$-process program by replacing
$Fill(i)$ and $Empty(i)$ with actions $FillNI(i)$ and $EmptyNi(i)$
that have no \UNCHANGED conjuncts except the one for $UnB(i)$.  In the
proof of equivalence, formula $\PhiTwou$ is changed by replacing its
next-state action
 $Rcv \/ Snd$
with 
 $Rcv \/ Snd \/ (RcvNI /\ SndNI)$,
and $\PhiNu$ is changed by replacing its next-state action with
 $:E: i :in: \ZN : Fill(i) \/ Empty(i) \/ (FillNI(i) /\ EmptyNI(i))$.
Formulas $\PhiTwoh$ and $\PhiNh$ are obtained by adding history
variables to the new versions of $\PhiTwou$ and $\PhiNu$.  The proof
of equivalence is the same as before, except we have to consider the
next-state actions' extra disjuncts.  These disjuncts represent the
simultaneous sending and receiving of values.

Indivisible state changes are an abstraction; executing an operation
of a real program takes time.  In TLA, we can represent the concurrent
execution of program operations either as successive steps, or as a
single step.  Which representation we choose is a matter of
convenience, not philosophy.  We have found that interleaving
representations are usually, but not always, more convenient than
noninterleaving ones for reasoning about algorithms.


%try
A proof that two algorithms are equivalent can be turned into a
derivation of one algorithm from the other.  Our proof yields the
following derivation, where each equivalence is obtained from the
indicated proof step(s).
%
\newlength{\fooa}%
\newlength{\foob}%
\newlength{\fooc}%
\settowidth{\fooa}{$\PiTwo$}
\settowidth{\foob}{$\EE pp, gg, ctl, p, g : \PhiNh   /\ \Box Inv$}
\settowidth{\fooc}{$\comment{3.4 and  3.5}$}
%
\[\begin{noj4}
      \PiTwo 
        &\;\equiv\;& \notla\makebox[\foob][l]{$\EE: p, g : \PhiTwou$}   
                    & \notla\makebox[\fooc][l]{$\comment{1a}$}\\
        &\;\equiv\;& :EE: p, g, pp, gg, ctl : \PhiTwoh  & \comment{2a}%\\
    \end{noj4}
\]
\pagebreak
\[\begin{noj4}
        &\;\equiv\;& :EE: p, g, pp, gg, ctl : \PhiTwoh /\ []Inv  
          & \comment{3.3a}\\
   \notla\makebox[\fooa]{}
        &\;\equiv\;&  :EE: pp, gg, ctl, p, g : \PhiNh   /\ []Inv  
          & \comment{3.4 and  3.5}\\
        &\;\equiv\;&  :EE: pp, gg, ctl, p, g : \PhiNh    & \comment{3.3b}\\
        &\;\equiv\;&  :EE: p, g : \PhiNu  & \comment{2b}\\
        &\;\equiv\;&  :EE: p, g : \PhiNu /\ []InvN   & \comment{1b.1b}\\
        &\;\equiv\;&  :EE: p, g : \PhiN /\ []InvN    & \comment{1b.3}\\
        &\;\equiv\;&  \PiN                 & \comment{1b.1a}
    \end{noj4}
\]
%
% \[ \begin{noj4}
%      \PiTwo 
%        &\;\equiv\;& :EE: p, g : \PhiTwou   & \comment{1a}\\
%        &\;\equiv\;& :EE: p, g, pp, gg, ctl : \PhiTwoh  & \comment{2a}\\
%        &\;\equiv\;& :EE: p, g, pp, gg, ctl : \PhiTwoh /\ []Inv  
%          & \comment{3.3a}\\
%        &\;\equiv\;&  :EE: pp, gg, ctl, p, g : \PhiNh   /\ []Inv  
%          & \comment{3.4 and  3.5}\\
%        &\;\equiv\;&  :EE: pp, gg, ctl, p, g : \PhiNh    & \comment{3.3b}\\
%        &\;\equiv\;&  :EE: p, g : \PhiNu  & \comment{2b}\\
%        &\;\equiv\;&  :EE: p, g : \PhiNu /\ []InvN   & \comment{1b.1b}\\
%        &\;\equiv\;&  :EE: p, g : \PhiN /\ []InvN    & \comment{1b.3}\\
%        &\;\equiv\;&  \PiN                 & \comment{1b.1a}
%    \end{noj4}\]
Our derivation uses rules of logic to rewrite formulas.  In process
algebra~\cite{milner:ccs}, analogous transformations are performed by
applying algebraic laws.  It would be interesting to compare a
process-algebraic proof of equivalence of the two ring-buffer programs
with our TLA proof.
%try


%try
\appendix

%\tcsformat{\vspace{2\baselineskip}} %%% formatting

\section{Proof of the Theorem} \label{appendix:proof}
{\bf Theorem } $\PiTwo\,\equiv\,\PiN$ 
\begin{prooflist}{1b.}
\pfitem{1a.}{$\PhiTwo \equiv \PhiTwou$}
    \begin{prooflist}{1a.1.}
      \pfitem{1a.1.}{$Type2 => ([Rcv]_{<<p, buf, in>>} /\ [Snd]_{<<g, out>>} 
                         \equiv [Rcv \/ Snd]_{var2})$}
%
      \pfitem{1a.2.}{$[]Type2 => 
                        ([][Rcv]_{<<p, buf, in>>} /\ [][Snd]_{<<g, out>>}
                           \equiv [][Rcv \/ Snd]_{var2})$}
%
    \end{prooflist}
\pfitem{1b.}{$\PhiN \equiv \PhiNu$}
  \begin{prooflist}{1b.1a.}
     \pfitem{1b.1a.}{$\PhiN  => []\InvN$}
      \begin{prooflist}{1b.1a.9}
         \pfitem{1b.1a.1}{$TypeN /\ (:A: i :in: \ZN : pp[i]=gg[i]=0) => \InvN$}
         \pfitem{1b.1a.2}{$\begin{conj}
                        \InvN \\
                           [TypeN  /\ (:A: i :in: \ZN :cn: Fill(i) 
                                   \/ Empty(i) \/ NotProc(i))]_{varN}
                        \end{conj}\\
                       => \InvN'$}
        \pfitem{1b.1a.3.}{$
           \begin{conj}
             TypeN /\ (:A: i :in: \ZN : pp[i]=gg[i]=0) \\
             []TypeN 
           /\ [][:A: i :in: \ZN :cn: Fill(i)  \/ Empty(i) \/ NotProc(i)]_{varN}
           \end{conj}\negspace\\
           => []\InvN$}
      \end{prooflist}
     \pfitem{1b.1b.}{$\PhiNu => []\InvN$}
       \begin{prooflist}{1b.1a.1.}
        \pfitem{1b.1b.1.}{$TypeN /\ (:A: i :in: \ZN : pp[i]=gg[i]=0) => \InvN$}
        \pfitem{1b.1b.2.}{$\begin{conj}
                           \InvN \\
                           [TypeN  /\ (:E: i :in: \ZN : 
                               Fill(i) \/ Empty(i)]_{varN}
                           \end{conj}\\
                           => \InvN'$}
        \pfitem{1b.1b.3.}{$\begin{conj}
                           TypeN /\ (:A: i :in: \ZN : pp[i]=gg[i]=0) \\
                            []TypeN 
                            /\ [][:E: i :in: \ZN Fill(i) \/ Empty(i)]_{varN}
                           \end{conj}\\
                          => \InvN'$}
       \end{prooflist}

   
     \pfitem{1b.2.}{$TypeN /\ \InvN \, =>$\\
                    \s{1}$[:E: i :in: \ZN :cn:
                            Fill(i) \/ Empty(i)]_{varN}\,\equiv$\\
                    \s{2} $:A: i :in: \ZN : [Fill(i) \/ Empty(i) 
                                 \/ NotProc(i)]_{varN}$}
   
     \pfitem{1b.3.}{$[]TypeN /\ []\InvN =>$\\
             \s{1}$[][:E: i :in: \ZN :cn: 
                         Fill(i) \/ Empty(i)]_{varN}\,\equiv$\\
             \s{2}$:A: i :in: \ZN : [][Fill(i) \/ Empty(i) 
                               \/ NotProc(i)]_{varN}$}
  \end{prooflist}
 \pfitem{2a.}{$\PhiTwou \,\,\equiv\, :EE: pp, gg, ctl : \PhiTwoh$}
 \extraitem{b.}{$\PhiNu \,\equiv\, :EE: p, g : \PhiNh$\vs{.2}}
\pfitem{3.}{$\PhiTwoh \,\equiv\, \PhiNh$}
  \begin{prooflist}{3.1a.}
   \pfitem{3.1a.}{$Type /\ \InvH => (HRcv \equiv :E: i :in: \ZN : HFill(i))$}
     \begin{prooflist}{3.1a.1.}
      \pfitem{3.1a.1}{$Type /\ \InvH => (HRcv \equiv HFill(p :bmod: N))$}
         \begin{prooflist}{3.1a.1.1.}
           \pfitem{3.1a.1.1.}{$Type /\ \InvH => 
                     ((p-g # N) \equiv (ctl[p :bmod: N] = "empty"))$\negspace}
           \pfitem{3.1a.1.2.}{$Type /\ \InvH => IsNext(pp,p :bmod: N)$}
         \end{prooflist}
      \pfitem{3.1a.2}{$Type /\ \InvH => (HFill(p :bmod: N) \equiv 
                         (:E: i :in: \ZN : HFill(i))$}
     \end{prooflist}

   \pfitem{3.1b.}{$Type /\ \InvH => (HSnd \equiv :E: i :in: \ZN : HEmpty(i))$}
     \begin{prooflist}{3.1b.1.}
      \pfitem{3.1b.1}{$Type /\ \InvH => (HSnd \equiv HEmpty(g :bmod: N)$}
         \begin{prooflist}{3.1b.1.1.}
           \pfitem{3.1b.1.1.}{$Type /\ \InvH => 
                     ((p-g # 0) \equiv (ctl[g :bmod: N] = "empty"))\negspace$}
           \pfitem{3.1b.1.2.}{$Type /\ \InvH => IsNext(gg,g :bmod: N)$}
         \end{prooflist}
      \pfitem{3.1b.1}{$Type /\ \InvH => (HEmpty(p :bmod: N) \equiv 
                         (:E: i :in: \ZN : HEmpty(i))$}
     \end{prooflist}


   \pfitem{3.2.}{$[Type /\ \InvH /\ (HRcv \/ HSnd)]_{var} \equiv \V{.1}
                       __[Type /\ \InvH /\ (:E: i :in: \ZN :  
                           HFill(i) \/ HEmpty(i))]_{var}$}

   \pfitem{3.3a.}{$\PhiTwohS => []\InvH$}
   \extraitem{b.}{$\PhiNhS => []\InvH$}
    \begin{prooflist}{3.3.1a.}
      \pfitem{3.3.1.}{$Init => \InvH$}
      \pfitem{3.3.2a.}{$\InvH /\ [Type /\ (HRcv \/ HSnd)]_{var} => \InvH'$}
      \begin{prooflist}{3.3.2a.1}
        \pfitem{3.3.2a.1}{$\InvH /\ Type /\ HRcv => \InvH'$}
        \pfitem{3.3.2a.2}{$\InvH /\ Type /\ HSnd => \InvH'$}
        \pfitem{3.3.2a.3}{$\InvH /\ (var'=var) => \InvH'$}
      \end{prooflist}

      \pfitem{3.3.2b.}{$\InvH /\ [Type /\ (:E: i :in: \ZN :  
                           HFill(i) \/ HEmpty(i))]_{var} => \InvH'$}
    \end{prooflist}

   \pfitem{3.4.}{$\PhiTwohS \equiv \PhiNhS$}

   \pfitem{3.5.}{$[]\InvH /\ \PhiNhS => \,
                   \,(\WF_{<<g, out>>}(Snd) \,\equiv\, 
                        (:A: i :in: \ZN :cn: \WF_{varN}(Empty(i))))$}
     \begin{prooflist}{3.5.1.}
       \pfitem{3.5.1.}{$[]\InvH /\ \PhiNhS \,=> \\
                    __(:A: i :in: \ZN :cn: \WF_{varN}(Empty(i)))
          \,\equiv\, 
               \WF_{varN}(:E: i :in: \ZN :cn: Empty(i))\negspace\negspace$}
       \begin{prooflist}{3.5.1.1.}
          \pfitem{3.5.1.1.}{$\PhiNhS => 
                [][:E: i :in: \ZN : Fill(i) \/ Empty(i)]_{varN}$}
          \pfitem{3.5.1.2.}{$\begin{conj}
                               i\in\ZN\\
                               IsNext(gg,i) \\
                               [](\InvH /\ Type)\\
                               [][(:E: j :in: \ZN : Fill(j) \/ Empty(j)) 
                                         /\ ~Empty(i)]_{varN}
                              \end{conj}$\\
                          $=> []IsNext(gg,i)$}
          \pfitem{3.5.1.3.}{$\begin{conj}
                             (i,j\in\ZN) /\ (i#j)\\
                             \ENABLED<<Empty(i)>>_{varN}\\
                             [](\InvH /\ Type)\\
                             [][(:E: k :in: \ZN : Fill(k) \/ Empty(k)) 
                                  /\ ~Empty(i)]_{varN}
                          \end{conj}$\\
                          $=> []~\ENABLED<<Empty(j)>>_{varN}$}
      \end{prooflist}
    
       \pfitem{3.5.2.}{$[]\InvH /\ []Type /\ [][HRcv \/ HSnd]_{var}\,=> \\
                     __\WF_{<<g, out>>}(Snd)\,\equiv\,
                       \WF_{varN}(:E: i :in: \ZN : Empty(i))$}
        \begin{prooflist}{3.5.2.1.}
          \pfitem{3.5.2.1.}{$\InvH /\ Type /\ [HRcv \/ HSnd]_{var} => \\
                    __<<Snd>>_{<<g, out>>} \equiv
                     <<:E: i :in: \ZN :cn: Empty(i)>>_{varN}$}

          \pfitem{3.5.2.2.}{$[]\InvH /\ []Type /\ [][HRcv \/ HSnd]_{var} => \\
                    __[]<><<Snd>>_{<<g, out>>} \equiv
                      []<><<:E: i :in: \ZN : Empty(i))>>_{varN}$}
          \pfitem{3.5.2.3}{$[]\InvH /\ []Type  /\ [][HRcv \/ HSnd]_{var}=> \\
                    __[]<>~\ENABLED<<Snd>>_{<<g, out>>} \equiv\\
                    ___[]<>~\ENABLED<<:E: i :in: \ZN : Empty(i))>>_{varN}$}
        \end{prooflist}
   \end{prooflist}
  \end{prooflist}
\end{prooflist}

%try
\section{Proof of Lemma~\protect\ref{lemma:rep}} \label{appendix:lemma}

\setcounter{lemma}{0}
\begin{lemma}
If $m\in\Nat$ and  $i\in\ZN$, then
\begin{enumerate}
\item $IsNext(Rep(m),i) \equiv (i=m\bmod N)$

\item $IsNext(Rep(m),i) => \\ __Rep(m+1) = [Rep(m) \EXCEPT ![i]=1-Rep(m)[i]]$
\end{enumerate}
\end{lemma}
\begin{prooflist}{1.}
\pfitem{1.}{$Rep(m+1)= [Rep(m) \EXCEPT ![m :bmod: N] = 1 - Rep(m)[m :bmod: N]]$}
  \begin{prooflist}{1.1.}
    \pfitem{1.1.}{\case{$(m\plus1) :bmod: 2N = (m :bmod: 2N)+1$}}
    \pf\ It suffices to prove that
          \[ Rep(m+1)[j] \;=\;
                     \IF{j=m :bmod: N}\THEN 1- Rep(m)[j]\\
                                        \ELSE Rep(m)[j]\FI\]
     for any $j\in\ZN$.  The proof follows.
    \begin{prooflist}{1.1.1.}
      \pfitem{1.1.1.}{$(j  = m :bmod: N) \equiv 
                      (j  = m :bmod: 2N) \/ (j+N = m :bmod: 2N)$}
      \pf\ Simple number theory.
      \pfitem{1.1.2.}{If $j = m :bmod: N$, then \\
                      $__(j < 1+(m :bmod: 2N) :leq: j+N)
                              \equiv ~(j < m :bmod: 2N :leq: j+N)$}
      \pf\ Step 1.1.1 and simple arithmetic.

      \pfitem{1.1.3.}{If $j # m :bmod: N$ then\\
                       $__(j < 1+(m :bmod: 2N) :leq: j+N)
                       \equiv (j < m :bmod: 2N :leq: j+N)$}
      \pf\ Step 1.1.1 and simple arithmetic.

      \pfitem{1.1.4.}{Q.E.D.}
      \pf\ By 1.1.2, 1.1.3, and the definition of $Rep$.
    \end{prooflist}
    \pfitem{1.2.}{\case{$(m\plus1) :bmod: 2N # (m :bmod: 2N) + 1$}}
      \pf\ The case assumption implies $m :bmod: 2N = 2N-1$, which
      implies
      \[ __\begin{noj3}
           Rep(m)  &=&[i :in: \ZN |-> {\bf\ if\ } i=N-1
                                          {\bf\ then\ } 0{\bf\ else\ } 1] \V{.2}
           Rep(m+1)&=&[i :in: \ZN |-> 0]
         \end{noj3}\]

%    \begin{prooflist}{1.2.1.}
%      \pfitem{1.2.1.}{$m :bmod: 2N = 2N-1$}
%      \pf\ Elementary number theory.
%
%      \pfitem{1.2.2.}{$Rep(m) \;=\; 
%                        [i :in: \ZN |-> {\bf\ if\ } i=N-1
%                           {\bf\ then\ } 0{\bf\ else\ } 1]$}
%      \pf\ Step 1.2.1 and the definition of $Rep$.
%
%      \pfitem{1.2.3.}{$Rep(m+1) \,=\, [i :in: \ZN |-> 0]$}
%      \pf\ Step 1.2.1 and
%         the definition of $Rep$.
%
%      \pfitem{1.2.4.}{Q.E.D.}
%      \pf\ Steps 1.2.2 and 1.2.3.
%    \end{prooflist}
    \pfitem{1.3.}{Q.E.D.}
    \pf\ Steps 1.1 and 1.2.
  \end{prooflist}
\pfitem{2.}{$IsNext(Rep(m),i) \equiv (i=m\bmod N)$}
    The proof is by induction on $m$.
    \begin{prooflist}{2.1.}
      \pfitem{2.1.}{\case{$m=0$}}
      \pf\ $Rep(0)=[j :in: \ZN |-> 0]$ and $IsNext(Rep(0),i)\equiv(i=0)$,
      for $i\in\ZN$.

      \pfitem{2.2.}{\assume{$IsNext(Rep(m),i) \equiv (i=m\bmod N)$}
         \prove{$IsNext(Rep(m+1),i) \equiv (i=m+1\bmod N)$}}
      The result is trivial if $N=1$.  We assume $N>1$.
      \begin{prooflist}{2.2.1.}
        \pfitem{2.2.1.}{$(i = m :bmod: N) \,=>\, 
                        (IsNext(Rep(m+1),i) \equiv ~IsNext(Rep(m),i))$}
         \pf\ $i = m :bmod: N$ implies $IsNext(Rep(m+1),i) \\
                  __\begin{noj2}
                   \equiv & \tlacomment{by definition of $IsNext$}\\
                          & \IF{i=0}\THEN Rep(m+1)[0] = Rep(m+1)[N-1]\\
                                    \ELSE Rep(m+1)[i] # Rep(m+1)[i-1]
                             \FI\\
                   \equiv & \comment{by step 1}\\
                          & \IF{i=0}\THEN 1-Rep(m)[0] = Rep(m)[N-1]\\
                                    \ELSE 1-Rep(m)[i] # Rep(m)[i-1] \FI\\
                   \equiv & ~IsNext(Rep(m),i)
                \end{noj2}$
        \pfitem{2.2.2.}{$(i  = m+1 :bmod: N) \,=>\,
                        (IsNext(Rep(m+1),i) \equiv ~IsNext(Rep(m),i))$}
         \pf\  $i  = m+1 :bmod: N$ implies $IsNext(Rep(m+1),i) \\
             __\begin{noj2}
               \equiv & \tlacomment{by definition of $IsNext$}\\
                      & \IF{i=0}\THEN Rep(m+1)[0] = Rep(m+1)[N-1]\\
                               \ELSE Rep(m+1)[i] # Rep(m+1)[i-1] \FI\\
               \equiv & \tlacomment{by step 1, since $N>1$ implies
                                     $m+1 \bmod N # m \bmod N$ }\\
                      & \IF{i=0}\THEN Rep(m)[0] = 1-Rep(m)[N-1]\\
                               \ELSE Rep(m)[i] # 1-Rep(m)[i-1]
                       \FI\\
               \equiv & ~IsNext(Rep(m),i)
             \end{noj2}$
        \pfitem{2.2.3.}{$(i # m :bmod: N) /\ (i # m+1 :bmod: N) \,=>$\\
                        $__IsNext(Rep(m+1),i) \equiv IsNext(Rep(m),i)$}

         \pf\ The hypothesis implies $IsNext(Rep(m+1),i) \\
              __\begin{noj2}
                \equiv & \tlacomment{by definition  of $IsNext$}\\
                       & \IF{i=0}\THEN Rep(m+1)[0] = Rep(m+1)[N-1]\\
                               \ELSE Rep(m+1)[i] # Rep(m+1)[i-1]
                       \FI\\
                \equiv & \comment{by step 1}\\
                       & \IF{i=0}\THEN Rep(m)[0] = Rep(m)[N-1]\\
                               \ELSE Rep(m)[i] # Rep(m)[i-1]
                       \FI\\
                \equiv & IsNext(Rep(m),i)
              \end{noj2}$

        \pfitem{2.2.4.}{Q.E.D.}
        \pf\ By 2.2.1--2.2.3 and the induction assumption.
     \end{prooflist}
    \pfitem{2.3}{Q.E.D.}
     \pf\ By steps 2.1 and 2.2 and mathematical induction.
    \end{prooflist}
\pfitem{3.}{$IsNext(Rep(m), i) => 
    (Rep(m+1) = [Rep(m) \EXCEPT ![i] = 1 - Rep(m)[i]])$}
   \pf\ Immediate from steps 1 and 2.

\pfitem{4.}{Q.E.D.}
  \pf\ Steps 2 and 3.
\end{prooflist}

\newpage
\addcontentsline{toc}{section}{References}
%try
%\bibliography{mybib}
\begin{thebibliography}{1}

\bibitem{abadi:refining}
Mart\'{\i}n Abadi, Leslie Lamport, and Stephan Merz.
\newblock Refining specifications.
\newblock To appear.

\bibitem{hoare:csp}
C.~A.~R. Hoare.
\newblock Communicating sequential processes.
\newblock {\em Communications of the ACM}, 21(8):666--677, August 1978.

\bibitem{kurshan:multiplier}
R.~P. Kurshan and Leslie Lamport.
\newblock Verification of a multiplier: 64 bits and beyond.
\newblock In Costas Courcoubetis, editor, {\em Computer-Aided Verification},
  volume 697 of {\em Lecture Notes in Computer Science}, pages 166--179,
  Berlin, June 1993. Springer-Verlag.
\newblock Proceedings of the Fifth International Conference, CAV'93.

\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:newtla}
Leslie Lamport.
\newblock The temporal logic of actions.
\newblock {\em ACM Transactions on Programming Languages and Systems},
  16(3):872--923, May 1994.

\bibitem{milner:ccs}
R.~Milner.
\newblock {\em A Calculus of Communicating Systems}, volume~92 of {\em Lecture
  Notes in Computer Science}.
\newblock Springer-Verlag, Berlin, Heidelberg, New York, 1980.

\end{thebibliography}

\bibliographystyle{plain}

\end{document}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
