		Search-engine friendly clone of the ACL2 documentation.

4v-nsexpr-vars

4v-nsexpr-vars-nonsparse

Non-sparse version.

Don't use this directly; use 4v-nsexpr-vars instead.

Definitions and Theorems

Function: 4v-nsexpr-vars-nonsparse

(defun 4v-nsexpr-vars-nonsparse (x)
  (declare (xargs :guard (4v-nsexpr-p x)))
  (if (atom x)
      (if x (bitset-singleton x) 0)
    (4v-sexpr-vars-list-mask-nonsparse (cdr x))))

Function: 4v-sexpr-vars-list-mask-nonsparse

(defun 4v-sexpr-vars-list-mask-nonsparse (x)
  (declare (xargs :guard (4v-nsexpr-list-p x)))
  (if (atom x)
      0
    (bitset-union (4v-nsexpr-vars-nonsparse (car x))
                  (4v-sexpr-vars-list-mask-nonsparse (cdr x)))))

Function: 4v-nsexpr-vars-nonsparse-memoize-condition

(defun 4v-nsexpr-vars-nonsparse-memoize-condition (x)
  (declare (ignorable x)
           (xargs :guard (4v-nsexpr-p x)))
  (and (consp x) (consp (cdr x))))

Theorem: bitset-members-4v-nsexpr-vars-nonsparse

(defthm bitset-members-4v-nsexpr-vars-nonsparse
  (implies (4v-nsexpr-p x)
           (equal (bitset-members (4v-nsexpr-vars-nonsparse x))
                  (4v-sexpr-vars x))))

Theorem: bitset-members-4v-sexpr-vars-list-mask-nonsparse

(defthm bitset-members-4v-sexpr-vars-list-mask-nonsparse
  (implies
       (4v-nsexpr-list-p x)
       (equal (bitset-members (4v-sexpr-vars-list-mask-nonsparse x))
              (4v-sexpr-vars-list x))))