		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Assigns-vars

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

Definitions and Theorems

Function: assigns-vars

(defun assigns-vars (x)
  (declare (xargs :guard (assigns-p x)))
  (let ((__function__ 'assigns-vars))
    (declare (ignorable __function__))
    (b* ((x (assigns-fix x))
         ((when (atom x)) nil)
         ((driver x1) (cdar x)))
      (append (lhs-vars (caar x))
              (svex-vars x1.value)
              (assigns-vars (cdr x))))))

Theorem: svarlist-p-of-assigns-vars

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

Theorem: assigns-vars-of-assigns-fix-x

(defthm assigns-vars-of-assigns-fix-x
  (equal (assigns-vars (assigns-fix x))
         (assigns-vars x)))

Theorem: assigns-vars-assigns-equiv-congruence-on-x

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