		Search-engine friendly clone of the ACL2 documentation.

Bit-blasting

Svexlistlist->a4vec

Signature
(svexlistlist->a4vec x env masks) → a4vecs
Arguments: x — Guard (svexlistlist-p x).; env — Guard (svex-a4vec-env-p env).; masks — Guard (svex-mask-alist-p masks).
Returns: a4vecs — Type (a4veclistlist-p a4vecs).

Definitions and Theorems

Function: svexlistlist->a4vec

(defun svexlistlist->a4vec (x env masks)
  (declare (xargs :guard (and (svexlistlist-p x)
                              (svex-a4vec-env-p env)
                              (svex-mask-alist-p masks))))
  (let ((__function__ 'svexlistlist->a4vec))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (cons (svexlist->a4vec (car x) env masks)
            (svexlistlist->a4vec (cdr x)
                                 env masks)))))

Theorem: a4veclistlist-p-of-svexlistlist->a4vec

(defthm a4veclistlist-p-of-svexlistlist->a4vec
  (b* ((a4vecs (svexlistlist->a4vec x env masks)))
    (a4veclistlist-p a4vecs))
  :rule-classes :rewrite)

Theorem: svexlistlist->a4vec-of-svexlistlist-fix-x

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

Theorem: svexlistlist->a4vec-svexlistlist-equiv-congruence-on-x

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

Theorem: svexlistlist->a4vec-of-svex-a4vec-env-fix-env

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

Theorem: svexlistlist->a4vec-svex-a4vec-env-equiv-congruence-on-env

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

Theorem: svexlistlist->a4vec-of-svex-mask-alist-fix-masks

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

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

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