		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Elab-mod$a-wiretablei

Signature
(elab-mod$a-wiretablei idx elab-mod$a) → wire
Arguments: idx — Guard (natp idx).; elab-mod$a — Guard (elab-mod$ap elab-mod$a).
Returns: wire — Type (wire-p wire).

Definitions and Theorems

Function: elab-mod$a-wiretablei

(defun elab-mod$a-wiretablei (idx elab-mod$a)
  (declare (xargs :guard (and (natp idx)
                              (elab-mod$ap elab-mod$a))))
  (declare (xargs :guard (< idx (elab-mod$a-nwires elab-mod$a))))
  (let ((__function__ 'elab-mod$a-wiretablei))
    (declare (ignorable __function__))
    (wire-fix (nth idx
                   (g :wires (elab-mod$a-fix elab-mod$a))))))

Theorem: wire-p-of-elab-mod$a-wiretablei

(defthm wire-p-of-elab-mod$a-wiretablei
  (b* ((wire (elab-mod$a-wiretablei idx elab-mod$a)))
    (wire-p wire))
  :rule-classes :rewrite)

Theorem: elab-mod$a-wiretablei-of-nfix-idx

(defthm elab-mod$a-wiretablei-of-nfix-idx
  (equal (elab-mod$a-wiretablei (nfix idx)
                                elab-mod$a)
         (elab-mod$a-wiretablei idx elab-mod$a)))

Theorem: elab-mod$a-wiretablei-nat-equiv-congruence-on-idx

(defthm elab-mod$a-wiretablei-nat-equiv-congruence-on-idx
  (implies (nat-equiv idx idx-equiv)
           (equal (elab-mod$a-wiretablei idx elab-mod$a)
                  (elab-mod$a-wiretablei idx-equiv elab-mod$a)))
  :rule-classes :congruence)

Theorem: elab-mod$a-wiretablei-of-elab-mod$a-fix-elab-mod$a

(defthm elab-mod$a-wiretablei-of-elab-mod$a-fix-elab-mod$a
  (equal (elab-mod$a-wiretablei idx (elab-mod$a-fix elab-mod$a))
         (elab-mod$a-wiretablei idx elab-mod$a)))

Theorem: elab-mod$a-wiretablei-elab-mod$a-equiv-congruence-on-elab-mod$a

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