Eliminate dead code in errors and pairs consisting of function information and a function environment.
(funinfo+funenv-result-dead funinfoenv?) → new-funinfoenv?
We transform the pairs and leave errors unchanged.
Function:
(defun funinfo+funenv-result-dead (funinfoenv?) (declare (xargs :guard (funinfo+funenv-resultp funinfoenv?))) (let ((__function__ 'funinfo+funenv-result-dead)) (declare (ignorable __function__)) (b* ((funinfoenv? (funinfo+funenv-result-fix funinfoenv?))) (if (reserrp funinfoenv?) funinfoenv? (funinfo+funenv-dead funinfoenv?)))))
Theorem:
(defthm funinfo+funenv-resultp-of-funinfo+funenv-result-dead (b* ((new-funinfoenv? (funinfo+funenv-result-dead funinfoenv?))) (funinfo+funenv-resultp new-funinfoenv?)) :rule-classes :rewrite)
Theorem:
(defthm funinfo+funenv-result-dead-of-funinfo+funenv-result-fix-funinfoenv? (equal (funinfo+funenv-result-dead (funinfo+funenv-result-fix funinfoenv?)) (funinfo+funenv-result-dead funinfoenv?)))
Theorem:
(defthm funinfo+funenv-result-dead-funinfo+funenv-result-equiv-congruence-on-funinfoenv? (implies (funinfo+funenv-result-equiv funinfoenv? funinfoenv?-equiv) (equal (funinfo+funenv-result-dead funinfoenv?) (funinfo+funenv-result-dead funinfoenv?-equiv))) :rule-classes :congruence)