WHOLEBIZ.README.TXT              Revised 2003 May 24

Note: An extra extension .TXT has been added to the WHOLEBIZ.M file to 
make it easier to read with a web browser.  It is safe to remove this
extra extension if you save the file.  The same goes for the *.M files
in the various subdirectories.

The file WHOLEBIZ.M is used to load some of the test suites, using the
paths currently set up on a Gateway 700XL machine. This test suite
runs in about 20 minutes on that machine. These files loaded are here 
gathered into the first two of the following directories:

(1) TESTS - most of the test suites loaded by WHOLEBIZ

(2) QUAIFE - those test suites that test modified versions of Quaife's
theorems. Note: Since the GOEDEL program does not assume Quaife's
modification of Kuratowski's ordered pair is being used, the test suites
will not verify theorems that depend explicitly on this construction.
The GOEDEL program also does not assume that either the axioms of choice
or regularity are valid, so it does not test those theorems of Quaife's
RE group that depend on AxReg.  The theorems in Quaife's AP group are
here replaced with versions that use A(image(x,singleton(y))) instead
of Quaife's U(image(x,singleton(y))).  This seems to work better for
the GOEDEL program.  (In our Otter work, we continue to use Quaife's
definition for apply.)

(3) LOGS - output of the WHOLEBIZ file for a recent version of the
GOEDEL program.

(4) USABLE - a new test suite based on the theorems that Belinfante 
proved using Otter, as of October 2000.  The run time for this test 
suite is too long to be used on a routine basis, and therefore is not 
part of the standard WHOLEBIZ collection. 

(5) MMA - the standard INIT.M and END.M files used to log Mathematica
sessions.