crt.lisp, except that it depends
on some lemmas from the author's
library of floating-point arithmetic.
In order to certify this file (after obtaining and certifying the library), first replace each
of the two occurrences of "/u/druss/" with the path to the directory under which
your copy of the library resides. A second event file,
summary.lisp,
which contains the definitions and main lemmas involved in the proof, may then be certified.
You can download a gzipped tar file containing this file together with the two event files discussed above.