		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Moddb-wireidx->paths

Signature
(moddb-wireidx->paths wires modidx moddb) → paths
Arguments: wires — Guard (nat-listp wires).; modidx — Guard (natp modidx).; moddb — Guard (moddb-ok moddb).
Returns: paths — Type (pathlist-p paths).

Definitions and Theorems

Function: moddb-wireidx->paths

(defun moddb-wireidx->paths (wires modidx moddb)
  (declare (xargs :stobjs (moddb)))
  (declare (xargs :guard (and (nat-listp wires)
                              (natp modidx)
                              (moddb-ok moddb))))
  (declare
       (xargs :guard (and (< modidx (moddb->nmods moddb))
                          (< (nat-list-max wires)
                             (moddb-mod-totalwires modidx moddb)))))
  (let ((__function__ 'moddb-wireidx->paths))
    (declare (ignorable __function__))
    (if (atom wires)
        nil
      (cons (moddb-wireidx->path (car wires)
                                 modidx moddb)
            (moddb-wireidx->paths (cdr wires)
                                  modidx moddb)))))

Theorem: pathlist-p-of-moddb-wireidx->paths

(defthm pathlist-p-of-moddb-wireidx->paths
  (b* ((paths (moddb-wireidx->paths wires modidx moddb)))
    (pathlist-p paths))
  :rule-classes :rewrite)

Theorem: moddb-wireidx->paths-of-nat-list-fix-wires

(defthm moddb-wireidx->paths-of-nat-list-fix-wires
  (equal (moddb-wireidx->paths (acl2::nat-list-fix wires)
                               modidx moddb)
         (moddb-wireidx->paths wires modidx moddb)))

Theorem: moddb-wireidx->paths-nat-list-equiv-congruence-on-wires

(defthm moddb-wireidx->paths-nat-list-equiv-congruence-on-wires
  (implies (acl2::nat-list-equiv wires wires-equiv)
           (equal (moddb-wireidx->paths wires modidx moddb)
                  (moddb-wireidx->paths wires-equiv modidx moddb)))
  :rule-classes :congruence)

Theorem: moddb-wireidx->paths-of-nfix-modidx

(defthm moddb-wireidx->paths-of-nfix-modidx
  (equal (moddb-wireidx->paths wires (nfix modidx)
                               moddb)
         (moddb-wireidx->paths wires modidx moddb)))

Theorem: moddb-wireidx->paths-nat-equiv-congruence-on-modidx

(defthm moddb-wireidx->paths-nat-equiv-congruence-on-modidx
  (implies (nat-equiv modidx modidx-equiv)
           (equal (moddb-wireidx->paths wires modidx moddb)
                  (moddb-wireidx->paths wires modidx-equiv moddb)))
  :rule-classes :congruence)

Theorem: moddb-wireidx->paths-of-moddb-fix-moddb

(defthm moddb-wireidx->paths-of-moddb-fix-moddb
  (equal (moddb-wireidx->paths wires modidx (moddb-fix moddb))
         (moddb-wireidx->paths wires modidx moddb)))

Theorem: moddb-wireidx->paths-moddb-equiv-congruence-on-moddb

(defthm moddb-wireidx->paths-moddb-equiv-congruence-on-moddb
  (implies (moddb-equiv moddb moddb-equiv)
           (equal (moddb-wireidx->paths wires modidx moddb)
                  (moddb-wireidx->paths wires modidx moddb-equiv)))
  :rule-classes :congruence)