		Search-engine friendly clone of the ACL2 documentation.

Bit-blasting

Svexlist->a4vec-nrev

Signature
(svexlist->a4vec-nrev x env masks memo acl2::nrev) → (mv new-nrev memo1)
Arguments: x — Guard (svexlist-p x).; env — Guard (svex-a4vec-env-p env).; masks — Guard (svex-mask-alist-p masks).; memo — Guard (svex-aig-memotable-p memo).
Returns: memo1 — Type (svex-aig-memotable-p memo1).

Definitions and Theorems

Function: svexlist->a4vec-nrev

(defun svexlist->a4vec-nrev (x env masks memo acl2::nrev)
  (declare (xargs :stobjs (acl2::nrev)))
  (declare (xargs :guard (and (svexlist-p x)
                              (svex-a4vec-env-p env)
                              (svex-mask-alist-p masks)
                              (svex-aig-memotable-p memo))))
  (let ((__function__ 'svexlist->a4vec-nrev))
    (declare (ignorable __function__))
    (if (atom x)
        (b* ((acl2::nrev (acl2::nrev-fix acl2::nrev)))
          (mv acl2::nrev
              (svex-aig-memotable-fix memo)))
      (b* (((mv first memo)
            (svex->a4vec-memo (car x)
                              env masks memo))
           (acl2::nrev (acl2::nrev-push first acl2::nrev)))
        (svexlist->a4vec-nrev (cdr x)
                              env masks memo acl2::nrev)))))

Theorem: svex-aig-memotable-p-of-svexlist->a4vec-nrev.memo1

(defthm svex-aig-memotable-p-of-svexlist->a4vec-nrev.memo1
  (b* (((mv ?new-nrev ?memo1)
        (svexlist->a4vec-nrev x env masks memo acl2::nrev)))
    (svex-aig-memotable-p memo1))
  :rule-classes :rewrite)

Theorem: svexlist->a4vec-nrev-removal

(defthm svexlist->a4vec-nrev-removal
  (b* (((mv ?new-nrev ?memo1)
        (svexlist->a4vec-nrev x env masks memo acl2::nrev)))
    (b* (((mv out-spec memo1-spec)
          (svexlist->a4vec-memo x env masks memo)))
      (and (equal new-nrev (append acl2::nrev out-spec))
           (equal memo1 memo1-spec)))))

Theorem: svexlist->a4vec-nrev-of-svexlist-fix-x

(defthm svexlist->a4vec-nrev-of-svexlist-fix-x
  (equal (svexlist->a4vec-nrev (svexlist-fix x)
                               env masks memo acl2::nrev)
         (svexlist->a4vec-nrev x env masks memo acl2::nrev)))

Theorem: svexlist->a4vec-nrev-svexlist-equiv-congruence-on-x

(defthm svexlist->a4vec-nrev-svexlist-equiv-congruence-on-x
 (implies
   (svexlist-equiv x x-equiv)
   (equal (svexlist->a4vec-nrev x env masks memo acl2::nrev)
          (svexlist->a4vec-nrev x-equiv env masks memo acl2::nrev)))
 :rule-classes :congruence)

Theorem: svexlist->a4vec-nrev-of-svex-a4vec-env-fix-env

(defthm svexlist->a4vec-nrev-of-svex-a4vec-env-fix-env
  (equal (svexlist->a4vec-nrev x (svex-a4vec-env-fix env)
                               masks memo acl2::nrev)
         (svexlist->a4vec-nrev x env masks memo acl2::nrev)))

Theorem: svexlist->a4vec-nrev-svex-a4vec-env-equiv-congruence-on-env

(defthm svexlist->a4vec-nrev-svex-a4vec-env-equiv-congruence-on-env
 (implies
   (svex-a4vec-env-equiv env env-equiv)
   (equal (svexlist->a4vec-nrev x env masks memo acl2::nrev)
          (svexlist->a4vec-nrev x env-equiv masks memo acl2::nrev)))
 :rule-classes :congruence)

Theorem: svexlist->a4vec-nrev-of-svex-mask-alist-fix-masks

(defthm svexlist->a4vec-nrev-of-svex-mask-alist-fix-masks
  (equal (svexlist->a4vec-nrev x env (svex-mask-alist-fix masks)
                               memo acl2::nrev)
         (svexlist->a4vec-nrev x env masks memo acl2::nrev)))

Theorem: svexlist->a4vec-nrev-svex-mask-alist-equiv-congruence-on-masks

(defthm
     svexlist->a4vec-nrev-svex-mask-alist-equiv-congruence-on-masks
 (implies
   (svex-mask-alist-equiv masks masks-equiv)
   (equal (svexlist->a4vec-nrev x env masks memo acl2::nrev)
          (svexlist->a4vec-nrev x env masks-equiv memo acl2::nrev)))
 :rule-classes :congruence)

Theorem: svexlist->a4vec-nrev-of-svex-aig-memotable-fix-memo

(defthm svexlist->a4vec-nrev-of-svex-aig-memotable-fix-memo
  (equal
       (svexlist->a4vec-nrev x
                             env masks (svex-aig-memotable-fix memo)
                             acl2::nrev)
       (svexlist->a4vec-nrev x env masks memo acl2::nrev)))

Theorem: svexlist->a4vec-nrev-svex-aig-memotable-equiv-congruence-on-memo

(defthm
   svexlist->a4vec-nrev-svex-aig-memotable-equiv-congruence-on-memo
 (implies
   (svex-aig-memotable-equiv memo memo-equiv)
   (equal (svexlist->a4vec-nrev x env masks memo acl2::nrev)
          (svexlist->a4vec-nrev x env masks memo-equiv acl2::nrev)))
 :rule-classes :congruence)