These files are the supporting materials for the paper "Formally
Verifying an Algorithm Based on Interval Arithmetic for Checking
Transversality" by Marcio Gameiro and Panagiotis Manolios, ACL2-2004.

To certify using ACL2 or ACL2(r) v2.9, in the ground-zero theory type:
 
   (ld "certify.lsp")

If you are on a system that supports "make", then to certify using ACL2
you can simply type "make".