		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Assigns-check-masks

Signature
(assigns-check-masks x mask-acc conf-acc) → (mv mask-acc1 conf-acc1)
Arguments: x — Guard (assigns-p x).; mask-acc — Guard (4vmask-alist-p mask-acc).; conf-acc — Guard (4vmask-alist-p conf-acc).
Returns: mask-acc1 — Type (4vmask-alist-p mask-acc1).; conf-acc1 — Type (4vmask-alist-p conf-acc1).

Definitions and Theorems

Function: assigns-check-masks

(defun assigns-check-masks (x mask-acc conf-acc)
  (declare (xargs :guard (and (assigns-p x)
                              (4vmask-alist-p mask-acc)
                              (4vmask-alist-p conf-acc))))
  (let ((__function__ 'assigns-check-masks))
    (declare (ignorable __function__))
    (b* ((x (assigns-fix x))
         (mask-acc (4vmask-alist-fix mask-acc))
         (conf-acc (4vmask-alist-fix conf-acc))
         ((when (atom x)) (mv mask-acc conf-acc))
         ((mv mask-acc conf-acc)
          (lhs-check-masks (caar x)
                           mask-acc conf-acc)))
      (assigns-check-masks (cdr x)
                           mask-acc conf-acc))))

Theorem: 4vmask-alist-p-of-assigns-check-masks.mask-acc1

(defthm 4vmask-alist-p-of-assigns-check-masks.mask-acc1
  (b* (((mv ?mask-acc1 ?conf-acc1)
        (assigns-check-masks x mask-acc conf-acc)))
    (4vmask-alist-p mask-acc1))
  :rule-classes :rewrite)

Theorem: 4vmask-alist-p-of-assigns-check-masks.conf-acc1

(defthm 4vmask-alist-p-of-assigns-check-masks.conf-acc1
  (b* (((mv ?mask-acc1 ?conf-acc1)
        (assigns-check-masks x mask-acc conf-acc)))
    (4vmask-alist-p conf-acc1))
  :rule-classes :rewrite)

Theorem: assigns-check-masks-of-assigns-fix-x

(defthm assigns-check-masks-of-assigns-fix-x
  (equal (assigns-check-masks (assigns-fix x)
                              mask-acc conf-acc)
         (assigns-check-masks x mask-acc conf-acc)))

Theorem: assigns-check-masks-assigns-equiv-congruence-on-x

(defthm assigns-check-masks-assigns-equiv-congruence-on-x
  (implies (assigns-equiv x x-equiv)
           (equal (assigns-check-masks x mask-acc conf-acc)
                  (assigns-check-masks x-equiv mask-acc conf-acc)))
  :rule-classes :congruence)

Theorem: assigns-check-masks-of-4vmask-alist-fix-mask-acc

(defthm assigns-check-masks-of-4vmask-alist-fix-mask-acc
  (equal (assigns-check-masks x (4vmask-alist-fix mask-acc)
                              conf-acc)
         (assigns-check-masks x mask-acc conf-acc)))

Theorem: assigns-check-masks-4vmask-alist-equiv-congruence-on-mask-acc

(defthm
      assigns-check-masks-4vmask-alist-equiv-congruence-on-mask-acc
  (implies (4vmask-alist-equiv mask-acc mask-acc-equiv)
           (equal (assigns-check-masks x mask-acc conf-acc)
                  (assigns-check-masks x mask-acc-equiv conf-acc)))
  :rule-classes :congruence)

Theorem: assigns-check-masks-of-4vmask-alist-fix-conf-acc

(defthm assigns-check-masks-of-4vmask-alist-fix-conf-acc
 (equal (assigns-check-masks x mask-acc (4vmask-alist-fix conf-acc))
        (assigns-check-masks x mask-acc conf-acc)))

Theorem: assigns-check-masks-4vmask-alist-equiv-congruence-on-conf-acc

(defthm
      assigns-check-masks-4vmask-alist-equiv-congruence-on-conf-acc
  (implies (4vmask-alist-equiv conf-acc conf-acc-equiv)
           (equal (assigns-check-masks x mask-acc conf-acc)
                  (assigns-check-masks x mask-acc conf-acc-equiv)))
  :rule-classes :congruence)