## A Mechanical Proof of the Chinese Remainder Theorem

### David M. Russinoff

This paper
(ps, pdf), which was presented at ACL2 Workshop 2000
(see slides: ps, pdf),
describes an ACL2 proof of the Chinese Remainder Theorem:

If *m*_{1}, ..., *m*_{k} are pairwise
relatively prime moduli and *a*_{1}, ..., *a*_{k} are natural numbers, then there exists
a natural number *x* that simultaneously satisfies *x* = *a*_{i} (mod *m*_{i}), *i*=1, ..., *k*.

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.