Function:
(defun bitarr-to-s32v-col (row bitcol bitarr s32v) (declare (xargs :stobjs (bitarr s32v))) (declare (xargs :guard (and (natp row) (natp bitcol)))) (declare (xargs :guard (and (<= row (s32v-nrows s32v)) (<= (s32v-nrows s32v) (bits-length bitarr)) (< bitcol (* 32 (s32v-ncols s32v)))))) (let ((__function__ 'bitarr-to-s32v-col)) (declare (ignorable __function__)) (b* (((when (mbe :logic (zp (- (s32v-nrows s32v) (nfix row))) :exec (eql row (s32v-nrows s32v)))) s32v) (bit (get-bit row bitarr)) (s32v (s32v-install-bit row bitcol bit s32v))) (bitarr-to-s32v-col (1+ (lnfix row)) bitcol bitarr s32v))))
Theorem:
(defthm s32v-nrows-of-bitarr-to-s32v-col (b* ((?new-s32v (bitarr-to-s32v-col row bitcol bitarr s32v))) (equal (len (stobjs::2darr->rows new-s32v)) (len (stobjs::2darr->rows s32v)))))
Theorem:
(defthm s32v-ncols-of-bitarr-to-s32v-col (b* ((?new-s32v (bitarr-to-s32v-col row bitcol bitarr s32v))) (equal (stobjs::2darr->ncols new-s32v) (stobjs::2darr->ncols s32v))))
Theorem:
(defthm bitarr-to-s32v-col-of-nfix-row (equal (bitarr-to-s32v-col (nfix row) bitcol bitarr s32v) (bitarr-to-s32v-col row bitcol bitarr s32v)))
Theorem:
(defthm bitarr-to-s32v-col-nat-equiv-congruence-on-row (implies (nat-equiv row row-equiv) (equal (bitarr-to-s32v-col row bitcol bitarr s32v) (bitarr-to-s32v-col row-equiv bitcol bitarr s32v))) :rule-classes :congruence)
Theorem:
(defthm bitarr-to-s32v-col-of-nfix-bitcol (equal (bitarr-to-s32v-col row (nfix bitcol) bitarr s32v) (bitarr-to-s32v-col row bitcol bitarr s32v)))
Theorem:
(defthm bitarr-to-s32v-col-nat-equiv-congruence-on-bitcol (implies (nat-equiv bitcol bitcol-equiv) (equal (bitarr-to-s32v-col row bitcol bitarr s32v) (bitarr-to-s32v-col row bitcol-equiv bitarr s32v))) :rule-classes :congruence)