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.