(fraig-ctrex-invals->vecsim n packed-vals packed-relevants s32v aignet) → new-s32v
Function:
(defun fraig-ctrex-invals->vecsim (n packed-vals packed-relevants s32v aignet) (declare (xargs :stobjs (packed-vals packed-relevants s32v aignet))) (declare (xargs :guard (natp n))) (declare (xargs :guard (and (<= n (num-ins aignet)) (<= (s32v-ncols s32v) (s32v-ncols packed-vals)) (<= (s32v-ncols s32v) (s32v-ncols packed-relevants)) (<= (num-ins aignet) (s32v-nrows packed-vals)) (<= (num-ins aignet) (s32v-nrows packed-relevants)) (<= (num-fanins aignet) (s32v-nrows s32v))))) (let ((__function__ 'fraig-ctrex-invals->vecsim)) (declare (ignorable __function__)) (b* (((when (mbe :logic (zp (- (num-ins aignet) (nfix n))) :exec (eql n (num-ins aignet)))) s32v) (id (innum->id n aignet)) (s32v (s32v-copy-cares 0 n id packed-vals packed-relevants s32v))) (fraig-ctrex-invals->vecsim (1+ (lnfix n)) packed-vals packed-relevants s32v aignet))))
Theorem:
(defthm nrows-of-fraig-ctrex-invals->vecsim (b* ((?new-s32v (fraig-ctrex-invals->vecsim n packed-vals packed-relevants s32v aignet))) (implies (<= (num-fanins aignet) (s32v-nrows s32v)) (equal (len (stobjs::2darr->rows new-s32v)) (len (stobjs::2darr->rows s32v))))))
Theorem:
(defthm ncols-of-fraig-ctrex-invals->vecsim (b* ((?new-s32v (fraig-ctrex-invals->vecsim n packed-vals packed-relevants s32v aignet))) (equal (stobjs::2darr->ncols new-s32v) (stobjs::2darr->ncols s32v))))
Theorem:
(defthm fraig-ctrex-invals->vecsim-of-nfix-n (equal (fraig-ctrex-invals->vecsim (nfix n) packed-vals packed-relevants s32v aignet) (fraig-ctrex-invals->vecsim n packed-vals packed-relevants s32v aignet)))
Theorem:
(defthm fraig-ctrex-invals->vecsim-nat-equiv-congruence-on-n (implies (nat-equiv n n-equiv) (equal (fraig-ctrex-invals->vecsim n packed-vals packed-relevants s32v aignet) (fraig-ctrex-invals->vecsim n-equiv packed-vals packed-relevants s32v aignet))) :rule-classes :congruence)