		Search-engine friendly clone of the ACL2 documentation.

Rewriting

Svex-mask-acons

Signature
(svex-mask-acons x m al) → aa
Arguments: x — Guard (svex-p x).; m — Guard (4vmask-p m).; al — Guard (svex-mask-alist-p al).
Returns: aa — Type (svex-mask-alist-p aa).

Definitions and Theorems

Function: svex-mask-acons

(defun svex-mask-acons (x m al)
  (declare (xargs :guard (and (svex-p x)
                              (4vmask-p m)
                              (svex-mask-alist-p al))))
  (let ((__function__ 'svex-mask-acons))
    (declare (ignorable __function__))
    (mbe :logic (cons (cons (svex-fix x) (4vmask-fix m))
                      (svex-mask-alist-fix al))
         :exec (hons-acons x m al))))

Theorem: svex-mask-alist-p-of-svex-mask-acons

(defthm svex-mask-alist-p-of-svex-mask-acons
  (b* ((aa (svex-mask-acons x m al)))
    (svex-mask-alist-p aa))
  :rule-classes :rewrite)

Theorem: svex-mask-acons-of-svex-fix-x

(defthm svex-mask-acons-of-svex-fix-x
  (equal (svex-mask-acons (svex-fix x) m al)
         (svex-mask-acons x m al)))

Theorem: svex-mask-acons-svex-equiv-congruence-on-x

(defthm svex-mask-acons-svex-equiv-congruence-on-x
  (implies (svex-equiv x x-equiv)
           (equal (svex-mask-acons x m al)
                  (svex-mask-acons x-equiv m al)))
  :rule-classes :congruence)

Theorem: svex-mask-acons-of-4vmask-fix-m

(defthm svex-mask-acons-of-4vmask-fix-m
  (equal (svex-mask-acons x (4vmask-fix m) al)
         (svex-mask-acons x m al)))

Theorem: svex-mask-acons-4vmask-equiv-congruence-on-m

(defthm svex-mask-acons-4vmask-equiv-congruence-on-m
  (implies (4vmask-equiv m m-equiv)
           (equal (svex-mask-acons x m al)
                  (svex-mask-acons x m-equiv al)))
  :rule-classes :congruence)

Theorem: svex-mask-acons-of-svex-mask-alist-fix-al

(defthm svex-mask-acons-of-svex-mask-alist-fix-al
  (equal (svex-mask-acons x m (svex-mask-alist-fix al))
         (svex-mask-acons x m al)))

Theorem: svex-mask-acons-svex-mask-alist-equiv-congruence-on-al

(defthm svex-mask-acons-svex-mask-alist-equiv-congruence-on-al
  (implies (svex-mask-alist-equiv al al-equiv)
           (equal (svex-mask-acons x m al)
                  (svex-mask-acons x m al-equiv)))
  :rule-classes :congruence)