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