		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Svar-map-named->indexed

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

Definitions and Theorems

Function: svar-map-named->indexed

(defun svar-map-named->indexed (x modidx moddb)
  (declare (xargs :stobjs (moddb)))
  (declare (xargs :guard (and (svar-map-p x)
                              (natp modidx)
                              (moddb-ok moddb))))
  (declare (xargs :guard (and (svarlist-addr-p (svar-map-vars x))
                              (< modidx (moddb->nmods moddb)))))
  (let ((__function__ 'svar-map-named->indexed))
    (declare (ignorable __function__))
    (b* ((x (svar-map-fix x))
         ((when (atom x)) (mv nil nil))
         ((cons lhs rhs) (car x))
         ((mv err1 lhs)
          (svar-named->indexed lhs modidx moddb))
         ((mv err2 rhs)
          (svar-named->indexed rhs modidx moddb))
         ((mv err3 rest)
          (svar-map-named->indexed (cdr x)
                                   modidx moddb)))
      (mv (or err1 err2 err3)
          (cons (cons lhs rhs) rest)))))

Theorem: svar-map-p-of-svar-map-named->indexed.xx

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

Theorem: svar-map-named->indexed-of-svar-map-fix-x

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

Theorem: svar-map-named->indexed-svar-map-equiv-congruence-on-x

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

Theorem: svar-map-named->indexed-of-nfix-modidx

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

Theorem: svar-map-named->indexed-nat-equiv-congruence-on-modidx

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

Theorem: svar-map-named->indexed-of-moddb-fix-moddb

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

Theorem: svar-map-named->indexed-moddb-equiv-congruence-on-moddb

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

Theorem: svar-map-idxaddr-okp-of-svar-map-named->indexed

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