(svtv-debug-eval-aliases n aliases wirevals vcd-vals) → vcd-vals1
Function:
(defun svtv-debug-eval-aliases (n aliases wirevals vcd-vals) (declare (xargs :stobjs (aliases vcd-vals))) (declare (xargs :guard (and (natp n) (svex-env-p wirevals)))) (declare (xargs :guard (and (<= n (aliass-length aliases)) (<= (aliass-length aliases) (4vecs-length vcd-vals))))) (let ((__function__ 'svtv-debug-eval-aliases)) (declare (ignorable __function__)) (b* (((when (mbe :logic (zp (- (aliass-length aliases) (nfix n))) :exec (eql (aliass-length aliases) n))) vcd-vals) (lhs (get-alias n aliases)) (val (svtv-debug-lhs-eval lhs n wirevals vcd-vals)) (vcd-vals (set-4vec n val vcd-vals))) (svtv-debug-eval-aliases (1+ (lnfix n)) aliases wirevals vcd-vals))))
Theorem:
(defthm len-vcd-vals-of-svtv-debug-eval-aliases (<= (len vcd-vals) (len (svtv-debug-eval-aliases n aliases wirevals vcd-vals))) :rule-classes :linear)
Theorem:
(defthm svtv-debug-eval-aliases-of-nfix-n (equal (svtv-debug-eval-aliases (nfix n) aliases wirevals vcd-vals) (svtv-debug-eval-aliases n aliases wirevals vcd-vals)))
Theorem:
(defthm svtv-debug-eval-aliases-nat-equiv-congruence-on-n (implies (nat-equiv n n-equiv) (equal (svtv-debug-eval-aliases n aliases wirevals vcd-vals) (svtv-debug-eval-aliases n-equiv aliases wirevals vcd-vals))) :rule-classes :congruence)
Theorem:
(defthm svtv-debug-eval-aliases-of-lhslist-fix-aliases (equal (svtv-debug-eval-aliases n (lhslist-fix aliases) wirevals vcd-vals) (svtv-debug-eval-aliases n aliases wirevals vcd-vals)))
Theorem:
(defthm svtv-debug-eval-aliases-lhslist-equiv-congruence-on-aliases (implies (lhslist-equiv aliases aliases-equiv) (equal (svtv-debug-eval-aliases n aliases wirevals vcd-vals) (svtv-debug-eval-aliases n aliases-equiv wirevals vcd-vals))) :rule-classes :congruence)
Theorem:
(defthm svtv-debug-eval-aliases-of-svex-env-fix-wirevals (equal (svtv-debug-eval-aliases n aliases (svex-env-fix wirevals) vcd-vals) (svtv-debug-eval-aliases n aliases wirevals vcd-vals)))
Theorem:
(defthm svtv-debug-eval-aliases-svex-env-equiv-congruence-on-wirevals (implies (svex-env-equiv wirevals wirevals-equiv) (equal (svtv-debug-eval-aliases n aliases wirevals vcd-vals) (svtv-debug-eval-aliases n aliases wirevals-equiv vcd-vals))) :rule-classes :congruence)