Major Section: ACL2-BUILT-INS
(mod-expt r i m) is the result of raising the number
r to the
i and then taking the residue mod
m. That is,
(mod-expt r i m) is equal to
(mod (expt r i) m).
The guard for
(mod-expt r i m) is that
r is a rational number
i is an integer; if
i is nonnegative; and
m is a non-zero rational number.
In some implementations (GCL Version 2.7.0 as of this writing), this function
is highly optimized when
i are natural numbers, not both zero,
m is a positive integer. For other Lisp implementations, consider
mod-expt-fast, defined in the community book
arithmetic-3/floor-mod/mod-expt-fast.lisp, which should still provide
significantly improved performance over this function.
To see the ACL2 definition of this function, see pf.