\documentstyle[11pt,twoside]{article}

%%% The contents of this file can be inserted into a document
%%% in place of the tla style.

%%%% 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:
%     14 Oct 94 : Made equation and eqnarray environments work use TLA mode
%                 Also redefined \label and \ref so they work with
%                 arbitrary labels inside TLA mode.
%
%   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}}
\def\tla@stepx#1#2{\endgroup\tla@stepy{#1}{#2}}

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

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

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

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


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

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

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

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


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

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

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

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

\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}
\newcommand{\V}{\begingroup\notlachars\tla@V}
\def\tla@V#1{\endgroup\vs{#1}\\}

%%% end file tla.sty

\makeatother


%%* "Proving Possibility Properties"
% Cleared 10 Feb 95

% 21 June 95: Simple corrections  based on comments by Cynthia Hibbard

% 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 
                             %    foot to baseline of last line of text.

\title{\bf Proving Possibility Properties}
\author{Leslie Lamport}
%\date{\moddate}
\date{4 July 1995}

\nocoloncommands

%%% proof style
\setlength{\pfsep}{1pt plus 1pt}
\setlength{\stepsep}{1pt plus 1pt}
%%%%%%%%% NOTATION
%
%  \M{F}            == semantic meaning of F
%  \prefix          == prefix notation
%  \cat             == sequence concatenation
%  \valid{F}        == |= F
%  \possibly{Pi}{P} == always possible P for Pi
%  \closure{P}      == The closure of P.
%  \closureop       == The closure operator.
%  \states          == Set of states
%  \behaviors       == Set of infinite behaviors
%  \finbehaviors    == Set of finite behaviors
%  \WSF             == Either WF or SF.
%  \Nat             == Set of naturals
%  \SIN             == Strongest invariant

