(sparseint-unrev-blocks nbits blocksz x) → res
Function:
(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:
(defthm sparseint-p-of-sparseint-unrev-blocks (b* ((res (sparseint-unrev-blocks nbits blocksz x))) (sparseint-p res)) :rule-classes :rewrite)
Theorem:
(defthm sparseint-unrev-blocks-val (b* ((?res (sparseint-unrev-blocks nbits blocksz x))) (natp (sparseint-val res))) :rule-classes :type-prescription)