		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Lhspairs-named->indexed-aux-nrev

Signature
(lhspairs-named->indexed-aux-nrev x modidx moddb acl2::nrev err) → (mv * acl2::nrev)
Arguments: x — Guard (lhspairs-p x).; modidx — Guard (natp modidx).; moddb — Guard (moddb-ok moddb).

Definitions and Theorems

Function: lhspairs-named->indexed-aux-nrev

(defun lhspairs-named->indexed-aux-nrev
       (x modidx moddb acl2::nrev err)
 (declare (xargs :stobjs (moddb acl2::nrev)))
 (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-aux-nrev))
  (declare (ignorable __function__))
  (b* ((x (lhspairs-fix x))
       ((when (atom x))
        (b* ((acl2::nrev (acl2::nrev-fix acl2::nrev)))
          (mv err acl2::nrev)))
       ((cons lhs rhs) (car x))
       ((mv err1 lhs)
        (lhs-named->indexed lhs modidx moddb))
       ((mv err2 rhs)
        (lhs-named->indexed rhs modidx moddb))
       (err (or err err1 err2))
       (acl2::nrev (acl2::nrev-push (cons lhs rhs)
                                    acl2::nrev)))
   (lhspairs-named->indexed-aux-nrev (cdr x)
                                     modidx moddb acl2::nrev err))))

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

(defthm lhspairs-named->indexed-aux-nrev-of-lhspairs-fix-x
 (equal
  (lhspairs-named->indexed-aux-nrev (lhspairs-fix x)
                                    modidx moddb acl2::nrev err)
  (lhspairs-named->indexed-aux-nrev x modidx moddb acl2::nrev err)))

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

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

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

(defthm lhspairs-named->indexed-aux-nrev-of-nfix-modidx
 (equal
  (lhspairs-named->indexed-aux-nrev x (nfix modidx)
                                    moddb acl2::nrev err)
  (lhspairs-named->indexed-aux-nrev x modidx moddb acl2::nrev err)))

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

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

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

(defthm lhspairs-named->indexed-aux-nrev-of-moddb-fix-moddb
 (equal
  (lhspairs-named->indexed-aux-nrev x modidx (moddb-fix moddb)
                                    acl2::nrev err)
  (lhspairs-named->indexed-aux-nrev x modidx moddb acl2::nrev err)))

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

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