		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Elab-mod$c-wire-abstraction

Signature
(elab-mod$c-wire-abstraction elabmod) → wires
Returns: wires — Type (wirelist-p wires).

Definitions and Theorems

Function: elab-mod$c-wire-abstraction

(defun elab-mod$c-wire-abstraction (elabmod)
  (declare (xargs :guard t))
  (let ((__function__ 'elab-mod$c-wire-abstraction))
    (declare (ignorable __function__))
    (wirelist-fix (take (nth *elab-mod$c->nwires* elabmod)
                        (nth *elab-mod$c->wiretablei* elabmod)))))

Theorem: wirelist-p-of-elab-mod$c-wire-abstraction

(defthm wirelist-p-of-elab-mod$c-wire-abstraction
  (b* ((wires (elab-mod$c-wire-abstraction elabmod)))
    (wirelist-p wires))
  :rule-classes :rewrite)

Theorem: member-of-abstraction-when-wires-ok

(defthm member-of-abstraction-when-wires-ok
 (implies
  (and (elab-mod$c-wires-ok elab-mod$c)
       (name-p x))
  (iff
   (hons-assoc-equal x
                     (nth *elab-mod$c->wirename-idxes-get*
                          elab-mod$c))
   (member
      x
      (wirelist->names (elab-mod$c-wire-abstraction elab-mod$c))))))

Theorem: no-duplicatesp-of-abstraction-when-wires-ok

(defthm no-duplicatesp-of-abstraction-when-wires-ok
 (implies
  (elab-mod$c-wires-ok elab-mod$c)
  (no-duplicatesp
       (wirelist->names (elab-mod$c-wire-abstraction elab-mod$c)))))

Theorem: wirelist-nodups-p-of-abstraction-when-wires-ok

(defthm wirelist-nodups-p-of-abstraction-when-wires-ok
 (implies
      (elab-mod$c-wires-ok elab-mod$c)
      (wirelist-nodups-p (elab-mod$c-wire-abstraction elab-mod$c))))