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