		Search-engine friendly clone of the ACL2 documentation.

Tonelli-shanks-supportive-functions

Repeated-square

Signature
(repeated-square base n p) → retval
Arguments: base — Guard (natp base).; n — Guard (natp n).; p — Guard (natp p).
Returns: retval — Type (natp retval).

Definitions and Theorems

Function: repeated-square

(defun repeated-square (base n p)
       (declare (xargs :guard (and (natp base) (natp n) (natp p))))
       (declare (xargs :guard (and (natp base)
                                   (natp n)
                                   (natp p)
                                   (< 2 p))))
       (let ((acl2::__function__ 'repeated-square))
            (declare (ignorable acl2::__function__))
            (if (or (not (natp base))
                    (not (natp n))
                    (not (natp p))
                    (< p 3))
                0
                (if (zp n)
                    base
                    (repeated-square (mod (* base base) p)
                                     (- n 1)
                                     p)))))

Theorem: natp-of-repeated-square

(defthm natp-of-repeated-square
        (b* ((retval (repeated-square base n p)))
            (natp retval))
        :rule-classes :rewrite)