(svstmt-lhs-check-masks blk-masks nonblk-masks full-lhs blockingp stack) → (mv new-blk-masks new-nonblk-masks conflicts)
Function:
(defun svstmt-lhs-check-masks (blk-masks nonblk-masks full-lhs blockingp stack) (declare (xargs :guard (and (4vmask-alist-p blk-masks) (4vmask-alist-p nonblk-masks) (lhs-p full-lhs) (svstack-p stack)))) (declare (xargs :guard (consp stack))) (let ((__function__ 'svstmt-lhs-check-masks)) (declare (ignorable __function__)) (b* (((mv masks1 conflicts) (lhs-check-masks full-lhs nil nil)) (- (fast-alist-free masks1)) (filtered-lhs (svstack-filter-global-lhs-vars full-lhs stack)) ((mv new-masks confs1) (lhs-check-masks filtered-lhs (if blockingp blk-masks nonblk-masks) nil))) (fast-alist-free confs1) (if blockingp (mv new-masks (4vmask-alist-fix nonblk-masks) conflicts) (mv (4vmask-alist-fix blk-masks) new-masks conflicts)))))
Theorem:
(defthm 4vmask-alist-p-of-svstmt-lhs-check-masks.new-blk-masks (b* (((mv ?new-blk-masks ?new-nonblk-masks ?conflicts) (svstmt-lhs-check-masks blk-masks nonblk-masks full-lhs blockingp stack))) (4vmask-alist-p new-blk-masks)) :rule-classes :rewrite)
Theorem:
(defthm 4vmask-alist-p-of-svstmt-lhs-check-masks.new-nonblk-masks (b* (((mv ?new-blk-masks ?new-nonblk-masks ?conflicts) (svstmt-lhs-check-masks blk-masks nonblk-masks full-lhs blockingp stack))) (4vmask-alist-p new-nonblk-masks)) :rule-classes :rewrite)
Theorem:
(defthm 4vmask-alist-p-of-svstmt-lhs-check-masks.conflicts (b* (((mv ?new-blk-masks ?new-nonblk-masks ?conflicts) (svstmt-lhs-check-masks blk-masks nonblk-masks full-lhs blockingp stack))) (4vmask-alist-p conflicts)) :rule-classes :rewrite)
Theorem:
(defthm svstmt-lhs-check-masks-of-4vmask-alist-fix-blk-masks (equal (svstmt-lhs-check-masks (4vmask-alist-fix blk-masks) nonblk-masks full-lhs blockingp stack) (svstmt-lhs-check-masks blk-masks nonblk-masks full-lhs blockingp stack)))
Theorem:
(defthm svstmt-lhs-check-masks-4vmask-alist-equiv-congruence-on-blk-masks (implies (4vmask-alist-equiv blk-masks blk-masks-equiv) (equal (svstmt-lhs-check-masks blk-masks nonblk-masks full-lhs blockingp stack) (svstmt-lhs-check-masks blk-masks-equiv nonblk-masks full-lhs blockingp stack))) :rule-classes :congruence)
Theorem:
(defthm svstmt-lhs-check-masks-of-4vmask-alist-fix-nonblk-masks (equal (svstmt-lhs-check-masks blk-masks (4vmask-alist-fix nonblk-masks) full-lhs blockingp stack) (svstmt-lhs-check-masks blk-masks nonblk-masks full-lhs blockingp stack)))
Theorem:
(defthm svstmt-lhs-check-masks-4vmask-alist-equiv-congruence-on-nonblk-masks (implies (4vmask-alist-equiv nonblk-masks nonblk-masks-equiv) (equal (svstmt-lhs-check-masks blk-masks nonblk-masks full-lhs blockingp stack) (svstmt-lhs-check-masks blk-masks nonblk-masks-equiv full-lhs blockingp stack))) :rule-classes :congruence)
Theorem:
(defthm svstmt-lhs-check-masks-of-lhs-fix-full-lhs (equal (svstmt-lhs-check-masks blk-masks nonblk-masks (lhs-fix full-lhs) blockingp stack) (svstmt-lhs-check-masks blk-masks nonblk-masks full-lhs blockingp stack)))
Theorem:
(defthm svstmt-lhs-check-masks-lhs-equiv-congruence-on-full-lhs (implies (lhs-equiv full-lhs full-lhs-equiv) (equal (svstmt-lhs-check-masks blk-masks nonblk-masks full-lhs blockingp stack) (svstmt-lhs-check-masks blk-masks nonblk-masks full-lhs-equiv blockingp stack))) :rule-classes :congruence)
Theorem:
(defthm svstmt-lhs-check-masks-of-svstack-fix-stack (equal (svstmt-lhs-check-masks blk-masks nonblk-masks full-lhs blockingp (svstack-fix stack)) (svstmt-lhs-check-masks blk-masks nonblk-masks full-lhs blockingp stack)))
Theorem:
(defthm svstmt-lhs-check-masks-svstack-equiv-congruence-on-stack (implies (svstack-equiv stack stack-equiv) (equal (svstmt-lhs-check-masks blk-masks nonblk-masks full-lhs blockingp stack) (svstmt-lhs-check-masks blk-masks nonblk-masks full-lhs blockingp stack-equiv))) :rule-classes :congruence)