		Search-engine friendly clone of the ACL2 documentation.

Parametrize

Bitarr-range-count

Signature
(bitarr-range-count start count bitarr) → bitcount
Arguments: start — Guard (natp start).; count — Guard (natp count).
Returns: bitcount — Type (natp bitcount).

Definitions and Theorems

Function: bitarr-range-count

(defun bitarr-range-count (start count bitarr)
  (declare (xargs :stobjs (bitarr)))
  (declare (xargs :guard (and (natp start) (natp count))))
  (declare (xargs :guard (<= (+ start count)
                             (bits-length bitarr))))
  (let ((__function__ 'bitarr-range-count))
    (declare (ignorable __function__))
    (if (zp count)
        0
      (+ (get-bit start bitarr)
         (bitarr-range-count (1+ (lnfix start))
                             (1- count)
                             bitarr)))))

Theorem: natp-of-bitarr-range-count

(defthm natp-of-bitarr-range-count
  (b* ((bitcount (bitarr-range-count start count bitarr)))
    (natp bitcount))
  :rule-classes :type-prescription)

Theorem: bitarr-range-count-of-update

(defthm bitarr-range-count-of-update
  (equal (bitarr-range-count start count (update-nth n b bitarr))
         (+ (bitarr-range-count start count bitarr)
            (cond ((< (nfix n) (nfix start)) 0)
                  ((<= (+ (nfix start) (nfix count))
                       (nfix n))
                   0)
                  (t (- (bfix b) (bfix (nth n bitarr))))))))

Theorem: bitarr-range-count-upper-bound

(defthm bitarr-range-count-upper-bound
  (b* ((?bitcount (bitarr-range-count start count bitarr)))
    (<= bitcount (nfix count)))
  :rule-classes :linear)

Theorem: bitarr-range-count-not-equal-when-nonzer

(defthm bitarr-range-count-not-equal-when-nonzer
  (b* nil
    (implies (and (not (equal 1 (nth n mark)))
                  (<= (nfix start) (nfix n))
                  (< (nfix n)
                     (+ (nfix start) (nfix count))))
             (not (equal count
                         (bitarr-range-count start count mark))))))

Theorem: bitarr-range-count-less-when-nonzer

(defthm bitarr-range-count-less-when-nonzer
  (b* nil
    (implies (and (not (equal 1 (nth n mark)))
                  (<= (nfix start) (nfix n))
                  (< (nfix n)
                     (+ (nfix start) (nfix count))))
             (< (bitarr-range-count start count mark)
                (nfix count))))
  :rule-classes :linear)

Theorem: bitarr-range-count-of-resize-nil

(defthm bitarr-range-count-of-resize-nil
  (b* nil
    (equal (bitarr-range-count start count (resize-list nil k 0))
           0)))

Theorem: bitarr-range-count-of-nfix-start

(defthm bitarr-range-count-of-nfix-start
  (equal (bitarr-range-count (nfix start)
                             count bitarr)
         (bitarr-range-count start count bitarr)))

Theorem: bitarr-range-count-nat-equiv-congruence-on-start

(defthm bitarr-range-count-nat-equiv-congruence-on-start
  (implies (nat-equiv start start-equiv)
           (equal (bitarr-range-count start count bitarr)
                  (bitarr-range-count start-equiv count bitarr)))
  :rule-classes :congruence)

Theorem: bitarr-range-count-of-nfix-count

(defthm bitarr-range-count-of-nfix-count
  (equal (bitarr-range-count start (nfix count)
                             bitarr)
         (bitarr-range-count start count bitarr)))

Theorem: bitarr-range-count-nat-equiv-congruence-on-count

(defthm bitarr-range-count-nat-equiv-congruence-on-count
  (implies (nat-equiv count count-equiv)
           (equal (bitarr-range-count start count bitarr)
                  (bitarr-range-count start count-equiv bitarr)))
  :rule-classes :congruence)