		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Lhspairs-named->indexed

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

Definitions and Theorems

Function: lhspairs-named->indexed

(defun lhspairs-named->indexed (x modidx moddb)
  (declare (xargs :stobjs (moddb)))
  (declare (xargs :guard (and (lhspairs-p x)
                              (natp modidx)
                              (moddb-ok moddb))))
  (declare (xargs :guard (and (svarlist-addr-p (lhspairs-vars x))
                              (< modidx (moddb->nmods moddb)))))
  (let ((__function__ 'lhspairs-named->indexed))
    (declare (ignorable __function__))
    (mbe :logic
         (b* ((x (lhspairs-fix x))
              ((when (atom x)) (mv nil nil))
              ((cons lhs rhs) (car x))
              ((mv err1 lhs)
               (lhs-named->indexed lhs modidx moddb))
              ((mv err2 rhs)
               (lhs-named->indexed rhs modidx moddb))
              ((mv err3 rest)
               (lhspairs-named->indexed (cdr x)
                                        modidx moddb)))
           (mv (or err1 err2 err3)
               (cons (cons lhs rhs) rest)))
         :exec
         (if (atom x)
             (mv nil nil)
           (with-local-stobj
                acl2::nrev
                (mv-let (err ans acl2::nrev)
                        (b* (((mv err acl2::nrev)
                              (lhspairs-named->indexed-aux-nrev
                                   x modidx moddb acl2::nrev nil))
                             ((mv ans acl2::nrev)
                              (acl2::nrev-finish acl2::nrev)))
                          (mv err ans acl2::nrev))
                  (mv err ans)))))))

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

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

Theorem: lhspairs-named->indexed-true-listp

(defthm lhspairs-named->indexed-true-listp
  (b* (((mv ?errmsg ?xx)
        (lhspairs-named->indexed x modidx moddb)))
    (true-listp xx))
  :rule-classes :type-prescription)

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

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

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

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

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

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

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

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

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

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

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

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

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

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