(svstmt-write-var-sizes x blockstack acc) → sizes
Function:
(defun svstmt-write-var-sizes (x blockstack acc) (declare (xargs :guard (and (svstmt-write-p x) (svstack-p blockstack) (svar-size-alist-p acc)))) (declare (xargs :guard (consp blockstack))) (let ((__function__ 'svstmt-write-var-sizes)) (declare (ignorable __function__)) (b* (((svstmt-write x)) (acc (svar-size-alist-fix acc)) (lhs-var (svex-select-inner-var x.lhs)) ((unless (svstack-globalp lhs-var blockstack)) acc)) (cons (cons lhs-var (svex-select-inner-width x.lhs)) acc))))
Theorem:
(defthm svar-size-alist-p-of-svstmt-write-var-sizes (b* ((sizes (svstmt-write-var-sizes x blockstack acc))) (svar-size-alist-p sizes)) :rule-classes :rewrite)
Theorem:
(defthm svstmt-write-var-sizes-of-svstmt-write-fix-x (equal (svstmt-write-var-sizes (svstmt-write-fix x) blockstack acc) (svstmt-write-var-sizes x blockstack acc)))
Theorem:
(defthm svstmt-write-var-sizes-svstmt-write-equiv-congruence-on-x (implies (svstmt-write-equiv x x-equiv) (equal (svstmt-write-var-sizes x blockstack acc) (svstmt-write-var-sizes x-equiv blockstack acc))) :rule-classes :congruence)
Theorem:
(defthm svstmt-write-var-sizes-of-svstack-fix-blockstack (equal (svstmt-write-var-sizes x (svstack-fix blockstack) acc) (svstmt-write-var-sizes x blockstack acc)))
Theorem:
(defthm svstmt-write-var-sizes-svstack-equiv-congruence-on-blockstack (implies (svstack-equiv blockstack blockstack-equiv) (equal (svstmt-write-var-sizes x blockstack acc) (svstmt-write-var-sizes x blockstack-equiv acc))) :rule-classes :congruence)
Theorem:
(defthm svstmt-write-var-sizes-of-svar-size-alist-fix-acc (equal (svstmt-write-var-sizes x blockstack (svar-size-alist-fix acc)) (svstmt-write-var-sizes x blockstack acc)))
Theorem:
(defthm svstmt-write-var-sizes-svar-size-alist-equiv-congruence-on-acc (implies (svar-size-alist-equiv acc acc-equiv) (equal (svstmt-write-var-sizes x blockstack acc) (svstmt-write-var-sizes x blockstack acc-equiv))) :rule-classes :congruence)