		Search-engine friendly clone of the ACL2 documentation.

Svstmt.lisp

Svstmt-write-vars

Signature
(svstmt-write-vars x) → vars
Arguments: x — Guard (svstmt-write-p x).
Returns: vars — Type (svarlist-p vars).

Definitions and Theorems

Function: svstmt-write-vars

(defun svstmt-write-vars (x)
  (declare (xargs :guard (svstmt-write-p x)))
  (let ((__function__ 'svstmt-write-vars))
    (declare (ignorable __function__))
    (b* (((svstmt-write x)))
      (append-without-guard (svex-select-vars x.lhs)
                            (svex-vars x.rhs)))))

Theorem: svarlist-p-of-svstmt-write-vars

(defthm svarlist-p-of-svstmt-write-vars
  (b* ((vars (svstmt-write-vars x)))
    (svarlist-p vars))
  :rule-classes :rewrite)

Theorem: svstmt-write-vars-of-svstmt-write-fix-x

(defthm svstmt-write-vars-of-svstmt-write-fix-x
  (equal (svstmt-write-vars (svstmt-write-fix x))
         (svstmt-write-vars x)))

Theorem: svstmt-write-vars-svstmt-write-equiv-congruence-on-x

(defthm svstmt-write-vars-svstmt-write-equiv-congruence-on-x
  (implies (svstmt-write-equiv x x-equiv)
           (equal (svstmt-write-vars x)
                  (svstmt-write-vars x-equiv)))
  :rule-classes :congruence)