		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Constraintlist-named->indexed

Signature
(constraintlist-named->indexed x modidx moddb) → (mv errmsg xx)
Arguments: x — Guard (constraintlist-p x).; modidx — Guard (natp modidx).; moddb — Guard (moddb-ok moddb).
Returns: xx — Type (constraintlist-p xx).

Definitions and Theorems

Function: constraintlist-named->indexed

(defun constraintlist-named->indexed (x modidx moddb)
  (declare (xargs :stobjs (moddb)))
  (declare (xargs :guard (and (constraintlist-p x)
                              (natp modidx)
                              (moddb-ok moddb))))
  (declare
       (xargs :guard (and (svarlist-addr-p (constraintlist-vars x))
                          (< modidx (moddb->nmods moddb)))))
  (let ((__function__ 'constraintlist-named->indexed))
    (declare (ignorable __function__))
    (b* (((when (atom x)) (mv nil nil))
         ((constraint x1) (car x))
         ((mv err1 new-cond)
          (svex-named->indexed x1.cond modidx moddb))
         ((mv err2 rest)
          (constraintlist-named->indexed (cdr x)
                                         modidx moddb)))
      (mv (or err1 err2)
          (cons (change-constraint x1 :cond new-cond)
                rest)))))

Theorem: constraintlist-p-of-constraintlist-named->indexed.xx

(defthm constraintlist-p-of-constraintlist-named->indexed.xx
  (b* (((mv ?errmsg ?xx)
        (constraintlist-named->indexed x modidx moddb)))
    (constraintlist-p xx))
  :rule-classes :rewrite)

Theorem: constraintlist-idxaddr-okp-of-constraintlist-named->indexed

(defthm constraintlist-idxaddr-okp-of-constraintlist-named->indexed
 (b* (((mv err ans)
       (constraintlist-named->indexed x modidx moddb)))
  (implies
       (and (moddb-ok moddb)
            (< (nfix modidx)
               (nfix (nth *moddb->nmods* moddb)))
            (not err))
       (svarlist-idxaddr-okp (constraintlist-vars ans)
                             (moddb-mod-totalwires modidx moddb)))))

Theorem: constraintlist-named->indexed-of-constraintlist-fix-x

(defthm constraintlist-named->indexed-of-constraintlist-fix-x
  (equal (constraintlist-named->indexed (constraintlist-fix x)
                                        modidx moddb)
         (constraintlist-named->indexed x modidx moddb)))

Theorem: constraintlist-named->indexed-constraintlist-equiv-congruence-on-x

(defthm
 constraintlist-named->indexed-constraintlist-equiv-congruence-on-x
 (implies
      (constraintlist-equiv x x-equiv)
      (equal (constraintlist-named->indexed x modidx moddb)
             (constraintlist-named->indexed x-equiv modidx moddb)))
 :rule-classes :congruence)

Theorem: constraintlist-named->indexed-of-nfix-modidx

(defthm constraintlist-named->indexed-of-nfix-modidx
  (equal (constraintlist-named->indexed x (nfix modidx)
                                        moddb)
         (constraintlist-named->indexed x modidx moddb)))

Theorem: constraintlist-named->indexed-nat-equiv-congruence-on-modidx

(defthm constraintlist-named->indexed-nat-equiv-congruence-on-modidx
  (implies
       (nat-equiv modidx modidx-equiv)
       (equal (constraintlist-named->indexed x modidx moddb)
              (constraintlist-named->indexed x modidx-equiv moddb)))
  :rule-classes :congruence)

Theorem: constraintlist-named->indexed-of-moddb-fix-moddb

(defthm constraintlist-named->indexed-of-moddb-fix-moddb
  (equal (constraintlist-named->indexed x modidx (moddb-fix moddb))
         (constraintlist-named->indexed x modidx moddb)))

Theorem: constraintlist-named->indexed-moddb-equiv-congruence-on-moddb

(defthm
      constraintlist-named->indexed-moddb-equiv-congruence-on-moddb
  (implies
       (moddb-equiv moddb moddb-equiv)
       (equal (constraintlist-named->indexed x modidx moddb)
              (constraintlist-named->indexed x modidx moddb-equiv)))
  :rule-classes :congruence)