		Search-engine friendly clone of the ACL2 documentation.

Rewriting

Svex-args-apply-masks

Signature
(svex-args-apply-masks args masks mask-al) → mask-al1
Arguments: args — Guard (svexlist-p args).; masks — Guard (4vmasklist-p masks).; mask-al — Guard (svex-mask-alist-p mask-al).
Returns: mask-al1 — Type (svex-mask-alist-p mask-al1).

Definitions and Theorems

Function: svex-args-apply-masks

(defun svex-args-apply-masks (args masks mask-al)
  (declare (xargs :guard (and (svexlist-p args)
                              (4vmasklist-p masks)
                              (svex-mask-alist-p mask-al))))
  (declare (xargs :guard (equal (len args) (len masks))))
  (let ((__function__ 'svex-args-apply-masks))
    (declare (ignorable __function__))
    (b* (((when (atom args))
          (mbe :logic (svex-mask-alist-fix mask-al)
               :exec mask-al))
         (mask-al (svex-args-apply-masks (cdr args)
                                         (cdr masks)
                                         mask-al))
         (look (svex-mask-lookup (car args) mask-al))
         (mask (4vmask-union (car masks) look)))
      (if (sparseint-equal mask look)
          mask-al
        (svex-mask-acons (car args)
                         mask mask-al)))))

Theorem: svex-mask-alist-p-of-svex-args-apply-masks

(defthm svex-mask-alist-p-of-svex-args-apply-masks
  (b* ((mask-al1 (svex-args-apply-masks args masks mask-al)))
    (svex-mask-alist-p mask-al1))
  :rule-classes :rewrite)

Theorem: svex-args-apply-masks-lookup-subsumes-prev-lookup

(defthm svex-args-apply-masks-lookup-subsumes-prev-lookup
  (4vmask-subsumes
       (svex-mask-lookup x
                         (svex-args-apply-masks args masks mask-al))
       (svex-mask-lookup x mask-al)))

Theorem: svex-args-apply-masks-lookup-when-not-in-args

(defthm svex-args-apply-masks-lookup-when-not-in-args
 (implies
  (not (member (svex-fix y)
               (svexlist-fix args)))
  (equal
       (svex-mask-lookup y
                         (svex-args-apply-masks args masks mask-al))
       (svex-mask-lookup y mask-al))))

Theorem: svex-args-apply-masks-lookup-subsumes-mask

(defthm svex-args-apply-masks-lookup-subsumes-mask
 (implies
  (< (nfix n) (len args))
  (4vmask-subsumes
       (svex-mask-lookup (nth n args)
                         (svex-args-apply-masks args masks mask-al))
       (nth n masks))))

Theorem: svex-args-apply-masks-argmasks-lookup-subsumes-prev-lookup

(defthm svex-args-apply-masks-argmasks-lookup-subsumes-prev-lookup
 (4vmasklist-subsumes
   (svex-argmasks-lookup x
                         (svex-args-apply-masks args masks mask-al))
   (svex-argmasks-lookup x mask-al)))

Theorem: sparseint-equal-implies-equal-sparseint-val-1

(defthm sparseint-equal-implies-equal-sparseint-val-1
  (implies (sparseint-equal x x-equiv)
           (equal (sparseint-val x)
                  (sparseint-val x-equiv)))
  :rule-classes (:congruence))

Function: 4vmask-equal

(defun 4vmask-equal (x y)
  (sparseint-equal (4vmask-fix x)
                   (4vmask-fix y)))

Theorem: 4vmask-equal-is-an-equivalence

(defthm 4vmask-equal-is-an-equivalence
  (and (booleanp (4vmask-equal x y))
       (4vmask-equal x x)
       (implies (4vmask-equal x y)
                (4vmask-equal y x))
       (implies (and (4vmask-equal x y)
                     (4vmask-equal y z))
                (4vmask-equal x z)))
  :rule-classes (:equivalence))

Theorem: svex-args-apply-masks-lookup-when-all

(defthm svex-args-apply-masks-lookup-when-all
 (implies
  (sparseint-equal (svex-mask-lookup x mask-al)
                   -1)
  (sparseint-equal
       (svex-mask-lookup x
                         (svex-args-apply-masks args masks mask-al))
       -1)))

Theorem: svex-args-apply-masks-lookup-when-neg1

(defthm svex-args-apply-masks-lookup-when-neg1
 (implies
  (equal (svex-mask-lookup x mask-al) -1)
  (equal
       (svex-mask-lookup x
                         (svex-args-apply-masks args masks mask-al))
       -1)))

Theorem: svex-args-apply-masks-argmasks-lookups-subsume-masks

(defthm svex-args-apply-masks-argmasks-lookups-subsume-masks
 (implies
  (equal (len args) (len masks))
  (4vmasklist-subsumes
   (svex-argmasks-lookup args
                         (svex-args-apply-masks args masks mask-al))
   masks)))

Theorem: svex-args-apply-masks-of-svexlist-fix-args

(defthm svex-args-apply-masks-of-svexlist-fix-args
  (equal (svex-args-apply-masks (svexlist-fix args)
                                masks mask-al)
         (svex-args-apply-masks args masks mask-al)))

Theorem: svex-args-apply-masks-svexlist-equiv-congruence-on-args

(defthm svex-args-apply-masks-svexlist-equiv-congruence-on-args
  (implies (svexlist-equiv args args-equiv)
           (equal (svex-args-apply-masks args masks mask-al)
                  (svex-args-apply-masks args-equiv masks mask-al)))
  :rule-classes :congruence)

Theorem: svex-args-apply-masks-of-4vmasklist-fix-masks

(defthm svex-args-apply-masks-of-4vmasklist-fix-masks
  (equal (svex-args-apply-masks args (4vmasklist-fix masks)
                                mask-al)
         (svex-args-apply-masks args masks mask-al)))

Theorem: svex-args-apply-masks-4vmasklist-equiv-congruence-on-masks

(defthm svex-args-apply-masks-4vmasklist-equiv-congruence-on-masks
  (implies (4vmasklist-equiv masks masks-equiv)
           (equal (svex-args-apply-masks args masks mask-al)
                  (svex-args-apply-masks args masks-equiv mask-al)))
  :rule-classes :congruence)

Theorem: svex-args-apply-masks-of-svex-mask-alist-fix-mask-al

(defthm svex-args-apply-masks-of-svex-mask-alist-fix-mask-al
  (equal (svex-args-apply-masks args
                                masks (svex-mask-alist-fix mask-al))
         (svex-args-apply-masks args masks mask-al)))

Theorem: svex-args-apply-masks-svex-mask-alist-equiv-congruence-on-mask-al

(defthm
  svex-args-apply-masks-svex-mask-alist-equiv-congruence-on-mask-al
  (implies (svex-mask-alist-equiv mask-al mask-al-equiv)
           (equal (svex-args-apply-masks args masks mask-al)
                  (svex-args-apply-masks args masks mask-al-equiv)))
  :rule-classes :congruence)