		Search-engine friendly clone of the ACL2 documentation.

Tonelli-shanks-supportive-functions

Q*2^s

Signature
(q*2^s n) → (mv q s)
Arguments: n — Guard (natp n).
Returns: q — Type (natp q).; s — Type (natp s).

Definitions and Theorems

Function: q*2^s

(defun q*2^s (n)
       (declare (xargs :guard (natp n)))
       (let ((acl2::__function__ 'q*2^s))
            (declare (ignorable acl2::__function__))
            (if (or (not (natp n)) (= n 0))
                (mv 0 0)
                (if (oddp n)
                    (mv n 0)
                    (mv-let (inner-q inner-s)
                            (q*2^s (/ n 2))
                            (mv inner-q (+ inner-s 1)))))))

Theorem: natp-of-q*2^s.q

(defthm natp-of-q*2^s.q
        (b* (((mv ?q ?s) (q*2^s n))) (natp q))
        :rule-classes :rewrite)

Theorem: natp-of-q*2^s.s

(defthm natp-of-q*2^s.s
        (b* (((mv ?q ?s) (q*2^s n))) (natp s))
        :rule-classes :rewrite)