This directory contains an ACL2 proof of the Chinese Remainder Theorem, as described in a paper presented at ACL2 Workshop 2000. The entire proof is contained in the single event file 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.