		Search-engine friendly clone of the ACL2 documentation.

Svex-argmasks

Sparseint-unrev-blocks

Signature
(sparseint-unrev-blocks nbits blocksz x) → res
Arguments: nbits — Guard (natp nbits).; blocksz — Guard (posp blocksz).; x — Guard (sparseint-p x).
Returns: res — Type (sparseint-p res).

Definitions and Theorems

Function: sparseint-unrev-blocks

(defun sparseint-unrev-blocks (nbits blocksz x)
  (declare (xargs :guard (and (natp nbits)
                              (posp blocksz)
                              (sparseint-p x))))
  (let ((__function__ 'sparseint-unrev-blocks))
    (declare (ignorable __function__))
    (b* ((nbits (lnfix nbits))
         (blocksz (mbe :logic (pos-fix blocksz)
                       :exec blocksz))
         ((when (< nbits blocksz))
          (sparseint-concatenate nbits x 0))
         (next-nbits (- nbits blocksz))
         (rest (sparseint-unrev-blocks next-nbits blocksz x)))
      (sparseint-concatenate blocksz
                             (sparseint-rightshift next-nbits x)
                             rest))))

Theorem: sparseint-p-of-sparseint-unrev-blocks

(defthm sparseint-p-of-sparseint-unrev-blocks
  (b* ((res (sparseint-unrev-blocks nbits blocksz x)))
    (sparseint-p res))
  :rule-classes :rewrite)

Theorem: sparseint-unrev-blocks-val

(defthm sparseint-unrev-blocks-val
  (b* ((?res (sparseint-unrev-blocks nbits blocksz x)))
    (natp (sparseint-val res)))
  :rule-classes :type-prescription)