(svstmt-writelist-var-sizes x blockstack acc) → sizes
Function:
(defun svstmt-writelist-var-sizes (x blockstack acc) (declare (xargs :guard (and (svstmt-writelist-p x) (svstack-p blockstack) (svar-size-alist-p acc)))) (declare (xargs :guard (consp blockstack))) (let ((__function__ 'svstmt-writelist-var-sizes)) (declare (ignorable __function__)) (if (atom x) (svar-size-alist-fix acc) (svstmt-writelist-var-sizes (cdr x) blockstack (svstmt-write-var-sizes (car x) blockstack acc)))))
Theorem:
(defthm svar-size-alist-p-of-svstmt-writelist-var-sizes (b* ((sizes (svstmt-writelist-var-sizes x blockstack acc))) (svar-size-alist-p sizes)) :rule-classes :rewrite)
Theorem:
(defthm svstmt-writelist-var-sizes-of-svstmt-writelist-fix-x (equal (svstmt-writelist-var-sizes (svstmt-writelist-fix x) blockstack acc) (svstmt-writelist-var-sizes x blockstack acc)))
Theorem:
(defthm svstmt-writelist-var-sizes-svstmt-writelist-equiv-congruence-on-x (implies (svstmt-writelist-equiv x x-equiv) (equal (svstmt-writelist-var-sizes x blockstack acc) (svstmt-writelist-var-sizes x-equiv blockstack acc))) :rule-classes :congruence)
Theorem:
(defthm svstmt-writelist-var-sizes-of-svstack-fix-blockstack (equal (svstmt-writelist-var-sizes x (svstack-fix blockstack) acc) (svstmt-writelist-var-sizes x blockstack acc)))
Theorem:
(defthm svstmt-writelist-var-sizes-svstack-equiv-congruence-on-blockstack (implies (svstack-equiv blockstack blockstack-equiv) (equal (svstmt-writelist-var-sizes x blockstack acc) (svstmt-writelist-var-sizes x blockstack-equiv acc))) :rule-classes :congruence)
Theorem:
(defthm svstmt-writelist-var-sizes-of-svar-size-alist-fix-acc (equal (svstmt-writelist-var-sizes x blockstack (svar-size-alist-fix acc)) (svstmt-writelist-var-sizes x blockstack acc)))
Theorem:
(defthm svstmt-writelist-var-sizes-svar-size-alist-equiv-congruence-on-acc (implies (svar-size-alist-equiv acc acc-equiv) (equal (svstmt-writelist-var-sizes x blockstack acc) (svstmt-writelist-var-sizes x blockstack acc-equiv))) :rule-classes :congruence)