		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)