Tonelli-Shanks modular square root. Finds a square root if a square root exists.
Function:
(defun tonelli-shanks-either-sqrt (n p z) (declare (xargs :guard (and (natp n) (natp p) (natp z)))) (declare (xargs :guard (and (> p 2) (< z p) (primep p) (< n p) (not (has-square-root? z p))))) (let ((acl2::__function__ 'tonelli-shanks-either-sqrt)) (declare (ignorable acl2::__function__)) (tonelli-shanks-sqrt-aux n p z)))
Theorem:
(defthm natp-of-tonelli-shanks-either-sqrt (implies (and (natp n) (natp p) (natp z) (< '2 p) (< z p) (primep p) (< n p) (not (has-square-root? z p))) (b* ((sqrt (tonelli-shanks-either-sqrt n p z))) (natp sqrt))) :rule-classes :rewrite)