MOD-EXPT

exponential function
Major Section:  ACL2-BUILT-INS

(mod-expt r i m) is the result of raising the number r to the integer power 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 and i is an integer; if r is 0 then 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 r and i are natural numbers, not both zero, and m is a positive integer. For other Lisp implementations, consider using function mod-expt-fast, defined in the 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.