Function:
(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:
(defthm natp-of-q*2^s.q (b* (((mv ?q ?s) (q*2^s n))) (natp q)) :rule-classes :rewrite)
Theorem:
(defthm natp-of-q*2^s.s (b* (((mv ?q ?s) (q*2^s n))) (natp s)) :rule-classes :rewrite)