(aignet-vals->regvals-after-invals n vals regvals aignet) → new-regvals
Function:
(defun aignet-vals->regvals-after-invals (n vals regvals aignet) (declare (xargs :stobjs (vals regvals aignet))) (declare (xargs :guard (natp n))) (declare (xargs :guard (and (<= (num-fanins aignet) (bits-length vals)) (<= (+ (num-ins aignet) (num-regs aignet)) (bits-length regvals)) (<= n (num-regs aignet))))) (let ((__function__ 'aignet-vals->regvals-after-invals)) (declare (ignorable __function__)) (b* (((when (mbe :logic (zp (- (num-regs aignet) (nfix n))) :exec (eql n (num-regs aignet)))) regvals) (id (regnum->id n aignet)) (val (get-bit id vals)) (regvals (set-bit (+ (lnfix n) (num-ins aignet)) val regvals))) (aignet-vals->regvals-after-invals (1+ (lnfix n)) vals regvals aignet))))
Theorem:
(defthm length-of-aignet-vals->regvals-after-invals (b* ((?new-regvals (aignet-vals->regvals-after-invals n vals regvals aignet))) (implies (<= (+ (num-ins aignet) (num-regs aignet)) (len regvals)) (equal (len new-regvals) (len regvals)))))
Theorem:
(defthm aignet-vals->regvals-after-invals-of-nfix-n (equal (aignet-vals->regvals-after-invals (nfix n) vals regvals aignet) (aignet-vals->regvals-after-invals n vals regvals aignet)))
Theorem:
(defthm aignet-vals->regvals-after-invals-nat-equiv-congruence-on-n (implies (nat-equiv n n-equiv) (equal (aignet-vals->regvals-after-invals n vals regvals aignet) (aignet-vals->regvals-after-invals n-equiv vals regvals aignet))) :rule-classes :congruence)