Function:
(defun nat-to-hex-string-size-aux (n) (declare (xargs :guard (natp n))) (let ((acl2::__function__ 'nat-to-hex-string-size-aux)) (declare (ignorable acl2::__function__)) (if (zp n) 0 (+ 1 (nat-to-hex-string-size-aux (ash n -4))))))
Theorem:
(defthm natp-of-nat-to-hex-string-size-aux (b* ((size (nat-to-hex-string-size-aux n))) (natp size)) :rule-classes :type-prescription)
Theorem:
(defthm nat-to-hex-string-size-aux-redef (equal (nat-to-hex-string-size-aux n) (len (basic-nat-to-hex-chars n))))