		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Elab-mod$a-add-inst

Signature
(elab-mod$a-add-inst elab-modinst$c elab-mod$a) → elab-mod$a2
Arguments: 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: elab-mod$a-add-inst

(defun elab-mod$a-add-inst (elab-modinst$c elab-mod$a)
 (declare (xargs :stobjs (elab-modinst$c)))
 (declare (xargs :guard (elab-mod$ap elab-mod$a)))
 (let ((__function__ 'elab-mod$a-add-inst))
  (declare (ignorable __function__))
  (let*
     ((elab-modinst (non-exec (elab-modinst$c-fix elab-modinst$c)))
      (iname (non-exec (elab-modinst$c->instname elab-modinst)))
      (elab-mod$a (elab-mod$a-fix elab-mod$a))
      (insts (g :insts elab-mod$a)))
   (s :insts
      (if (member-equal iname (elab-modinst-list-names insts))
          insts
        (append-without-guard insts (list (non-exec elab-modinst))))
      elab-mod$a))))

Theorem: elab-mod$ap-of-elab-mod$a-add-inst

(defthm elab-mod$ap-of-elab-mod$a-add-inst
 (b* ((elab-mod$a2 (elab-mod$a-add-inst elab-modinst$c elab-mod$a)))
   (elab-mod$ap elab-mod$a2))
 :rule-classes :rewrite)

Theorem: elab-mod$a-add-inst-of-elab-modinst-fix-elab-modinst$c

(defthm elab-mod$a-add-inst-of-elab-modinst-fix-elab-modinst$c
  (equal (elab-mod$a-add-inst (elab-modinst-fix elab-modinst$c)
                              elab-mod$a)
         (elab-mod$a-add-inst elab-modinst$c elab-mod$a)))

Theorem: elab-mod$a-add-inst-elab-modinst$c-equiv-congruence-on-elab-modinst$c

(defthm
 elab-mod$a-add-inst-elab-modinst$c-equiv-congruence-on-elab-modinst$c
 (implies
      (elab-modinst$c-equiv elab-modinst$c elab-modinst$c-equiv)
      (equal (elab-mod$a-add-inst elab-modinst$c elab-mod$a)
             (elab-mod$a-add-inst elab-modinst$c-equiv elab-mod$a)))
 :rule-classes :congruence)

Theorem: elab-mod$a-add-inst-of-elab-mod$a-fix-elab-mod$a

(defthm elab-mod$a-add-inst-of-elab-mod$a-fix-elab-mod$a
  (equal (elab-mod$a-add-inst elab-modinst$c
                              (elab-mod$a-fix elab-mod$a))
         (elab-mod$a-add-inst elab-modinst$c elab-mod$a)))

Theorem: elab-mod$a-add-inst-elab-mod$a-equiv-congruence-on-elab-mod$a

(defthm
      elab-mod$a-add-inst-elab-mod$a-equiv-congruence-on-elab-mod$a
 (implies
      (elab-mod$a-equiv elab-mod$a elab-mod$a-equiv)
      (equal (elab-mod$a-add-inst elab-modinst$c elab-mod$a)
             (elab-mod$a-add-inst elab-modinst$c elab-mod$a-equiv)))
 :rule-classes :congruence)