		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Sparseint$-length-rec

Signature
(sparseint$-length-rec x) → length
Arguments: x — Guard (sparseint$-p x).
Returns: length — Type (integerp length).

Definitions and Theorems

Function: sparseint$-length-rec

(defun sparseint$-length-rec (x)
  (declare (xargs :guard (sparseint$-p x)))
  (let ((__function__ 'sparseint$-length-rec))
    (declare (ignorable __function__))
    (sparseint$-case
         x :leaf
         (cond ((eql x.val 0) 0)
               ((eql x.val -1) -1)
               (t (integer-length x.val)))
         :concat
         (b* ((tail/len (sparseint$-length-rec x.msbs))
              ((when (< 0 tail/len))
               (+ x.width tail/len)))
           (sparseint$-length-width-rec x.width tail/len x.lsbs)))))

Theorem: integerp-of-sparseint$-length-rec

(defthm integerp-of-sparseint$-length-rec
  (b* ((length (sparseint$-length-rec x)))
    (integerp length))
  :rule-classes :type-prescription)

Theorem: sparseint$-length-rec-correct

(defthm sparseint$-length-rec-correct
  (b* ((common-lisp::?length (sparseint$-length-rec x)))
    (and (implies (< 0 length)
                  (equal length
                         (integer-length (sparseint$-val x))))
         (implies (<= length 0)
                  (equal length (sparseint$-val x)))
         (<= -1 length))))

Theorem: sparseint$-length-rec-of-sparseint$-fix-x

(defthm sparseint$-length-rec-of-sparseint$-fix-x
  (equal (sparseint$-length-rec (sparseint$-fix x))
         (sparseint$-length-rec x)))

Theorem: sparseint$-length-rec-sparseint$-equiv-congruence-on-x

(defthm sparseint$-length-rec-sparseint$-equiv-congruence-on-x
  (implies (sparseint$-equiv x x-equiv)
           (equal (sparseint$-length-rec x)
                  (sparseint$-length-rec x-equiv)))
  :rule-classes :congruence)