		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Aabf-integer-length-bound-s

Signature
(aabf-integer-length-bound-s x man) → bound
Arguments: x — Guard (true-listp x).
Returns: bound — Type (posp bound).

Definitions and Theorems

Function: aabf-integer-length-bound-s

(defun aabf-integer-length-bound-s (x man)
  (declare (xargs :guard (true-listp x)))
  (declare (xargs :guard (and (aabflist-p x man))))
  (let ((__function__ 'aabf-integer-length-bound-s))
    (declare (ignorable __function__))
    (max (len x) 1)))

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

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

Theorem: trivial-theorem-about-aabf-integer-length-bound-s

(defthm trivial-theorem-about-aabf-integer-length-bound-s
  (b* nil
    (b* ((?ignore (aabf-integer-length-bound-s x man)))
      t))
  :rule-classes nil)

Theorem: aabf-integer-length-bound-s-correct

(defthm aabf-integer-length-bound-s-correct
  (< (integer-length (bools->int (aabflist-eval x env man)))
     (aabf-integer-length-bound-s x man))
  :rule-classes :linear)