Function:
(defun s32v-repeat-bitcols (num-valid-input-bits row s32v) (declare (xargs :stobjs (s32v))) (declare (xargs :guard (and (posp num-valid-input-bits) (natp row)))) (declare (xargs :guard (and (<= num-valid-input-bits (* 32 (s32v-ncols s32v))) (<= row (s32v-nrows s32v))))) (let ((__function__ 's32v-repeat-bitcols)) (declare (ignorable __function__)) (b* (((when (mbe :logic (zp (- (s32v-nrows s32v) (nfix row))) :exec (eql row (s32v-nrows s32v)))) s32v) (s32v (s32v-row-repeat-bitcols 0 0 num-valid-input-bits row s32v))) (s32v-repeat-bitcols num-valid-input-bits (+ 1 (lnfix row)) s32v))))
Theorem:
(defthm s32v-nrows-of-s32v-repeat-bitcols (b* ((?new-s32v (s32v-repeat-bitcols num-valid-input-bits row s32v))) (equal (len (stobjs::2darr->rows new-s32v)) (len (stobjs::2darr->rows s32v)))))
Theorem:
(defthm s32v-ncols-of-s32v-repeat-bitcols (b* ((?new-s32v (s32v-repeat-bitcols num-valid-input-bits row s32v))) (equal (stobjs::2darr->ncols new-s32v) (stobjs::2darr->ncols s32v))))
Theorem:
(defthm s32v-repeat-bitcols-of-pos-fix-num-valid-input-bits (equal (s32v-repeat-bitcols (pos-fix num-valid-input-bits) row s32v) (s32v-repeat-bitcols num-valid-input-bits row s32v)))
Theorem:
(defthm s32v-repeat-bitcols-pos-equiv-congruence-on-num-valid-input-bits (implies (pos-equiv num-valid-input-bits num-valid-input-bits-equiv) (equal (s32v-repeat-bitcols num-valid-input-bits row s32v) (s32v-repeat-bitcols num-valid-input-bits-equiv row s32v))) :rule-classes :congruence)
Theorem:
(defthm s32v-repeat-bitcols-of-nfix-row (equal (s32v-repeat-bitcols num-valid-input-bits (nfix row) s32v) (s32v-repeat-bitcols num-valid-input-bits row s32v)))
Theorem:
(defthm s32v-repeat-bitcols-nat-equiv-congruence-on-row (implies (nat-equiv row row-equiv) (equal (s32v-repeat-bitcols num-valid-input-bits row s32v) (s32v-repeat-bitcols num-valid-input-bits row-equiv s32v))) :rule-classes :congruence)