		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Lhspairs->absindexed-nrev

Signature
(lhspairs->absindexed-nrev x scope moddb nrev nrev1) → (mv nrev nrev1)
Arguments: x — Guard (lhspairs-p x).; scope — Guard (modscope-p scope).; moddb — Guard (moddb-ok moddb).

Definitions and Theorems

Function: lhspairs->absindexed-nrev

(defun lhspairs->absindexed-nrev (x scope moddb nrev nrev1)
 (declare (xargs :stobjs (moddb nrev nrev1)))
 (declare (xargs :guard (and (lhspairs-p x)
                             (modscope-p scope)
                             (moddb-ok moddb))))
 (declare
  (xargs
   :guard
   (and (modscope-okp scope moddb)
        (svarlist-idxaddr-okp (lhspairs-vars x)
                              (modscope-local-bound scope moddb)))))
 (let ((__function__ 'lhspairs->absindexed-nrev))
   (declare (ignorable __function__))
   (b* ((x (lhspairs-fix x))
        ((when (atom x))
         (b* ((nrev (acl2::nrev-fix nrev))
              (nrev1 (acl2::nrev-fix nrev1)))
           (mv nrev nrev1)))
        ((cons lhs rhs) (car x))
        ((mv fails1 lhs)
         (lhs->absindexed lhs scope moddb))
        ((mv fails2 rhs)
         (lhs->absindexed rhs scope moddb))
        (nrev (acl2::nrev-append fails1 nrev))
        (nrev (acl2::nrev-append fails2 nrev))
        (nrev1 (acl2::nrev-push (cons lhs rhs) nrev1)))
     (lhspairs->absindexed-nrev (cdr x)
                                scope moddb nrev nrev1))))

Theorem: lhspairs->absindexed-nrev-of-lhspairs-fix-x

(defthm lhspairs->absindexed-nrev-of-lhspairs-fix-x
  (equal (lhspairs->absindexed-nrev (lhspairs-fix x)
                                    scope moddb nrev nrev1)
         (lhspairs->absindexed-nrev x scope moddb nrev nrev1)))

Theorem: lhspairs->absindexed-nrev-lhspairs-equiv-congruence-on-x

(defthm lhspairs->absindexed-nrev-lhspairs-equiv-congruence-on-x
 (implies
   (lhspairs-equiv x x-equiv)
   (equal
        (lhspairs->absindexed-nrev x scope moddb nrev nrev1)
        (lhspairs->absindexed-nrev x-equiv scope moddb nrev nrev1)))
 :rule-classes :congruence)

Theorem: lhspairs->absindexed-nrev-of-modscope-fix-scope

(defthm lhspairs->absindexed-nrev-of-modscope-fix-scope
  (equal (lhspairs->absindexed-nrev x (modscope-fix scope)
                                    moddb nrev nrev1)
         (lhspairs->absindexed-nrev x scope moddb nrev nrev1)))

Theorem: lhspairs->absindexed-nrev-modscope-equiv-congruence-on-scope

(defthm lhspairs->absindexed-nrev-modscope-equiv-congruence-on-scope
 (implies
   (modscope-equiv scope scope-equiv)
   (equal
        (lhspairs->absindexed-nrev x scope moddb nrev nrev1)
        (lhspairs->absindexed-nrev x scope-equiv moddb nrev nrev1)))
 :rule-classes :congruence)

Theorem: lhspairs->absindexed-nrev-of-moddb-fix-moddb

(defthm lhspairs->absindexed-nrev-of-moddb-fix-moddb
  (equal (lhspairs->absindexed-nrev x scope (moddb-fix moddb)
                                    nrev nrev1)
         (lhspairs->absindexed-nrev x scope moddb nrev nrev1)))

Theorem: lhspairs->absindexed-nrev-moddb-equiv-congruence-on-moddb

(defthm lhspairs->absindexed-nrev-moddb-equiv-congruence-on-moddb
 (implies
   (moddb-equiv moddb moddb-equiv)
   (equal
        (lhspairs->absindexed-nrev x scope moddb nrev nrev1)
        (lhspairs->absindexed-nrev x scope moddb-equiv nrev nrev1)))
 :rule-classes :congruence)