		Search-engine friendly clone of the ACL2 documentation.

Dead-code-eliminator-execution

Funinfo+funenv-dead

Eliminate dead code in pairs consisting of function information and a function environment.

Signature
(funinfo+funenv-dead funinfoenv) → new-funinfoenv
Arguments: funinfoenv — Guard (funinfo+funenv-p funinfoenv).
Returns: new-funinfoenv — Type (funinfo+funenv-p new-funinfoenv).

Definitions and Theorems

Function: funinfo+funenv-dead

(defun funinfo+funenv-dead (funinfoenv)
  (declare (xargs :guard (funinfo+funenv-p funinfoenv)))
  (let ((__function__ 'funinfo+funenv-dead))
    (declare (ignorable __function__))
    (b* (((funinfo+funenv funinfoenv)
          funinfoenv))
      (make-funinfo+funenv :info (funinfo-dead funinfoenv.info)
                           :env (funenv-dead funinfoenv.env)))))

Theorem: funinfo+funenv-p-of-funinfo+funenv-dead

(defthm funinfo+funenv-p-of-funinfo+funenv-dead
  (b* ((new-funinfoenv (funinfo+funenv-dead funinfoenv)))
    (funinfo+funenv-p new-funinfoenv))
  :rule-classes :rewrite)

Theorem: funinfo+funenv->info-of-funinfo+funenv-dead

(defthm funinfo+funenv->info-of-funinfo+funenv-dead
  (equal (funinfo+funenv->info (funinfo+funenv-dead funinfoenv))
         (funinfo-dead (funinfo+funenv->info funinfoenv))))

Theorem: funinfo+funenv->env-of-funinfo+funenv-dead

(defthm funinfo+funenv->env-of-funinfo+funenv-dead
  (equal (funinfo+funenv->env (funinfo+funenv-dead funinfoenv))
         (funenv-dead (funinfo+funenv->env funinfoenv))))

Theorem: funinfo+funenv-dead-of-funinfo+funenv-fix-funinfoenv

(defthm funinfo+funenv-dead-of-funinfo+funenv-fix-funinfoenv
  (equal (funinfo+funenv-dead (funinfo+funenv-fix funinfoenv))
         (funinfo+funenv-dead funinfoenv)))

Theorem: funinfo+funenv-dead-funinfo+funenv-equiv-congruence-on-funinfoenv

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