		Search-engine friendly clone of the ACL2 documentation.

Sparseint$

Sparseint$-count

Measure for recurring over sparseint$ structures.

Signature
(sparseint$-count x) → count
Arguments: x — Guard (sparseint$-p x).
Returns: count — Type (natp count).

Definitions and Theorems

Function: sparseint$-count

(defun sparseint$-count (x)
 (declare (xargs :guard (sparseint$-p x)))
 (let ((__function__ 'sparseint$-count))
   (declare (ignorable __function__))
   (case (sparseint$-kind x)
     (:leaf 1)
     (:concat (+ 6
                 (sparseint$-count (sparseint$-concat->lsbs x))
                 (sparseint$-count (sparseint$-concat->msbs x)))))))

Theorem: natp-of-sparseint$-count

(defthm natp-of-sparseint$-count
  (b* ((count (sparseint$-count x)))
    (natp count))
  :rule-classes :type-prescription)

Theorem: sparseint$-count-of-sparseint$-fix-x

(defthm sparseint$-count-of-sparseint$-fix-x
  (equal (sparseint$-count (sparseint$-fix x))
         (sparseint$-count x)))

Theorem: sparseint$-count-sparseint$-equiv-congruence-on-x

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

Theorem: sparseint$-count-of-sparseint$-concat

(defthm sparseint$-count-of-sparseint$-concat
 (implies
    t
    (< (+ (sparseint$-count lsbs)
          (sparseint$-count msbs))
       (sparseint$-count
            (sparseint$-concat width
                               lsbs-taller msbs-taller lsbs msbs))))
 :rule-classes :linear)

Theorem: sparseint$-count-of-sparseint$-concat->lsbs

(defthm sparseint$-count-of-sparseint$-concat->lsbs
  (implies (equal (sparseint$-kind x) :concat)
           (< (sparseint$-count (sparseint$-concat->lsbs x))
              (sparseint$-count x)))
  :rule-classes :linear)

Theorem: sparseint$-count-of-sparseint$-concat->msbs

(defthm sparseint$-count-of-sparseint$-concat->msbs
  (implies (equal (sparseint$-kind x) :concat)
           (< (sparseint$-count (sparseint$-concat->msbs x))
              (sparseint$-count x)))
  :rule-classes :linear)