		Search-engine friendly clone of the ACL2 documentation.

Process.lisp

Svtv-collect-masks

Signature
(svtv-collect-masks x) → xx
Arguments: x — Guard (svtv-lines-p x).
Returns: xx — Type (svar-boolmasks-p xx).

Definitions and Theorems

Function: svtv-collect-masks

(defun svtv-collect-masks (x)
  (declare (xargs :guard (svtv-lines-p x)))
  (let ((__function__ 'svtv-collect-masks))
    (declare (ignorable __function__))
    (b* (((when (atom x)) nil)
         ((svtv-line xf) (car x))
         (vars (svtv-entries->vars xf.entries))
         (overrideconds (svtv-entries->overrideconds xf.entries))
         (mask (lhs->mask xf.lhs)))
      (append (pairlis$ vars (replicate (len vars) mask))
              (pairlis$ overrideconds
                        (replicate (len overrideconds) mask))
              (svtv-collect-masks (cdr x))))))

Theorem: svar-boolmasks-p-of-svtv-collect-masks

(defthm svar-boolmasks-p-of-svtv-collect-masks
  (b* ((xx (svtv-collect-masks x)))
    (svar-boolmasks-p xx))
  :rule-classes :rewrite)

Theorem: svtv-collect-masks-of-svtv-lines-fix-x

(defthm svtv-collect-masks-of-svtv-lines-fix-x
  (equal (svtv-collect-masks (svtv-lines-fix x))
         (svtv-collect-masks x)))

Theorem: svtv-collect-masks-svtv-lines-equiv-congruence-on-x

(defthm svtv-collect-masks-svtv-lines-equiv-congruence-on-x
  (implies (svtv-lines-equiv x x-equiv)
           (equal (svtv-collect-masks x)
                  (svtv-collect-masks x-equiv)))
  :rule-classes :congruence)