		Search-engine friendly clone of the ACL2 documentation.

S4vecs

Sparseint-rev-blocks

Signature
(sparseint-rev-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-rev-blocks

(defun sparseint-rev-blocks (nbits blocksz x)
 (declare (xargs :guard (and (natp nbits)
                             (posp blocksz)
                             (sparseint-p x))))
 (let ((__function__ 'sparseint-rev-blocks))
   (declare (ignorable __function__))
   (b*
    ((nbits (lnfix nbits))
     (blocksz (lposfix blocksz))
     ((when (< nbits blocksz))
      (sparseint-concatenate nbits x 0))
     (next-nbits (- nbits blocksz))
     (rest (sparseint-rev-blocks next-nbits blocksz
                                 (sparseint-rightshift blocksz x))))
    (sparseint-concatenate next-nbits rest
                           (sparseint-concatenate blocksz x 0)))))

Theorem: sparseint-p-of-sparseint-rev-blocks

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

Theorem: sparseint-rev-blocks-correct

(defthm sparseint-rev-blocks-correct
  (b* ((?res (sparseint-rev-blocks nbits blocksz x)))
    (equal (sparseint-val res)
           (rev-blocks nbits blocksz (sparseint-val x)))))

Theorem: sparseint-rev-blocks-of-nfix-nbits

(defthm sparseint-rev-blocks-of-nfix-nbits
  (equal (sparseint-rev-blocks (nfix nbits)
                               blocksz x)
         (sparseint-rev-blocks nbits blocksz x)))

Theorem: sparseint-rev-blocks-nat-equiv-congruence-on-nbits

(defthm sparseint-rev-blocks-nat-equiv-congruence-on-nbits
  (implies (nat-equiv nbits nbits-equiv)
           (equal (sparseint-rev-blocks nbits blocksz x)
                  (sparseint-rev-blocks nbits-equiv blocksz x)))
  :rule-classes :congruence)

Theorem: sparseint-rev-blocks-of-pos-fix-blocksz

(defthm sparseint-rev-blocks-of-pos-fix-blocksz
  (equal (sparseint-rev-blocks nbits (pos-fix blocksz)
                               x)
         (sparseint-rev-blocks nbits blocksz x)))

Theorem: sparseint-rev-blocks-pos-equiv-congruence-on-blocksz

(defthm sparseint-rev-blocks-pos-equiv-congruence-on-blocksz
  (implies (pos-equiv blocksz blocksz-equiv)
           (equal (sparseint-rev-blocks nbits blocksz x)
                  (sparseint-rev-blocks nbits blocksz-equiv x)))
  :rule-classes :congruence)

Theorem: sparseint-rev-blocks-of-sparseint-fix-x

(defthm sparseint-rev-blocks-of-sparseint-fix-x
  (equal (sparseint-rev-blocks nbits blocksz (sparseint-fix x))
         (sparseint-rev-blocks nbits blocksz x)))

Theorem: sparseint-rev-blocks-sparseint-equiv-congruence-on-x

(defthm sparseint-rev-blocks-sparseint-equiv-congruence-on-x
  (implies (sparseint-equiv x x-equiv)
           (equal (sparseint-rev-blocks nbits blocksz x)
                  (sparseint-rev-blocks nbits blocksz x-equiv)))
  :rule-classes :congruence)