		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Elab-modinst$c-copy

Signature
(elab-modinst$c-copy elab-modinst$c elab-modinst$c2) → elab-modinst$c2

Definitions and Theorems

Function: elab-modinst$c-copy

(defun elab-modinst$c-copy (elab-modinst$c elab-modinst$c2)
 (declare (xargs :stobjs (elab-modinst$c elab-modinst$c2)))
 (declare (xargs :guard t))
 (let ((__function__ 'elab-modinst$c-copy))
  (declare (ignorable __function__))
  (mbe
   :logic
   (non-exec (elab-modinst$c-fix elab-modinst$c))
   :exec
   (b*
    ((elab-modinst$c2 (update-elab-modinst$c->instname
                           (elab-modinst$c->instname elab-modinst$c)
                           elab-modinst$c2))
     (elab-modinst$c2 (update-elab-modinst$c->modidx
                           (elab-modinst$c->modidx elab-modinst$c)
                           elab-modinst$c2))
     (elab-modinst$c2
          (update-elab-modinst$c->wire-offset
               (elab-modinst$c->wire-offset elab-modinst$c)
               elab-modinst$c2)))
    (update-elab-modinst$c->inst-offset
         (elab-modinst$c->inst-offset elab-modinst$c)
         elab-modinst$c2)))))

Theorem: elab-modinst$c-copy-of-elab-modinst-fix-elab-modinst$c

(defthm elab-modinst$c-copy-of-elab-modinst-fix-elab-modinst$c
  (equal (elab-modinst$c-copy (elab-modinst-fix elab-modinst$c)
                              elab-modinst$c2)
         (elab-modinst$c-copy elab-modinst$c elab-modinst$c2)))

Theorem: elab-modinst$c-copy-elab-modinst$c-equiv-congruence-on-elab-modinst$c

(defthm
 elab-modinst$c-copy-elab-modinst$c-equiv-congruence-on-elab-modinst$c
 (implies
   (elab-modinst$c-equiv elab-modinst$c elab-modinst$c-equiv)
   (equal
        (elab-modinst$c-copy elab-modinst$c elab-modinst$c2)
        (elab-modinst$c-copy elab-modinst$c-equiv elab-modinst$c2)))
 :rule-classes :congruence)

Theorem: elab-modinst$c-copy-of-elab-modinst-fix-elab-modinst$c2

(defthm elab-modinst$c-copy-of-elab-modinst-fix-elab-modinst$c2
  (equal (elab-modinst$c-copy elab-modinst$c
                              (elab-modinst-fix elab-modinst$c2))
         (elab-modinst$c-copy elab-modinst$c elab-modinst$c2)))

Theorem: elab-modinst$c-copy-elab-modinst$c-equiv-congruence-on-elab-modinst$c2

(defthm
 elab-modinst$c-copy-elab-modinst$c-equiv-congruence-on-elab-modinst$c2
 (implies
   (elab-modinst$c-equiv elab-modinst$c2 elab-modinst$c2-equiv)
   (equal
        (elab-modinst$c-copy elab-modinst$c elab-modinst$c2)
        (elab-modinst$c-copy elab-modinst$c elab-modinst$c2-equiv)))
 :rule-classes :congruence)