Substitute into a vl-always-p.
(vl-always-subst x sigma) → new-x
Function:
(defun vl-always-subst (x sigma) (declare (xargs :guard (and (vl-always-p x) (vl-sigma-p sigma)))) (declare (ignorable x sigma)) (let ((__function__ 'vl-always-subst)) (declare (ignorable __function__)) (change-vl-always x :stmt (vl-stmt-subst (vl-always->stmt x) sigma))))
Theorem:
(defthm vl-always-p-of-vl-always-subst (b* ((new-x (vl-always-subst x sigma))) (vl-always-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm vl-always-subst-of-vl-always-fix-x (equal (vl-always-subst (vl-always-fix x) sigma) (vl-always-subst x sigma)))
Theorem:
(defthm vl-always-subst-vl-always-equiv-congruence-on-x (implies (vl-always-equiv x x-equiv) (equal (vl-always-subst x sigma) (vl-always-subst x-equiv sigma))) :rule-classes :congruence)
Theorem:
(defthm vl-always-subst-of-vl-sigma-fix-sigma (equal (vl-always-subst x (vl-sigma-fix sigma)) (vl-always-subst x sigma)))
Theorem:
(defthm vl-always-subst-vl-sigma-equiv-congruence-on-sigma (implies (vl-sigma-equiv sigma sigma-equiv) (equal (vl-always-subst x sigma) (vl-always-subst x sigma-equiv))) :rule-classes :congruence)