Function:
(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:
(defthm natp-of-repeated-square (b* ((retval (repeated-square base n p))) (natp retval)) :rule-classes :rewrite)