		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Integer-length-bound-s

Signature
(integer-length-bound-s x) → bound
Returns: bound — Type (posp bound).

Definitions and Theorems

Function: integer-length-bound-s

(defun integer-length-bound-s (x)
  (declare (xargs :guard t))
  (let ((__function__ 'integer-length-bound-s))
    (declare (ignorable __function__))
    (max (len x) 1)))

Theorem: posp-of-integer-length-bound-s

(defthm posp-of-integer-length-bound-s
  (b* ((bound (integer-length-bound-s x)))
    (posp bound))
  :rule-classes :type-prescription)

Theorem: integer-length-bound-s-correct

(defthm integer-length-bound-s-correct
  (< (integer-length (bfr-list->s x env))
     (integer-length-bound-s x))
  :rule-classes :linear)