		Search-engine friendly clone of the ACL2 documentation.

Fraig

S32v-get-bit

Signature
(s32v-get-bit row bitnum s32v) → bit
Arguments: row — Guard (natp row).; bitnum — Guard (natp bitnum).
Returns: bit — Type (bitp bit).

Definitions and Theorems

Function: s32v-get-bit

(defun s32v-get-bit (row bitnum s32v)
  (declare (xargs :stobjs (s32v)))
  (declare (xargs :guard (and (natp row) (natp bitnum))))
  (declare (xargs :guard (and (< row (s32v-nrows s32v))
                              (< bitnum (* 32 (s32v-ncols s32v))))))
  (let ((__function__ 's32v-get-bit))
    (declare (ignorable __function__))
    (b* ((col (ash (lnfix bitnum) -5))
         (bitcol (logand (lnfix bitnum) 31))
         (s32-val (s32v-get2 row col s32v)))
      (logbit bitcol s32-val))))

Theorem: bitp-of-s32v-get-bit

(defthm bitp-of-s32v-get-bit
  (b* ((bit (s32v-get-bit row bitnum s32v)))
    (bitp bit))
  :rule-classes :type-prescription)

Theorem: s32v-get-bit-of-nfix-row

(defthm s32v-get-bit-of-nfix-row
  (equal (s32v-get-bit (nfix row) bitnum s32v)
         (s32v-get-bit row bitnum s32v)))

Theorem: s32v-get-bit-nat-equiv-congruence-on-row

(defthm s32v-get-bit-nat-equiv-congruence-on-row
  (implies (nat-equiv row row-equiv)
           (equal (s32v-get-bit row bitnum s32v)
                  (s32v-get-bit row-equiv bitnum s32v)))
  :rule-classes :congruence)

Theorem: s32v-get-bit-of-nfix-bitnum

(defthm s32v-get-bit-of-nfix-bitnum
  (equal (s32v-get-bit row (nfix bitnum) s32v)
         (s32v-get-bit row bitnum s32v)))

Theorem: s32v-get-bit-nat-equiv-congruence-on-bitnum

(defthm s32v-get-bit-nat-equiv-congruence-on-bitnum
  (implies (nat-equiv bitnum bitnum-equiv)
           (equal (s32v-get-bit row bitnum s32v)
                  (s32v-get-bit row bitnum-equiv s32v)))
  :rule-classes :congruence)