Function:
(defun s32v-bitcol-count-set (n acc bitcol s32v) (declare (xargs :stobjs (s32v))) (declare (xargs :guard (and (natp n) (natp acc) (natp bitcol)))) (declare (xargs :guard (and (<= n (s32v-nrows s32v)) (< bitcol (* 32 (s32v-ncols s32v)))))) (let ((__function__ 's32v-bitcol-count-set)) (declare (ignorable __function__)) (b* (((when (mbe :logic (zp (- (s32v-nrows s32v) (nfix n))) :exec (eql n (s32v-nrows s32v)))) (lnfix acc))) (s32v-bitcol-count-set (1+ (lnfix n)) (+ (lnfix acc) (s32v-get-bit n bitcol s32v)) bitcol s32v))))
Theorem:
(defthm s32v-bitcol-acc-elim (implies (syntaxp (not (equal acc ''0))) (equal (s32v-bitcol-count-set n acc bitcol s32v) (+ (nfix acc) (s32v-bitcol-count-set n 0 bitcol s32v)))))
Theorem:
(defthm s32v-bitcol-count-set-of-nfix-n (equal (s32v-bitcol-count-set (nfix n) acc bitcol s32v) (s32v-bitcol-count-set n acc bitcol s32v)))
Theorem:
(defthm s32v-bitcol-count-set-nat-equiv-congruence-on-n (implies (nat-equiv n n-equiv) (equal (s32v-bitcol-count-set n acc bitcol s32v) (s32v-bitcol-count-set n-equiv acc bitcol s32v))) :rule-classes :congruence)
Theorem:
(defthm s32v-bitcol-count-set-of-nfix-acc (equal (s32v-bitcol-count-set n (nfix acc) bitcol s32v) (s32v-bitcol-count-set n acc bitcol s32v)))
Theorem:
(defthm s32v-bitcol-count-set-nat-equiv-congruence-on-acc (implies (nat-equiv acc acc-equiv) (equal (s32v-bitcol-count-set n acc bitcol s32v) (s32v-bitcol-count-set n acc-equiv bitcol s32v))) :rule-classes :congruence)
Theorem:
(defthm s32v-bitcol-count-set-of-nfix-bitcol (equal (s32v-bitcol-count-set n acc (nfix bitcol) s32v) (s32v-bitcol-count-set n acc bitcol s32v)))
Theorem:
(defthm s32v-bitcol-count-set-nat-equiv-congruence-on-bitcol (implies (nat-equiv bitcol bitcol-equiv) (equal (s32v-bitcol-count-set n acc bitcol s32v) (s32v-bitcol-count-set n acc bitcol-equiv s32v))) :rule-classes :congruence)