		Search-engine friendly clone of the ACL2 documentation.

Bit-blasting

Svexlist->a4vec-top

Signature
(svexlist->a4vec-top x env masks) → *
Arguments: x — Guard (svexlist-p x).; env — Guard (svex-a4vec-env-p env).; masks — Guard (svex-mask-alist-p masks).

Definitions and Theorems

Function: svexlist->a4vec-top

(defun svexlist->a4vec-top (x env masks)
 (declare (xargs :guard (and (svexlist-p x)
                             (svex-a4vec-env-p env)
                             (svex-mask-alist-p masks))))
 (let ((__function__ 'svexlist->a4vec-top))
  (declare (ignorable __function__))
  (mbe
   :logic (svexlist->a4vec x env masks)
   :exec
   (b*
    (((mv res memo)
      (with-local-stobj
        acl2::nrev
        (mv-let
            (res memo acl2::nrev)
            (b* (((mv acl2::nrev memo)
                  (svexlist->a4vec-nrev x env masks nil acl2::nrev))
                 ((mv res acl2::nrev)
                  (acl2::nrev-finish acl2::nrev)))
              (mv res memo acl2::nrev))
          (mv res memo)))))
    (fast-alist-free memo)
    res))))

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

(defthm svexlist->a4vec-top-of-svexlist-fix-x
  (equal (svexlist->a4vec-top (svexlist-fix x)
                              env masks)
         (svexlist->a4vec-top x env masks)))

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

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

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

(defthm svexlist->a4vec-top-of-svex-a4vec-env-fix-env
  (equal (svexlist->a4vec-top x (svex-a4vec-env-fix env)
                              masks)
         (svexlist->a4vec-top x env masks)))

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

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

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

(defthm svexlist->a4vec-top-of-svex-mask-alist-fix-masks
  (equal (svexlist->a4vec-top x env (svex-mask-alist-fix masks))
         (svexlist->a4vec-top x env masks)))

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

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