		Search-engine friendly clone of the ACL2 documentation.

Bit-blasting

Svexlist-full-masks-p

Signature
(svexlist-full-masks-p x masks) → *
Arguments: x — Guard (svexlist-p x).; masks — Guard (svex-mask-alist-p masks).

Definitions and Theorems

Function: svexlist-full-masks-p

(defun svexlist-full-masks-p (x masks)
  (declare (xargs :guard (and (svexlist-p x)
                              (svex-mask-alist-p masks))))
  (let ((__function__ 'svexlist-full-masks-p))
    (declare (ignorable __function__))
    (if (atom x)
        t
      (and (equal -1
                  (sparseint-val (svex-mask-lookup (car x) masks)))
           (svexlist-full-masks-p (cdr x)
                                  masks)))))

Theorem: svexlist-full-masks-p-of-take

(defthm svexlist-full-masks-p-of-take
  (implies (and (svexlist-full-masks-p x masks)
                (<= (nfix n) (len x)))
           (svexlist-full-masks-p (take n x)
                                  masks)))

Theorem: svexlist-full-masks-p-of-nthcdr

(defthm svexlist-full-masks-p-of-nthcdr
  (implies (svexlist-full-masks-p x masks)
           (svexlist-full-masks-p (nthcdr n x)
                                  masks)))

Theorem: svexlist-full-masks-p-of-svexlist-mask-alist-lemma

(defthm svexlist-full-masks-p-of-svexlist-mask-alist-lemma
  (implies (subsetp (svexlist-fix y)
                    (svexlist-fix x))
           (svexlist-full-masks-p y (svexlist-mask-alist x))))

Theorem: svexlist-full-masks-p-of-svexlist-mask-alist

(defthm svexlist-full-masks-p-of-svexlist-mask-alist
  (svexlist-full-masks-p x (svexlist-mask-alist x)))

Theorem: 4veclist-mask-when-full-masksp

(defthm 4veclist-mask-when-full-masksp
  (implies (and (svexlist-full-masks-p x masks)
                (equal (len 4vecs) (len x)))
           (equal (4veclist-mask (svex-argmasks-lookup x masks)
                                 4vecs)
                  (4veclist-fix 4vecs))))

Theorem: svexlist-full-masks-p-of-svexlist-fix-x

(defthm svexlist-full-masks-p-of-svexlist-fix-x
  (equal (svexlist-full-masks-p (svexlist-fix x)
                                masks)
         (svexlist-full-masks-p x masks)))

Theorem: svexlist-full-masks-p-svexlist-equiv-congruence-on-x

(defthm svexlist-full-masks-p-svexlist-equiv-congruence-on-x
  (implies (svexlist-equiv x x-equiv)
           (equal (svexlist-full-masks-p x masks)
                  (svexlist-full-masks-p x-equiv masks)))
  :rule-classes :congruence)

Theorem: svexlist-full-masks-p-of-svex-mask-alist-fix-masks

(defthm svexlist-full-masks-p-of-svex-mask-alist-fix-masks
  (equal (svexlist-full-masks-p x (svex-mask-alist-fix masks))
         (svexlist-full-masks-p x masks)))

Theorem: svexlist-full-masks-p-svex-mask-alist-equiv-congruence-on-masks

(defthm
    svexlist-full-masks-p-svex-mask-alist-equiv-congruence-on-masks
  (implies (svex-mask-alist-equiv masks masks-equiv)
           (equal (svexlist-full-masks-p x masks)
                  (svexlist-full-masks-p x masks-equiv)))
  :rule-classes :congruence)