		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Moddb-mod-nwires

Signature
(moddb-mod-nwires modidx moddb) → nwires
Arguments: modidx — Guard (natp modidx).; moddb — Guard (moddb-basics-ok moddb).
Returns: nwires — Type (natp nwires).

Definitions and Theorems

Function: moddb-mod-nwires

(defun moddb-mod-nwires (modidx moddb)
  (declare (xargs :stobjs (moddb)))
  (declare (xargs :guard (and (natp modidx)
                              (moddb-basics-ok moddb))))
  (declare (xargs :guard (< modidx (moddb->nmods moddb))))
  (let ((__function__ 'moddb-mod-nwires))
    (declare (ignorable __function__))
    (b* (((unless (mbt (< (lnfix modidx)
                          (moddb->nmods moddb))))
          0)
         ((stobj-get nwires)
          ((elab-mod (moddb->modsi modidx moddb)))
          (elab-mod-nwires elab-mod)))
      nwires)))

Theorem: natp-of-moddb-mod-nwires

(defthm natp-of-moddb-mod-nwires
  (b* ((nwires (moddb-mod-nwires modidx moddb)))
    (natp nwires))
  :rule-classes :type-prescription)

Theorem: moddb-mod-nwires-of-nfix-modidx

(defthm moddb-mod-nwires-of-nfix-modidx
  (equal (moddb-mod-nwires (nfix modidx) moddb)
         (moddb-mod-nwires modidx moddb)))

Theorem: moddb-mod-nwires-nat-equiv-congruence-on-modidx

(defthm moddb-mod-nwires-nat-equiv-congruence-on-modidx
  (implies (nat-equiv modidx modidx-equiv)
           (equal (moddb-mod-nwires modidx moddb)
                  (moddb-mod-nwires modidx-equiv moddb)))
  :rule-classes :congruence)

Theorem: moddb-mod-nwires-of-moddb-fix-moddb

(defthm moddb-mod-nwires-of-moddb-fix-moddb
  (equal (moddb-mod-nwires modidx (moddb-fix moddb))
         (moddb-mod-nwires modidx moddb)))

Theorem: moddb-mod-nwires-moddb-equiv-congruence-on-moddb

(defthm moddb-mod-nwires-moddb-equiv-congruence-on-moddb
  (implies (moddb-equiv moddb moddb-equiv)
           (equal (moddb-mod-nwires modidx moddb)
                  (moddb-mod-nwires modidx moddb-equiv)))
  :rule-classes :congruence)