(aignet-vals->in/regvals vals ctrex-eval aignet) → new-ctrex-eval
Function:
(defun aignet-vals->in/regvals (vals ctrex-eval aignet) (declare (xargs :stobjs (vals ctrex-eval aignet))) (declare (xargs :guard (and (<= (num-fanins aignet) (bits-length vals)) (<= (+ (num-ins aignet) (num-regs aignet)) (bits-length ctrex-eval))))) (let ((__function__ 'aignet-vals->in/regvals)) (declare (ignorable __function__)) (b* ((ctrex-eval (aignet-vals->invals ctrex-eval vals aignet))) (aignet-vals->regvals-after-invals 0 vals ctrex-eval aignet))))
Theorem:
(defthm len-of-aignet-vals->in/regvals (b* ((?new-ctrex-eval (aignet-vals->in/regvals vals ctrex-eval aignet))) (implies (<= (+ (num-ins aignet) (num-regs aignet)) (bits-length ctrex-eval)) (equal (len new-ctrex-eval) (len ctrex-eval)))))