(svtv-collect-masks x) → xx
Function:
(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:
(defthm svar-boolmasks-p-of-svtv-collect-masks (b* ((xx (svtv-collect-masks x))) (svar-boolmasks-p xx)) :rule-classes :rewrite)
Theorem:
(defthm svtv-collect-masks-of-svtv-lines-fix-x (equal (svtv-collect-masks (svtv-lines-fix x)) (svtv-collect-masks x)))
Theorem:
(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)