Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-10-21 16:14:09 -0700 (Fri, 21 Oct 2005)
Revision: 7962
Log message:

      Adding reduceT to the end of autoCompleteT. This results in a noticeable
      reduction of ruleboxes (as much as 3 instead of 10 in some of the CZF proofs)
      at a cost of about 10% increase of the "status_all" running time.