		Search-engine friendly clone of the ACL2 documentation.

Svexlist-vars

Svexlist-vars-basics

Basic theorems about svexlist-vars.

Definitions and Theorems

Theorem: svexlist-vars-of-cons

(defthm svexlist-vars-of-cons
  (set-equiv (svexlist-vars (cons a b))
             (append (svex-vars a)
                     (svexlist-vars b))))

Theorem: svexlist-vars-of-append

(defthm svexlist-vars-of-append
  (equal (svexlist-vars (append x y))
         (union (svexlist-vars x)
                (svexlist-vars y))))

Set equiv congruence

Theorem: svex-vars-subset-of-svexlist-vars-when-member

(defthm svex-vars-subset-of-svexlist-vars-when-member
  (implies (member x y)
           (subsetp (svex-vars x)
                    (svexlist-vars y))))

Theorem: svexlist-vars-of-subset

(defthm svexlist-vars-of-subset
  (implies (subsetp x y)
           (subsetp (svexlist-vars x)
                    (svexlist-vars y))))

Theorem: set-equiv-implies-equal-svexlist-vars-1

(defthm set-equiv-implies-equal-svexlist-vars-1
  (implies (set-equiv x x-equiv)
           (equal (svexlist-vars x)
                  (svexlist-vars x-equiv)))
  :rule-classes (:congruence))