(vl-always-apply-trigger-to-updates trigger x) → new-x
Function:
(defun vl-always-apply-trigger-to-updates (trigger x) (declare (xargs :guard (and (sv::svex-p trigger) (sv::svex-alist-p x)))) (let ((__function__ 'vl-always-apply-trigger-to-updates)) (declare (ignorable __function__)) (b* (((when (atom x)) nil) ((unless (mbt (and (consp (car x)) (sv::svar-p (caar x))))) (vl-always-apply-trigger-to-updates trigger (cdr x))) ((cons var upd) (car x)) (upd (sv::svex-fix upd)) (prev-var (sv::make-svex-var :name (sv::svar-add-delay var 1))) (trigger-upd (sv::make-svex-call :fn 'sv::? :args (list trigger upd prev-var)))) (cons (cons var trigger-upd) (vl-always-apply-trigger-to-updates trigger (cdr x))))))
Theorem:
(defthm svex-alist-p-of-vl-always-apply-trigger-to-updates (b* ((new-x (vl-always-apply-trigger-to-updates trigger x))) (sv::svex-alist-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm keys-of-vl-always-apply-trigger-to-updates (b* ((?new-x (vl-always-apply-trigger-to-updates trigger x))) (iff (sv::svex-lookup v new-x) (sv::svex-lookup v x))))
Theorem:
(defthm vars-of-vl-always-apply-trigger-to-updates (b* ((?new-x (vl-always-apply-trigger-to-updates trigger x))) (implies (and (not (member v (sv::svex-alist-vars x))) (not (member v (sv::svex-vars trigger))) (not (member v (sv::svarlist-add-delay (sv::svex-alist-keys x) 1)))) (not (member v (sv::svex-alist-vars new-x))))))
Theorem:
(defthm vl-always-apply-trigger-to-updates-of-svex-alist-fix-x (equal (vl-always-apply-trigger-to-updates trigger (sv::svex-alist-fix x)) (vl-always-apply-trigger-to-updates trigger x)))
Theorem:
(defthm vl-always-apply-trigger-to-updates-svex-alist-equiv-congruence-on-x (implies (sv::svex-alist-equiv x x-equiv) (equal (vl-always-apply-trigger-to-updates trigger x) (vl-always-apply-trigger-to-updates trigger x-equiv))) :rule-classes :congruence)
Theorem:
(defthm vl-always-apply-trigger-to-updates-of-svex-fix-trigger (equal (vl-always-apply-trigger-to-updates (sv::svex-fix trigger) x) (vl-always-apply-trigger-to-updates trigger x)))
Theorem:
(defthm vl-always-apply-trigger-to-updates-svex-equiv-congruence-on-trigger (implies (sv::svex-equiv trigger trigger-equiv) (equal (vl-always-apply-trigger-to-updates trigger x) (vl-always-apply-trigger-to-updates trigger-equiv x))) :rule-classes :congruence)