		Search-engine friendly clone of the ACL2 documentation.

Svstmt-compile.lisp

Svstmt-writelist-var-sizes

Signature
(svstmt-writelist-var-sizes x blockstack acc) → sizes
Arguments: x — Guard (svstmt-writelist-p x).; blockstack — Guard (svstack-p blockstack).; acc — Guard (svar-size-alist-p acc).
Returns: sizes — Type (svar-size-alist-p sizes).

Definitions and Theorems

Function: svstmt-writelist-var-sizes

(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: svar-size-alist-p-of-svstmt-writelist-var-sizes

(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: svstmt-writelist-var-sizes-of-svstmt-writelist-fix-x

(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: svstmt-writelist-var-sizes-svstmt-writelist-equiv-congruence-on-x

(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: svstmt-writelist-var-sizes-of-svstack-fix-blockstack

(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: svstmt-writelist-var-sizes-svstack-equiv-congruence-on-blockstack

(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: svstmt-writelist-var-sizes-of-svar-size-alist-fix-acc

(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: svstmt-writelist-var-sizes-svar-size-alist-equiv-congruence-on-acc

(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)