		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Update-elab-mod$a->orig-mod

Signature
(update-elab-mod$a->orig-mod m elab-mod$a) → elab-mod$a2
Arguments: m — Guard (module-p m).; elab-mod$a — Guard (elab-mod$ap elab-mod$a).
Returns: elab-mod$a2 — Type (elab-mod$ap elab-mod$a2).

Definitions and Theorems

Function: update-elab-mod$a->orig-mod

(defun update-elab-mod$a->orig-mod (m elab-mod$a)
  (declare (xargs :guard (and (module-p m)
                              (elab-mod$ap elab-mod$a))))
  (let ((__function__ 'update-elab-mod$a->orig-mod))
    (declare (ignorable __function__))
    (s :orig-mod (module-fix m)
       (elab-mod$a-fix elab-mod$a))))

Theorem: elab-mod$ap-of-update-elab-mod$a->orig-mod

(defthm elab-mod$ap-of-update-elab-mod$a->orig-mod
  (b* ((elab-mod$a2 (update-elab-mod$a->orig-mod m elab-mod$a)))
    (elab-mod$ap elab-mod$a2))
  :rule-classes :rewrite)

Theorem: update-elab-mod$a->orig-mod-of-module-fix-m

(defthm update-elab-mod$a->orig-mod-of-module-fix-m
  (equal (update-elab-mod$a->orig-mod (module-fix m)
                                      elab-mod$a)
         (update-elab-mod$a->orig-mod m elab-mod$a)))

Theorem: update-elab-mod$a->orig-mod-module-equiv-congruence-on-m

(defthm update-elab-mod$a->orig-mod-module-equiv-congruence-on-m
  (implies (module-equiv m m-equiv)
           (equal (update-elab-mod$a->orig-mod m elab-mod$a)
                  (update-elab-mod$a->orig-mod m-equiv elab-mod$a)))
  :rule-classes :congruence)

Theorem: update-elab-mod$a->orig-mod-of-elab-mod$a-fix-elab-mod$a

(defthm update-elab-mod$a->orig-mod-of-elab-mod$a-fix-elab-mod$a
  (equal (update-elab-mod$a->orig-mod m (elab-mod$a-fix elab-mod$a))
         (update-elab-mod$a->orig-mod m elab-mod$a)))

Theorem: update-elab-mod$a->orig-mod-elab-mod$a-equiv-congruence-on-elab-mod$a

(defthm
 update-elab-mod$a->orig-mod-elab-mod$a-equiv-congruence-on-elab-mod$a
 (implies (elab-mod$a-equiv elab-mod$a elab-mod$a-equiv)
          (equal (update-elab-mod$a->orig-mod m elab-mod$a)
                 (update-elab-mod$a->orig-mod m elab-mod$a-equiv)))
 :rule-classes :congruence)