		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Update-elab-mod$a->totalwires

Signature
(update-elab-mod$a->totalwires n elab-mod$a) → elab-mod$a2
Arguments: n — Guard (natp n).; 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->totalwires

(defun update-elab-mod$a->totalwires (n elab-mod$a)
  (declare (xargs :guard (and (natp n)
                              (elab-mod$ap elab-mod$a))))
  (let ((__function__ 'update-elab-mod$a->totalwires))
    (declare (ignorable __function__))
    (s :totalwires (nfix n)
       (elab-mod$a-fix elab-mod$a))))

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

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

Theorem: update-elab-mod$a->totalwires-of-nfix-n

(defthm update-elab-mod$a->totalwires-of-nfix-n
  (equal (update-elab-mod$a->totalwires (nfix n)
                                        elab-mod$a)
         (update-elab-mod$a->totalwires n elab-mod$a)))

Theorem: update-elab-mod$a->totalwires-nat-equiv-congruence-on-n

(defthm update-elab-mod$a->totalwires-nat-equiv-congruence-on-n
  (implies
       (nat-equiv n n-equiv)
       (equal (update-elab-mod$a->totalwires n elab-mod$a)
              (update-elab-mod$a->totalwires n-equiv elab-mod$a)))
  :rule-classes :congruence)

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

(defthm update-elab-mod$a->totalwires-of-elab-mod$a-fix-elab-mod$a
  (equal
       (update-elab-mod$a->totalwires n (elab-mod$a-fix elab-mod$a))
       (update-elab-mod$a->totalwires n elab-mod$a)))

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

(defthm
 update-elab-mod$a->totalwires-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->totalwires n elab-mod$a)
             (update-elab-mod$a->totalwires n elab-mod$a-equiv)))
 :rule-classes :congruence)