		Search-engine friendly clone of the ACL2 documentation.

4vec-rev-blocks

Rev-block-index

For reasoning about rev-blocks, computes the offset into x corresponding to an offset into (rev-blocks nbits blocksz x).

Signature
(rev-block-index i nbits blocksz) → idx
Arguments: i — Guard (natp i).; nbits — Guard (natp nbits).; blocksz — Guard (posp blocksz).
Returns: idx — Type (natp idx).

(equal (logbitp i (rev-blocks nbits blocksz x))
       (logbitp (rev-block-index i nbits blogksz) x))

if i is in bounds.

Definitions and Theorems

Function: rev-block-index

(defun rev-block-index (i nbits blocksz)
  (declare (xargs :guard (and (natp i)
                              (natp nbits)
                              (posp blocksz))))
  (let ((__function__ 'rev-block-index))
    (declare (ignorable __function__))
    (b* ((nbits (lnfix nbits))
         (blocksz (mbe :logic (pos-fix blocksz)
                       :exec blocksz))
         (i (lnfix i))
         ((when (< nbits blocksz)) i)
         (next-nbits (- nbits blocksz))
         ((when (<= next-nbits i))
          (- i next-nbits)))
      (+ blocksz
         (rev-block-index i next-nbits blocksz)))))

Theorem: natp-of-rev-block-index

(defthm natp-of-rev-block-index
  (b* ((idx (rev-block-index i nbits blocksz)))
    (natp idx))
  :rule-classes :type-prescription)

Theorem: logbitp-of-rev-blocks

(defthm logbitp-of-rev-blocks
  (equal (logbitp i (rev-blocks nbits blocksz x))
         (and (< (nfix i) (nfix nbits))
              (logbitp (rev-block-index i nbits blocksz)
                       x))))