		Search-engine friendly clone of the ACL2 documentation.

Dead-code-eliminator-execution

Funenv-dead

Eliminate dead code in function environments.

Signature
(funenv-dead funenv) → new-funenv
Arguments: funenv — Guard (funenvp funenv).
Returns: new-funenv — Type (funenvp new-funenv).

We transform all the function scopes in the list.

Definitions and Theorems

Function: funenv-dead

(defun funenv-dead (funenv)
  (declare (xargs :guard (funenvp funenv)))
  (let ((__function__ 'funenv-dead))
    (declare (ignorable __function__))
    (cond ((endp funenv) nil)
          (t (cons (funscope-dead (car funenv))
                   (funenv-dead (cdr funenv)))))))

Theorem: funenvp-of-funenv-dead

(defthm funenvp-of-funenv-dead
  (b* ((new-funenv (funenv-dead funenv)))
    (funenvp new-funenv))
  :rule-classes :rewrite)

Theorem: funenv-dead-of-cons

(defthm funenv-dead-of-cons
  (equal (funenv-dead (cons funscope funscopes))
         (cons (funscope-dead funscope)
               (funenv-dead funscopes))))

Theorem: funenv-dead-of-funenv-fix-funenv

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

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

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