This directory contains PVS files associated with the example
arbiter described in section 7.2.  The dump file for the entire
example is arbiter.dump.

Notes
-----

The proof shown on pages 203-204, section 7.2 of the book is:

 (THEN 
 (SKOSIMP*)
 (CASE* "i!1 = 0" "i!1 = 1" "i!1 = 2" "i!1 = 3")
 (ASSERT) (REPLACE*)
 (MODEL-CHECK))


However, the proof in this directory is:

 (APPLY (THEN 
 (SKOSIMP*)
 (CASE* "i!1 = 0" "i!1 = 1" "i!1 = 2" "i!1 = 3")
 (ASSERT) (REPLACE*)
 (MODEL-CHECK)))

The outermost APPLY is used merely to have the effect of applying the
entire proof as an atomic proof command.