%\def\ensuremath#1{\relax\ifmmode #1\else $#1$\fi}
\newcommand{\M}[1]{\ensuremath{[\![#1]\!]}}
\newcommand{\prefix}{\ensuremath{\sqsubset}}
\newcommand{\cat}{\ensuremath{\cdot}}
\newcommand{\valid}[1]{\ensuremath{\models #1}}
\newcommand{\possibly}[2]{\ensuremath{{\bf P}_{{}_{\scriptstyle#1}}(#2)}}
\newcommand{\closure}[1]{\ensuremath{{\cal C}(#1)}}
\newcommand{\closureop}{\ensuremath{{\cal C}}}
\newcommand{\states}{\ensuremath{{\bf S}}}
\newcommand{\behaviors}{\ensuremath{{\bf S}^{\infty}}}
\newcommand{\finbehaviors}{\ensuremath{{\bf S}^{*}}}
\newcommand{\WSF}{\mbox{\rm W/SF}}
\newcommand{\Nat}{{\bf N}}
\newcommand{\SIN}{\ensuremath{sin}}

%%%% Theorem-like environments
\newtheorem{proposition}{Proposition}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                 MODIFICATION DATE                               %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                                 %
% Defines \moddate to expand to modification date such as         %
%                                                                 %
%    5 Aug 1991                                                   %
%                                                                 %
% 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{%                                                       %
%                                                                 %
%                                                                 %
  Last modified on Wed Jun 21 15:13:21 PDT 1995 by lamport        %
  endypmd}                                                        %
%                                                                 %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\moddate}{\expandafter\xpmd\ypmd}                     %
\def\xpmd Last modified                                           %
on #1 #2 #3 #4:#5:#6 #7 #8 by #9 endypmd{#3 #2 #8} %
\newcommand{\prdate}{\noindent\fbox{\Large\moddate}}              %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{document}
%try
\pagenumbering{roman}
\pagestyle{empty}
\vspace*{2.23cm}

\noindent
{\Large \bf Proving Possibility Properties}

\vspace{.5cm}

{\large
\noindent 
Leslie Lamport\\[.25cm]
July 4, 1995}


\clearpage

\mbox{}

\vfill

\noindent
{\bf \copyright Digital Equipment Corporation 1995}\\[\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.

\clearpage



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

A method is described for proving ``always possibly'' properties of
specifications in formalisms with linear-time trace semantics.  It is
shown to be relatively complete for TLA (Temporal Logic of Actions)
specifications.



\cleardoublepage
%\newpage
%try

\tableofcontents

\cleardoublepage
\pagenumbering{arabic}
\pagestyle{plain}


%\thispagestyle{empty}
%try
%\cleardoublepage
\setcounter{page}{1}
\section{Introduction}

Proving possibility properties provides no useful information about a
system.  Why prove that it is possible for a user to press $q$ on the
keyboard and for a $q$ subsequently to appear on the screen?  We know
that the user can always press the $q$ key, and what good is knowing
that a $q$ {\em might\/} appear on the screen?  What we want to prove
is that no $q$ appears on the screen unless a $q$ is typed (a safety
property), and that, if a $q$ is typed, then a $q$ eventually does
appear (a liveness property).

However, we do not reason about a system; we reason about a
mathematical model of a system.  A possibility property can provide a
sanity check on our model.  Proving that it is always possible for a
$press(q)$ action to occur tells us something useful about the model.
In general, we want to prove that a model allows the occurrence of
actions representing events that the system cannot prevent.

We present a method for proving that it is always possible for some
state or action eventually to occur.  This seems to be the most useful
class of possibility properties.  We first describe the general
approach, which applies to any formalism with a linear-time semantics.
We then show how the method is used with TLA, the Temporal Logic of
Actions~\cite{lamport:newtla}, and prove a relative completeness
result.

Possibility properties pose no problem in formalisms based on
branching-time semantics~\cite{emerson:chapter}.  However, it is
impossible to assert in linear-time temporal logic that something is
always possible~\cite{lamport:sometime}.  It is therefore not obvious
how to prove possibility properties in the formalisms that we
consider, which are based on linear-time semantics.


\section{Possibility and Closure}

\subsection{Closure and Safety}

We begin by reviewing some basic concepts of linear-time temporal
logic~\cite{manna:temporal}.  A behavior is an infinite sequence of
states or of events---for now, it doesn't matter which.  The meaning
\M{\Pi} of a temporal-logic formula $\Pi$ is a Boolean-valued function
on behaviors.  We say that the behavior $\sigma$ satisfies $\Pi$ iff
(if and only if) $\M{\Pi}(\sigma)$ equals \TRUE. Formula $\Pi$ is
valid, written \valid{\Pi}, iff every behavior satisfies $\Pi$.  To
use temporal logic to specify (a mathematical model of) a system, we
consider states to represent possible system states and events to
represent possible system actions, so a behavior represents a
conceivable execution of a system.  A system is specified by a formula
$\Pi$ that is satisfied by precisely those behaviors that represent a
legal system execution.

Boolean operations on formulas are defined in the obvious way;
for example, 
 $\M{\Pi /\ \Phi}(\sigma)\deq\M{\Pi}(\sigma) /\ \M{\Phi}(\sigma)$.
We define $[]\Pi$ to be the formula that is satisfied by a behavior
$\sigma$ iff every suffix of $\sigma$ satisfies $\Pi$, and we define
$<>\Pi$ to be satisfied by $\sigma$ iff some suffix of $\sigma$
satisfies $\Pi$.  The operators $[]$ and $<>$ are read {\em always\/}
and {\em eventually}, respectively.  We define $~>$ by
$\Pi ~> \Phi \;\deq\; [](\Pi=><>\Phi)$.

Let \behaviors\ be the set of all behaviors, let \finbehaviors\ be
the set of all finite behaviors (finite prefixes of elements of
\behaviors), let ``\cat'' be concatenation of sequences, and let
$\rho\prefix\sigma$ mean that $\rho$ is a finite prefix of the
behavior $\sigma$.  
The {\em closure\/} \closure{\Pi} of a formula $\Pi$ is defined by
\begin{equation} \label{eq:closure}
 \M{\closure{\Pi}}(\sigma) == 
  \forall \rho \prefix \sigma : \exists \tau \in \behaviors: 
                                  \M{\Pi}(\rho\cat\tau)
\end{equation} 
where $\forall\rho\prefix\sigma$ is universal quantification over all
finite prefixes $\rho$ of $\sigma$.  Thus, a behavior $\sigma$
satisfies \closure{\Pi} iff every finite prefix of $\sigma$ can be
extended to a behavior that satisfies $\Pi$.  The following proposition
follows easily from (\ref{eq:closure}).
\begin{proposition} \label{prop:closure}
For any formulas $\Pi$ and $\Phi$:
\begin{enumerate} 
\item $|= \Pi => \closure{\Pi}$ \label{item:superdiagonal}
\item $\valid{\Pi=>\Phi}$ implies $\valid{\closure{\Pi}=>\closure{\Phi}}$
          \label{item:monotonic}
\end{enumerate}
\end{proposition}

A {\em safety\/} formula is one that equals its closure.  Thus, a
safety formula $\Pi$ is satisfied by a behavior $\sigma$ iff every
prefix of $\sigma$ can be extended to a behavior satisfying $\Pi$.
%
% Formally, it follows from (\ref{eq:closure}) that $\Pi$ is a safety
% formula iff
% \begin{equation} \label{eq:safety}
%  \forall\sigma\in\behaviors: \M{\Pi}(\sigma) \equiv
%    \forall\rho\prefix\sigma: \exists\tau : \M{\Pi}(\rho\cat\tau)
%\end{equation}
%
Intuitively, a safety property $\Pi$ constrains only the finite
behavior of a system---any behavior that fails to satisfy $\Pi$ fails
at some specific instant.  More precisely, $\Pi$ is a safety
property iff
\begin{equation} \label{eq:not-safety}
  \forall\sigma\in\behaviors : \M{~\Pi}(\sigma) \,\equiv\,
   \exists\rho\prefix\sigma :
   \forall\tau\in\behaviors : \M{~\Pi}(\rho\cat\tau)
\end{equation}


\subsection{Possibility}

We now define a class of possibility properties and relate them to
closure.  The properties are of the form {\em always possibly\/} $P$,
meaning that at all times during an execution of the system, it is
possible for $P$ eventually to become true.  In linear-time temporal
logic, it is impossible to write a formula whose meaning is always
possibly $P$~\cite{lamport:sometime}.  However, for any particular
system, we can write a formula asserting that always possibly $P$
holds for behaviors of that system.  More precisely, we can define a
formula \possibly{\Pi}{P} such that always possibly $P$ holds for the
system specified by $\Pi$ iff \possibly{\Pi}{P} is valid.

Intuitively, always possibly $P$ holds for a system iff, at any point
during any execution of the system, it is possible to choose some
particular way of continuing the execution that makes $P$ eventually
hold.  In other words, if $\rho$ is the prefix of a behavior
satisfying the system's specification $\Pi$, there exists a behavior
$\tau$ such that $\rho\cat\tau$ satisfies $\Pi$, and $P$ holds at some
point in $\tau$.  We can therefore define \possibly{\Pi}{P} by
 \begin{equation} \label{eq:possibly}
 \M{\possibly{\Pi}{P}}(\sigma) ==
    \M{\Pi}(\sigma) => 
       \forall \rho \prefix \sigma : \exists \tau : \M{\Pi}(\rho\cat\tau)
              /\ \M{<>P}(\tau)
 \end{equation}
Our method of proving possibility properties is based on the following
result.  It and all subsequent propositions are proved in the
appendix.
%
\begin{proposition} \label{prop:closure-implies-possible}
If $~P$ is a safety property, then
 \[ \valid{\;(\closure{\Pi}=>\closure{\closure{\Pi} /\ []<>P})
      \;=>\; \possibly{\Pi}{P}}
 \]
\end{proposition}
We will use this result when $\M{P}(\sigma)$ depends only on the first
one or two elements of $\sigma$.  By (\ref{eq:not-safety}), $~P$ is a
safety property for such a $P$.


\section{Proving Possibility Properties in TLA}

\subsection{TLA}

To apply Proposition~\ref{prop:closure-implies-possible}, we need to
compute closures.  One can write TLA specifications in a way that
makes computing the closure easy.  We now give a thumbnail review of
TLA; see~\cite{lamport:newtla} for a real explanation of the logic.

In TLA, behaviors are infinite sequences of states, where a {\em
state\/} is an assignment of variables to values.  We let \states\ be
the set of all states.  Formulas are built from actions, Boolean
operators, and the temporal operator $[]$.  An {\em action\/} is a
Boolean expression containing primed and unprimed variables.  For
states $s$ and $t$, we define $\M{A}(s,t)$ to equal \TRUE\ iff $A$
holds with values from $s$ substituted for unprimed variables and with
values from $t$ substituted for primed variables.  We consider action
$A$ to be a temporal formula by letting
$\M{A}(s_{0},s_{1},s_{2},\ldots)$ equal $\M{A}(s_{0},s_{1})$.

A {\em state predicate\/} $P$ is an action with no primed variables; we write
$\M{P}(s)$ instead of $\M{P}(s,t)$, which is independent of $t$.  For
an action $A$, we define the predicate $\ENABLED A$ by 
 $\M{\ENABLED A}(s) \deq \exists t\in\states:\M{A}(s,t)$.  
A {\em state function\/} is a nonBoolean expression containing unprimed
variables.  For any state function $v$, we let $[A]_{v}\deq A \/
(v'=v)$ and $<<A>>_{v}\deq A /\ (v'#v)$, where $v'$ is the expression
obtained by priming the free variables in $v$.

The canonical form of a TLA formula is $Init /\ [][N]_{v} /\ F$, where
$Init$ is a state predicate, $N$ an action, $v$ a state function, and
$F$ the conjunction of formulas of the form $\WF_{v}(A)$ or
$\SF_{v}(A)$, with
 \[ \begin{noj3}
     \WF_{v}(A) & \deq & []<>~\ENABLED <<A>>_{v} \/ []<><<A>>_{v} \\
     \SF_{v}(A) & \deq & <>[]~\ENABLED <<A>>_{v} \/ []<><<A>>_{v} \\
    \end{noj3}
 \]
For example, a system that starts with $x$ and $y$ both 0, and
repeatedly either increments $x$ by $\pm 1$ or, if $x$ equals 0,
increments $y$ by $\pm1$, is specified by the following formula
$\Pi{}xy$.\footnote{A list of formulas bulleted with $\land$ or $\lor$
 denotes the conjunction or disjunction of the formulas; indentation is
 used to eliminate parentheses.%
 % We also let $=>$ have
 % lower precedence than the other Boolean operators.
}
%
 \[ \begin{noj3}
    Nxy  & \deq & \begin{disj}
              \begin{conj}
                x'\in\{x+1, x-1\} \\ y'=y 
              \end{conj}\\
              \begin{conj}
                x =x'=0 \\ y'\in \{y+1, y-1\}
              \end{conj}
         \end{disj}\\
    \Pi{}xy & \deq & (x=y=0) /\ [][Nxy]_{<<x,y>>} /\ \WF_{<<x,y>>}(Nxy)
   \end{noj3}
 \] 
The fairness condition $\WF_{<<x,y>>}(Nxy)$ asserts that
the system never stops.

TLA also has an operator $\EE$, where $\EE x : \Pi$ is essentially
$\Pi$ with variable $x$ hidden.  The system specified by
 $\EE x : \Pi$ satisfies a possibility property iff $\Pi$ does, so we 
ignore the $\EE$ operator here.  Using $\EE$, we can express
\possibly{\Pi}{P} and \closure{\Pi} as TLA formulas, for any formulas
$\Pi$ and $P$.  Propositions~\ref{prop:closure} and
\ref{prop:closure-implies-possible} can then be proved by
temporal-logic reasoning.

Closures of TLA formulas are computed using the following result.
%
\begin{proposition} \label{prop:computing-closure}
If $Init$ is a state predicate, $M$ implies $N$, and $F$ is the
conjunction of countably many formulas of the form $\WF_{v}(A)$ and/or
$\SF_{v}(A)$, where each $<<A>>_{v}$ implies $M$, then
  \[\closure{Init /\ [][N]_{v} /\ <>[][M]_{v} /\ F} \equiv Init /\ [][N]_{v}\]
\end{proposition}
%
Since $[]\Pi$ implies $<>[]\Pi$, for any $\Pi$, substituting $Nxy$ for
both $N$ and $M$ in the proposition proves that
$\closure{\Pi{}xy}\,\equiv\,(x=y=0) /\ [][Nxy]_{<<x,y>>}$.  For $M=N$,
Proposition~\ref{prop:computing-closure} is a special case of
Proposition~2 of~\cite{abadi:old-fashioned}.  

A formula of the form $Init /\ [][N]_{v} /\ F$ is called 
 {\em machine closed\/}~\cite{abadi:old-fashioned} if its closure equals 
$Init /\ [][N]_{v}$.  Proposition~\ref{prop:computing-closure} implies
that such a formula is machine closed if $F$ is the conjunction of
fairness conditions for actions that imply $N$.  It can be argued that
any specification that models a real implementation should be machine
closed, and that possibility properties need be proved only for a
model of an implementation, not for a high-level specification.


\subsection{The Proof Method}

We now show how to use Propositions \ref{prop:closure},
\ref{prop:closure-implies-possible}, and \ref{prop:computing-closure}
to prove possibility properties of the form \possibly{\Pi}{P} for a
state predicate $P$, where $\Pi$ equals $Init /\ [][N]_{v} /\ F$, and
\closure{\Pi} equals $Init /\ [][N]_{v}$.  For any action
$A$, formula \possibly{\Pi}{A} is equivalent to
$\possibly{\Pi}{\ENABLED([N]_{v} /\ A)}$.  Hence, our method
can be used to prove properties \possibly{\Pi}{A} for arbitrary
actions $A$.

To prove \possibly{\Pi}{P}, we find an action $M$ and a conjunction
$G$ of fairness properties such that 
\begin{equation} \label{eq:method1}
   Init /\ [][N]_{v} /\ <>[][M]_{v} /\ G => []<>P
\end{equation}
and for which we can use Proposition~\ref{prop:computing-closure} to
prove
\begin{equation} \label{eq:method2}
  \closure{Init /\ [][N]_{v} /\ <>[][M]_{v} /\ G} \equiv Init /\ [][N]_{v}
\end{equation}
We then deduce \possibly{\Pi}{P} as follows.
\begin{proof}
\pfshortnumbers{99}
\pflongindent
\step{1}{$Init /\ [][N]_{v} /\ <>[][M]_{v} /\ G => 
              Init /\ [][N]_{v} /\ []<>P$}
   \begin{proof}
   \pf\ (\ref{eq:method1}).
   \end{proof}

\step{2}{$Init /\ [][N]_{v} => \closure{Init /\ [][N]_{v} /\ []<>P}$}
  \begin{proof}
    \pf\ (\ref{eq:method2}) and part~\ref{item:monotonic} of 
    Proposition~\ref{prop:closure}.
  \end{proof}

\qedstep
  \begin{proof}
    \pf\ By Proposition~\ref{prop:closure-implies-possible}, since
    $Init /\ [][N]_{v} \equiv\closure{\Pi}$.
  \end{proof}
\end{proof}
\noindent
For example, to prove $\possibly{\Pi{}xy}{y=17}$, we take
\[ M == \begin{disj}
           \begin{conj}
                 ((x > 0) /\ (x' = x-1)) 
                 \,\/ \, ((x < 0) /\ (x' = x+1)) \\
                y'=y
           \end{conj} \\
          \begin{conj}
                x =x'=0 \\ 
                ((y > 17) /\ (y' = y-1))
                \,\/ \, ((y < 17) /\ (y' = y+1))
          \end{conj}
        \end{disj}\]
To prove (\ref{eq:method1}), we use the TLA rules from Figure~5
(page~888) of~\cite{lamport:newtla}.

We now show that this proof method is complete relative to
non-temporal reasoning about actions.  This means that if all the
necessary valid action formulas can be proved, then every valid
formula \possibly{\Pi}{P} is provable.  We write $|- \Psi$ to mean
that formula $\Psi$ is provable from Propositions~\ref{prop:closure},
\ref{prop:closure-implies-possible}, and \ref{prop:computing-closure}
and the rules in~\cite{lamport:newtla}.

Our results assume only that valid actions in some class of {\em
expressible\/} formulas are provable.  We assume that expressible
terms and formulas are closed under the operations of first-order
logic (conjunction, quantification, etc.),\ priming, and forming
tuples.  Relative completeness results for programming logics are
generally based on some form of predicate transformer analogous to the
\SIN\ operator of~\cite{lamport:win}.  For any action $A$ and state
predicate $P$, the state predicate $\SIN(A, P)$ can be defined by%
\begin{equation} \label{eq:sin}
 \begin{noj}
 \M{\SIN(A, P)}(s) == \\
 \s{1}  \exists s_{0}, \ldots, s_{n} \in\states :
          (s=s_{n}) /\ \M{P}(s_{0}) /\ (\forall i < n : \M{A}(s_{i},s_{i+1}))
 \end{noj}
\end{equation}
for all states $s$.  We first show completeness of the TLA rules
for proving invariance properties.


\begin{proposition} \label{prop:invariance-complete}
For any predicates $I$ and $Init$, state function $v$, and action $N$,
if
\begin{enumerate} 
  \item \label{ass1:relative-completeness}
           Every valid expressible action formula is provable.
  \item \label{ass1:expressible}
           $I$, $Init$, $v$, $N$, and $\SIN([N]_{v},Init)$ are expressible.
  \item  \label{ass1:valid}
         $|= Init /\ [][N]_{v} => []I$
\end{enumerate}
then \ $|- Init /\ [][N]_{v} => []I$.
\end{proposition}
Proposition~\ref{prop:invariance-complete} is essentially the TLA
version of the classical completeness results for Hoare
logics~\cite{apt:ten-years}.  We use it to show completeness 
of our method for proving possibility properties:%
%\pagebreak[0]
\begin{proposition} \label{prop:possibility-completeness}
If  
\begin{enumerate} 
  \item \label{ass:relative-completeness}
           Every valid expressible action formula is provable.
     \item \label{ass:expressible}
           $P$, $Init$, $v$, $N$, and $\SIN([N]_{v},Init)$ are expressible. 
     \item \label{ass:closure}
           $|- \closure{\Pi} \equiv Init /\ [][N]_{v}$
     \item \label{ass:possible}
           $|= \possibly{\Pi}{P}$
\end{enumerate}
then \ $|- \possibly{\Pi}{P}$.
\end{proposition}

\section{Conclusion}

Proving possibility properties provides a way of checking that the
mathematical models we make of our systems are sensible.  For real
time specifications, an important possibility property is nonZenoness,
which asserts that it is always possible for time to advance.  The
relation between possibility and closure was first observed for
nonZenoness in \cite{abadi:old-fashioned}.  Our method generalizes a
method described there for proving nonZenoness.

Propositions~\ref{prop:closure} and
\ref{prop:closure-implies-possible} are independent of TLA\@.  They
can be used for proving possibility properties in any trace-based
specification method for which closures can be computed.  It is easy
to compute closures when specifications are written as certain kinds
of transition systems.  For example, the closure of (the
temporal-logic formula corresponding to) a B\"{u}chi
automaton~\cite{alpern:recognizing} with a strongly connected state graph
is the automaton obtained by making every state an accepting state.
The closure of a specification written as a state transition
system~\cite{lam:specifying,lynch:hierarchical} 
 %% or an I/O automaton~\cite{
is obtained by removing the fairness properties, if those properties
are expressed as fairness conditions on transitions.  We do not know
of any practical method for computing the closure of arbitrary
temporal-logic formulas, or of transition systems with arbitrary
temporal formulas as fairness requirements.  We do not know how to
prove possibility properties for traditional temporal-logic
specifications~\cite{manna:temporal}.

\addcontentsline{toc}{section}{Acknowledgments}
\subsection*{Acknowledgments}

Mart\'{\i}n Abadi and Stephan Merz pointed out mistakes in the text of
an earlier version.  Fred Schneider suggested some improvements to the
presentation.

\clearpage
%try


\bibliographystyle{plain}
\addcontentsline{toc}{section}{References}
%\bibliography{mybib}
\begin{thebibliography}{10}

\bibitem{abadi:old-fashioned}
Mart\'{\i}n Abadi and Leslie Lamport.
\newblock An old-fashioned recipe for real time.
\newblock {\em ACM Transactions on Programming Languages and Systems},
  16(5):1543--1571, September 1994.

\bibitem{alpern:recognizing}
Bowen Alpern and Fred~B. Schneider.
\newblock Recognizing safety and liveness.
\newblock {\em Distributed Computing}, 2(3):117--126, 1987.

\bibitem{apt:ten-years}
Krzysztof~R. Apt.
\newblock Ten years of {H}oare's logic: A survey---part one.
\newblock {\em ACM Transactions on Programming Languages and Systems},
  3(4):431--483, October 1981.

\bibitem{emerson:chapter}
E.~Allen Emerson.
\newblock Temporal and modal logic.
\newblock In Jan van Leeuwen, editor, {\em Handbook of Theoretical Computer
  Science}, volume~B, chapter~16, pages 995--1072. Elsevier and MIT Press,
  Amsterdam and Cambridge, Massachusetts, 1990.

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

\bibitem{lamport:sometime}
Leslie Lamport.
\newblock `{S}ometime' is sometimes `not never': A tutorial on the temporal
  logic of programs.
\newblock In {\em Proceedings of the Seventh Annual Symposium on Principles of
  Programming Languages}, pages 174--185. ACM SIGACT-SIGPLAN, January 1980.

\bibitem{lamport:win}
Leslie Lamport.
\newblock {\em win\/} and {\em sin\/}: Predicate transformers for concurrency.
\newblock {\em ACM Transactions on Programming Languages and Systems},
  12(3):396--428, July 1990.

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

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

\end{thebibliography}


%try
\clearpage
\appendix
\section*{Appendix}
\addcontentsline{toc}{section}{Appendix}
\setcounter{section}{1}

We now prove Propositions
\ref{prop:closure-implies-possible}--\ref{prop:possibility-completeness}.
The proofs use a hierarchical style in which the proof of statement
\pfstepnumber{i}{j}{?} is either an ordinary paragraph-style proof or
the sequence of statements \pfstepnumber{i+1}{1}{?},
\pfstepnumber{i+1}{2}{?}, \ldots\ and their proofs.  We recommend
reading proofs top-down---reading the proof of a level-$k$ step by
first reading the level-\mbox{$(k\!+\!1)$} statements that form the
proof, together with the proof of the final Q.E.D. step, and then
reading the proofs of the level-\mbox{$(k\!+\!1)$} steps in any order.

\subsection{Proof of Proposition~\protect\ref{prop:closure-implies-possible}}

To prove the proposition, we must prove that if a behavior $\sigma$
satisfies $\closure{\Pi}=>\closure{\closure{\Pi} /\ []<>P}$, then it
satisfies \possibly{\Pi}{P}.  By the definition (\ref{eq:possibly}) of
\possibly{\Pi}{P}, the proposition is proved as follows.
%
\assume{\begin{pfenum}
         \item $\M{\Pi}(\sigma)$ 
         \item $\M{\closure{\Pi}=>\closure{\closure{\Pi} /\ []<>P}}(\sigma)$
        \end{pfenum}}
\prove{$\forall \rho \prefix \sigma : \exists \tau : \M{\Pi}(\rho\cat\tau)
              /\ \M{<>P}(\tau)$}
\begin{proof} %\small
\step{<1>1}{$\forall \rho\prefix\sigma : 
               \exists \eta \in \behaviors : \M{\closure{\Pi}}(\rho\cat\eta) 
                              /\ \M{[]<>P}(\rho\cat\eta)$}
\begin{proof}
  \step{<2>1}{$\M{\closure{\Pi}(\sigma)}$}
  \begin{proof}
    \pf\ Assumption 1 and part~\ref{item:superdiagonal} of 
     Proposition~\ref{prop:closure}.
  \end{proof}

  \step{<2>2}{$\closure{\closure{\Pi} /\ []<>P}(\sigma)$}
  \begin{proof}
    \pf\ \stepref{<2>1}, assumption 2, and the definition of $=>$ for 
    temporal formulas.
  \end{proof}

  \qedstep
  \begin{proof}
    \pf\ \stepref{<2>2}, (\ref{eq:closure}),
    and the definition of $/\ $ for temporal formulas.
  \end{proof}
\end{proof}

\step{<1>2}{$\forall \rho\prefix\sigma : 
                  \exists \xi \in \finbehaviors : 
                   \begin{conj}
                   \exists \phi \in \behaviors  : 
                        \M{\Pi}(\rho\cat\xi\cat\phi) \\
                        \forall \chi \in \behaviors : 
                              \M{<>P}(\xi\cat\chi)
                   \end{conj}$}
\begin{proof}
  \step{<2>1}{$\forall \rho\in\finbehaviors, \eta\in\behaviors:
                 \M{[]<>P}(\rho\cat\eta) => 
                    \exists \eta_{1}, \eta_{2} :
                       \eta=\eta_{1}\cat\eta_{2}
                         /\ \M{P}(\eta_{2})$}
  \begin{proof}
    \pf\ By definition of $[]$ and $<>$.
  \end{proof}
  \step{<2>2}{$\forall \eta_{2}\in\behaviors:
                 \M{P}(\eta_{2}) => 
                    \exists \eta_{3}\prefix\eta_{2} :  
                      \forall \chi \in \behaviors : \M{P}(\eta_{3}\cat\chi)$}
  \begin{proof}
   \pf\ By the hypothesis that $~P$ is a safety property and
   (\ref{eq:not-safety}) (substituting $~P$ for $\Pi$).
  \end{proof}

  \step{<2>3}{$\forall \rho\in\finbehaviors, \eta\in\behaviors:
                 \M{[]<>P}(\rho\cat\eta) => 
                    \exists \xi\prefix\eta : 
                      \forall \chi \in \behaviors : \M{<>P}(\xi\cat\chi)$}
  \begin{proof}
    \pf\ By \stepref{<2>1}, \stepref{<2>2}, and the definition of $<>$, 
    taking $\eta_{1}\cat\eta_{3}$ for $\xi$.
  \end{proof}

  \step{<2>4}{$\forall \rho\in\finbehaviors, \eta\in\behaviors,
               \xi\prefix\eta :
                 \M{\closure{\Pi}}(\rho\cat\eta) => 
                   \exists \phi \in \behaviors  : 
                        \M{\Pi}(\rho\cat\xi\cat\phi)$}
  \begin{proof}
    \pf\ By the definition (\ref{eq:closure}) of \closureop.
  \end{proof}

  \qedstep
  \begin{proof}
    \pf\ \stepref{<1>1}, \stepref{<2>3}, and \stepref{<2>4}.
  \end{proof}
\end{proof}

\qedstep
  \begin{proof}
   \pf\ By \stepref{<1>2}, letting $\tau$ be $\xi\cat\phi$
   and substituting $\phi$ for $\chi$.
  \end{proof}
\end{proof}

\subsection{Proof of Proposition~\protect\ref{prop:computing-closure}}

We prove the proposition for the special case that $F$ consists of
a single \WF\ or \SF\ formula, which is the only case used here.  The
general case is handled much as in the proof of Proposition~2 of
\cite{abadi:old-fashioned}.  In the following proof, $\WSF$ denotes
either \WF\ or \SF.
%
\assume{\begin{pfenum}
         \item $\valid{M => N}$
         \item $\valid{<<A>>_{v} => M}$
         \item $\sigma\in\behaviors$
        \end{pfenum}}
\prove{$\M{\closure{Init /\ [][N]_{v} /\ <>[][M]_{v} /\ \WSF_{v}(A)}}(\sigma)
          \equiv \M{Init /\ [][N]_{v}}(\sigma)$}
\begin{proof} %\small
\step{<1>1}{\assume{$\forall\rho\prefix\sigma: \exists \tau: 
                     \M{Init /\ [][N]_{v} /\ <>[][M]_{v} 
                         /\ \WSF_{v}(A)}(\rho\cat\tau)$}
            \prove{$\M{Init /\ [][N]_{v}}(\sigma)$}}
  \begin{proof}
    \pf\ Assumption~\levelref{<1>1} (from this step) implies 
      that $Init$ holds in the 
      first state of $\sigma$ and $[N]_{v}$ holds in every pair of 
      successive states of $\sigma$, which implies 
      $\M{Init /\ [][N]_{v}}(\sigma)$ by definition of $[]$ and of $\M{B}$
      for an action $B$.
  \end{proof}

\step{<1>2}{\assume{\begin{pfenum}
                     \item $\M{Init /\ [][N]_{v}}(\sigma)$
                     \item $\rho\prefix\sigma$                    
                    \end{pfenum}}
            \prove{$\exists\tau: \M{Init 
               /\ [][N]_{v} /\ <>[][M]_{v} /\ \WSF_{v}(A)}(\rho\cat\tau)$}}

  \begin{proof}
    \step{<2>1}{Choose states $s_{0}$, $s_{1}$, \ldots  such that 
        $\rho=s_{0}, \ldots, s_{n}$ and, for $i\geq n$, 
         \[ \begin{conj}
           \M{\ENABLED<<A>>_{v}}(s_{i}) => \M{<<A>>_{v}}(s_{i},s_{i+1}) \\
           ~\M{\ENABLED<<A>>_{v}}(s_{i}) => (s_{i+1} = s_{i})
         \end{conj}
        \]}
    \begin{proof}
      \pf\ The existence of the $s_{i}$ follows from the definition
      of \ENABLED.
    \end{proof}

    \step{<2>2}{$\M{[][M]_{v}}(s_{n}, s_{n+1}, \ldots$)}
    \begin{proof}
      \step{<3>1}{$\forall i\geq n: \M{[M]_{v}}(s_{i},s_{i+1})$}
      \begin{proof}
        \pf\ If $\M{\ENABLED<<A>>_{v}}(s_{i})$, this follows from
        assumption~2.  If 
       $~\M{\ENABLED<<A>>_{v}}(s_{i})$, this follows because
       $\M{[M]_{v}}(s,s)$ holds for any state~$s$.
      \end{proof}
     \qedstep
     \begin{proof}
       \pf\ \stepref{<3>1} and the definitions of $[]$ and
       of $\M{B}$ for an action $B$.
     \end{proof}
    \end{proof}

    \step{<2>3}{$\M{\WSF_{v}(A)}(s_{0}, s_{1}, \ldots$)}
    \begin{proof} % \sloppypar
       \pf\ $[]<>\ENABLED<<A>>_{v}$ implies $\M{\ENABLED<<A>>_{v}}(s_{i})$
       for infinitely many $i$, which by \stepref{<2>1} implies
       $\M{<<A>>_{v}}(s_{i},s_{i+1})$ for infinitely many $i$,
       which implies $\M{[]<><<A>>_{v}}(s_{0}, s_{1}, \ldots)$.
       The result then follows from the definition of \WF\ and
       \SF, since 
       $~[]<>\ENABLED<<A>>_{v}$ is equivalent to $<>[]~\ENABLED<<A>>_{v}$,
      which implies $[]<>~\ENABLED<<A>>_{v}$.
% $~[]<>\Pi$ implies $<>[]~\Pi$ which implies $[]<>~\Pi$,
% for any~$\Pi$.
     \end{proof}

    \step{<2>4}{$\M{[][N]_{v}}(s_{0}, s_{1}, \ldots)$}
    \begin{proof}
      \step{<3>1}{$\forall i : \M{[N]_{v}}(s_{i},s_{i+1})$}
      \begin{proof}
        \step{<4>1}{\assume{$i < n$}\prove{$\M{[N]_{v}}(s_{i},s_{i+1})$}}
        \begin{proof}
          \pf\ \stepref{<2>1} and assumptions \levelref{<1>2}:1 and 
          \levelref{<1>2}:2 (from step \stepref{<1>2}).
        \end{proof}
%\pagebreak 
        \step{<4>2}{\assume{$i\geq n$}\prove{$\M{[N]_{v}}(s_{i},s_{i+1})$}}
        \begin{proof}
           \pf\ By \stepref{<2>1} and, if $\M{\ENABLED<<A>>_{v}}(s_{i})$, 
           then by assumptions 
           1 and 2, else
           by definition of $[N]_{v}$.
        \end{proof}
        \qedstep
        \begin{proof}
          \pf\ \stepref{<4>1} and \stepref{<4>2}.
        \end{proof}
      \end{proof}

      \qedstep
      \begin{proof}
       \pf\ \stepref{<3>1} and the definitions of $[]$ and
       of $\M{B}$ for an action $B$.
      \end{proof}
    \end{proof}    

    \qedstep
    \begin{proof}
      \pf\ \stepref{<2>2}, \stepref{<2>3}, \stepref{<2>4}, 
      the definition of \M{Init}, and the
      definition of $<>$, taking $s_{n}, s_{n+1}, \ldots$ for~$\tau$.
    \end{proof}     
  \end{proof}
\qedstep
  \begin{proof}
   \pf\ \stepref{<1>1}, \stepref{<1>2}, and the definition (\ref{eq:closure})
    of \closureop.
  \end{proof}
\end{proof}

\subsection{Proof of Proposition~\protect\ref{prop:invariance-complete}}

\begin{proof} %\small
\step{<1>1}{$|- Init /\ [][N]_{v} => []\SIN([N]_{v},Init)$}
\begin{proof}
  \step{<2>1}{$|= Init => \SIN([N]_{v}, Init)$}
  \begin{proof}
    \pf\ Definition (\ref{eq:sin}) of \SIN.
  \end{proof}

  \step{<2>2}{$|= [N]_{v} /\ \SIN([N]_{v}, Init) => \SIN([N]_{v}, Init)'$}
  \begin{proof}
    \pf\  Definition (\ref{eq:sin}) of \SIN.
  \end{proof}

  \step{<2>3}{$|- \SIN([N]_{v}, Init) /\ [][N]_{v} => []\SIN([N]_{v},Init)$}
  \begin{proof}
    \pf\ \stepref{<2>2}, assumption~\ref{ass1:relative-completeness}, 
    and proof rule INV1.
  \end{proof}

  \qedstep
  \begin{proof}
    \pf\ \stepref{<2>1}, \stepref{<2>3}, and
    assumption~\ref{ass1:relative-completeness}.
  \end{proof}
\end{proof}

\step{<1>2}{$|- \SIN([N]_{v},Init) => I$}
  \begin{proof}
    \step{<2>1}{$\forall s\in\states :
      \begin{noj} \M{\SIN([N]_{v},Init)}(s) => \\
        \s{1} \exists s_{0}, \ldots, s_{n}\in\states :
         \M{Init /\ [][N]_{v}}(s_{0}, \ldots, s_{n},  s, s, s,
                \ldots)
       \end{noj} $}
    \begin{proof}
      \pf\ Definition (\ref{eq:sin}) of \SIN, and the definitions of $[]$
      and $[N]_{v}$.
    \end{proof}

    \step{<2>2}{$\forall s, s_{0}, \ldots, s_{n} \in\states : 
     \M{Init /\ [][N]_{v}}(s_{0}, \ldots, s_{n},  s, s, s, \ldots)
            => \M{I}(s)$}
    \begin{proof}
     \pf\ Assumption~\ref{ass1:valid} and definition of $[]I$.
    \end{proof}

    \step{<2>3}{$|= \SIN([N]_{v},Init) => I$}
    \begin{proof}
     \pf\ \stepref{<2>1} and \stepref{<2>2}.
    \end{proof}

    \qedstep
    \begin{proof}
     \pf\ \stepref{<2>3} and assumption~\ref{ass1:relative-completeness}.
    \end{proof}
   \end{proof}

\qedstep
\begin{proof}
 \pf\ \stepref{<1>1}, \stepref{<1>2}, and proof rule STL4 
 of~\cite{lamport:newtla}.
\end{proof}
\end{proof}

\subsection{Proof of Proposition~\protect\ref{prop:possibility-completeness}}

Let \Nat\ be the set of natural numbers and let $x_{1}$, \ldots,
$x_{n}$ be the free variables of $P$.  Since $[N]_{v} \equiv
[[N]_{v}]_{<<v,w>>}$, by replacing $N$ with $[N]_{v}$ and $v$ with
$<<v, x_{1}, \ldots, x_{n}>>$, we can assume:
\begin{enumerate}
  \setcounter{enumi}{4}\it
  \item \label{ass:unchanged}
             $|= (v'=v) => (P'=P)$ 
\end{enumerate}
In the following proof, $P_{n}$ is the predicate that is true iff $P$
can be made true by taking $n$ $N$-steps, but with no fewer than $n$
such steps.  

\begin{proof} %\small
  \pflet{$P_{n} == \IF{n=0} \THEN P\\
                           \ELSE \begin{conj}
                                   \forall i < n : ~P_{i} \\
                                   \ENABLED(N /\ (v'#v) /\ P'_{n-1})
                                 \end{conj}
                   \FI$\\
         $M == N /\ (\forall n : P_{n+1} => P'_{n})$}

  \step{<1>1}{$|- Init /\ [][N]_{v} => [](\exists n : P_{n})$}
  \begin{proof}
    \pflet{$\pi(s,n) == \exists s_{0}, \ldots, s_{n} :
                            \begin{conj}
                      (s = s_{0}) /\ \M{P}(s_{n}) \\
                      \forall i < n : \M{N /\ (v'#v)}(s_{i}, s_{i+1})
                    \end{conj}$}

    \step{<2>1}{$\forall (s_{0}, s_{1}, \ldots) \in \behaviors : \\
                 \s{1}\M{Init /\ [][N]_{v}}(s_{0}, s_{1}, \ldots)
                    => \forall i \in \Nat : \exists n \in \Nat : 
                         \pi(s_{i},n)$}
    \begin{proof}
      \pf\ Assumptions~\ref{ass:possible} and
       \ref{ass:unchanged} and
      the definition (\ref{eq:possibly}) of \possibly{\Pi}{P}.
    \end{proof}

    \step{<2>2}{$\forall s\in\states, n\in\Nat: 
                  \M{P_{n}}(s) \equiv \pi(s,n) /\ (\forall i < n : ~\pi(s,i))$}
    \begin{proof}
     \pf\ By induction on $n$ from the definitions of $P_{n}$, 
     $\pi$, and \ENABLED.
    \end{proof}

    \step{<2>3}{$\forall s\in\states: \M{\exists n : P_{n}}(s)
                   \equiv (\exists n\in\Nat:\pi(s,n))$}
    \begin{proof}
      \pf\ \stepref{<2>2}.
    \end{proof}

    \step{<2>4}{$|= Init /\ [][N]_{v} => [](\exists n : P_{n})$}
    \begin{proof}
      \pf\ \stepref{<2>1}, \stepref{<2>3}, and the definitions of 
      $[]$ and \M{[N]_{v}}.
    \end{proof}
    \qedstep
    \begin{proof}
      \pf\ \stepref{<2>4}, 
      assumptions~\ref{ass:expressible} and 
      \ref{ass:relative-completeness},
      and Proposition~\ref{prop:invariance-complete}, since
      $\ENABLED A$ is obtained by existential quantification over
      the primed variables of $A$, so it is expressible 
      if $A$ is, for any action $A$.
    \end{proof}
  \end{proof} %%%<1>1


  \step{<1>2}{\assume{$k\in\Nat$}
        \prove{$|- [](\exists n : P_{n}) /\ [][M]_{v} 
                  /\ \WF_{v}(M) => (P_{k+1} ~> P_{k})$}}
  \begin{proof}
    \step{<2>1}{$|- P_{k+1} /\ [M]_{v} => P'_{k+1} \/ P'_{k}$}
    \begin{proof}
      \pf\ Definition of $M$ and 
       assumption~\ref{ass:unchanged}.
    \end{proof}

    \step{<2>2}{$|- P_{k+1} /\ <<M>>_{v} => P'_{k}$}
    \begin{proof}
      \pf\ Definition of $M$.
    \end{proof}

    \step{<2>3}{$|- P_{k+1} => \ENABLED<<M>>_{v}$}
    \begin{proof}
      \step{<3>1}{$|= P_{k+1} => \forall n#(k+1) : ~P_{n}$}
      \begin{proof}
        \pf\ Definition of $P_{n}$.
      \end{proof}

      \step{<3>2}{$|= P_{k+1} => (M \equiv N /\ P'_{k})$}
      \begin{proof}
        \pf\ \stepref{<3>1} and definition of $M$.
      \end{proof}

      \step{<3>3}{$|= P_{k+1} => \ENABLED<<M>>_{v}$}
      \begin{proof}
        \pf\ \stepref{<3>2} and the definition of $P_{k+1}$.
      \end{proof}

      \qedstep
      \begin{proof}
        \pf\ \stepref{<3>3} and 
        assumption~\ref{ass:relative-completeness}.
      \end{proof}
    \end{proof}

    \qedstep
    \begin{proof}
      \pf\ \stepref{<2>1}--\stepref{<2>3} and rule WF1 
      of~\cite{lamport:newtla}.
    \end{proof}
  \end{proof}

  \step{<1>3}{$|- [](\exists n : P_{n}) /\ <>[][M]_{v} /\ \WF_{v}(M) =>
                   []<>P$}
  \begin{proof}
    \step{<2>1}{$|- [](\exists n : P_{n}) /\ <>[][M]_{v} /\ \WF_{v}(M) =>
                  ((\exists n : P_{n}) ~> P)$}
    \begin{proof}
      \pf\ \stepref{<1>2} and the Lattice Rule of~\cite{lamport:newtla}.
    \end{proof}

    \step{<2>2}{$|- []F /\ (F ~> G) => []<>G$, for any temporal formulas 
     $F$ and $G$.}
    \begin{proof}
      \pf\ \( \begin{noj2}
                []F /\ (F ~> G) &
                     \begin{noj3}
                       \equiv & []F /\ [](F => <> G) &
                         \s{1}\tlacomment{Definition of $~>$}\\
                       \equiv & [](F /\ (F => <> G)) &
                         \s{1}\comment{Rule STL5 of \cite{lamport:newtla}.}\\
                       => & []<>G &
                         \s{1}\comment{Rule STL4 of \cite{lamport:newtla}.}
                     \end{noj3}
              \end{noj2}
           \)
    \end{proof}

    \qedstep
    \begin{proof}
      \pf\ \stepref{<2>1} and \stepref{<2>2}.
    \end{proof}
  \end{proof}

  \qedstep
  \begin{proof}
    \step{<2>0}{$|- \closure{Init /\ [][N]_{v} /\ <>[][M]_{v} /\ \WF_{v}(M)}
                \equiv Init /\ [][N]_{v}$}
    \begin{proof}
      \pf\ Proposition~\ref{prop:computing-closure}, since $|- M => N$
       by definition of $M$.
    \end{proof}

    \step{<2>1}{$|- Init /\ [][N]_{v} /\ <>[][M]_{v} /\ \WF_{v}(M)
                 => \closure{\Pi} /\ []<>P$}
    \begin{proof}
      \pf\ \stepref{<1>1}, \stepref{<1>3}, and 
      assumption~\ref{ass:closure}.
    \end{proof}
    \step{<2>3}{$|- \closure{\Pi} => \closure{\closure{\Pi}/\ []<>P}$}
    \begin{proof}
      \pf\ \stepref{<2>0}, \stepref{<2>1}, assumption~\ref{ass:closure},
     and part \ref{item:monotonic} of Proposition~\ref{prop:closure}.
    \end{proof}    

    \qedstep
    \begin{proof}
      \pf\ \stepref{<2>3} and Proposition~\ref{prop:closure-implies-possible}.
    \end{proof}

  \end{proof}
\end{proof}



\end{document}
