Number of characters in the decimal representation of a natural.
Function:
(defun nat-to-dec-string-size$inline (x) (declare (xargs :guard (natp x))) (let ((acl2::__function__ 'nat-to-dec-string-size)) (declare (ignorable acl2::__function__)) (mbe :logic (if (< (lnfix x) 10) 1 (+ 1 (nat-to-dec-string-size (truncate x 10)))) :exec (if (<= (mbe :logic (nfix x) :exec x) 536870911) (nat-to-dec-string-size-fast x) (nat-to-dec-string-size-slow x)))))
Theorem:
(defthm posp-of-nat-to-dec-string-size (b* ((size (nat-to-dec-string-size$inline x))) (posp size)) :rule-classes :type-prescription)
Theorem:
(defthm nat-to-dec-string-size-slow-removal (equal (nat-to-dec-string-size-slow x) (nat-to-dec-string-size x)))
Theorem:
(defthm nat-to-dec-string-size-fast-removal (equal (nat-to-dec-string-size-fast x) (nat-to-dec-string-size x)))