		Search-engine friendly clone of the ACL2 documentation.

4v-nsexpr-vars

4v-nsexpr-vars-sparse

Sparse version.

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

Definitions and Theorems

Function: 4v-nsexpr-vars-sparse

(defun 4v-nsexpr-vars-sparse (x)
  (declare (xargs :guard (4v-nsexpr-p x)))
  (if (atom x)
      (if x (sbitset-singleton x) nil)
    (4v-sexpr-vars-list-mask-sparse (cdr x))))

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

(defun 4v-sexpr-vars-list-mask-sparse (x)
  (declare (xargs :guard (4v-nsexpr-list-p x)))
  (if (atom x)
      nil
    (sbitset-union (4v-nsexpr-vars-sparse (car x))
                   (4v-sexpr-vars-list-mask-sparse (cdr x)))))

Theorem: sbitsetp-of-4v-nsexpr-vars-sparse

(defthm sbitsetp-of-4v-nsexpr-vars-sparse
  (sbitsetp (4v-nsexpr-vars-sparse x)))

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

(defthm bitset-members-4v-sexpr-vars-list-mask-sparse
  (sbitsetp (4v-sexpr-vars-list-mask-sparse x)))

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

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

Theorem: sbitset-members-4v-nsexpr-vars-sparse

(defthm sbitset-members-4v-nsexpr-vars-sparse
  (implies (4v-nsexpr-p x)
           (equal (sbitset-members (4v-nsexpr-vars-sparse x))
                  (4v-sexpr-vars x))))

Theorem: sbitset-members-4v-sexpr-vars-list-mask-sparse

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