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