(nat-to-dec-string-size-slow x) → *
Function:
(defun nat-to-dec-string-size-slow (x) (declare (xargs :guard (natp x))) (let ((acl2::__function__ 'nat-to-dec-string-size-slow)) (declare (ignorable acl2::__function__)) (if (< (lnfix x) 10) 1 (the unsigned-byte (+ 1 (the unsigned-byte (nat-to-dec-string-size-slow (the unsigned-byte (truncate x 10)))))))))