		Search-engine friendly clone of the ACL2 documentation.

Dead-code-eliminator-execution

Funenv-result-dead

Eliminate dead code in errors and function environments.

Signature
(funenv-result-dead funenv?) → new-funenv?
Arguments: funenv? — Guard (funenv-resultp funenv?).
Returns: new-funenv? — Type (funenv-resultp new-funenv?).

We transform function environments and leave errors unchanged.

Definitions and Theorems

Function: funenv-result-dead

(defun funenv-result-dead (funenv?)
  (declare (xargs :guard (funenv-resultp funenv?)))
  (let ((__function__ 'funenv-result-dead))
    (declare (ignorable __function__))
    (b* ((funenv? (funenv-result-fix funenv?)))
      (if (reserrp funenv?)
          funenv?
        (funenv-dead funenv?)))))

Theorem: funenv-resultp-of-funenv-result-dead

(defthm funenv-resultp-of-funenv-result-dead
  (b* ((new-funenv? (funenv-result-dead funenv?)))
    (funenv-resultp new-funenv?))
  :rule-classes :rewrite)

Theorem: funenv-result-dead-of-funenv-result-fix-funenv?

(defthm funenv-result-dead-of-funenv-result-fix-funenv?
  (equal (funenv-result-dead (funenv-result-fix funenv?))
         (funenv-result-dead funenv?)))

Theorem: funenv-result-dead-funenv-result-equiv-congruence-on-funenv?

(defthm funenv-result-dead-funenv-result-equiv-congruence-on-funenv?
  (implies (funenv-result-equiv funenv? funenv?-equiv)
           (equal (funenv-result-dead funenv?)
                  (funenv-result-dead funenv?-equiv)))
  :rule-classes :congruence)