		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Sparseint$-bit

Signature
(sparseint$-bit n x) → bit
Arguments: n — Guard (natp n).; x — Guard (sparseint$-p x).
Returns: bit — Type (bitp bit).

Definitions and Theorems

Function: sparseint$-bit

(defun sparseint$-bit (n x)
  (declare (xargs :guard (and (natp n) (sparseint$-p x))))
  (let ((__function__ 'sparseint$-bit))
    (declare (ignorable __function__))
    (sparseint$-case x :leaf (logbit n x.val)
                     :concat
                     (b* ((n (lnfix n))
                          ((when (< n x.width))
                           (sparseint$-bit n x.lsbs)))
                       (sparseint$-bit (- n x.width)
                                       x.msbs)))))

Theorem: bitp-of-sparseint$-bit

(defthm bitp-of-sparseint$-bit
  (b* ((bit (sparseint$-bit n x)))
    (bitp bit))
  :rule-classes :type-prescription)

Theorem: sparseint$-bit-correct

(defthm sparseint$-bit-correct
  (b* nil
    (equal (sparseint$-bit n x)
           (logbit n (sparseint$-val x)))))

Theorem: sparseint$-bit-of-nfix-n

(defthm sparseint$-bit-of-nfix-n
  (equal (sparseint$-bit (nfix n) x)
         (sparseint$-bit n x)))

Theorem: sparseint$-bit-nat-equiv-congruence-on-n

(defthm sparseint$-bit-nat-equiv-congruence-on-n
  (implies (nat-equiv n n-equiv)
           (equal (sparseint$-bit n x)
                  (sparseint$-bit n-equiv x)))
  :rule-classes :congruence)

Theorem: sparseint$-bit-of-sparseint$-fix-x

(defthm sparseint$-bit-of-sparseint$-fix-x
  (equal (sparseint$-bit n (sparseint$-fix x))
         (sparseint$-bit n x)))

Theorem: sparseint$-bit-sparseint$-equiv-congruence-on-x

(defthm sparseint$-bit-sparseint$-equiv-congruence-on-x
  (implies (sparseint$-equiv x x-equiv)
           (equal (sparseint$-bit n x)
                  (sparseint$-bit n x-equiv)))
  :rule-classes :congruence)