• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
      • 4v-sexprs
        • 4v-sexpr-vars
          • 4v-sexpr-vars-1pass
          • 4v-nsexpr-vars
          • 4v-sexpr-vars-1pass-list-list
          • 4v-sexpr-vars-list-list
          • 4v-sexpr-vars-alists
          • 4v-sexpr-vars-alist
          • 4v-sexpr-vars-1pass-list
          • 4v-sexpr-vars-list
        • 4v-sexpr-eval
        • 4v-sexpr-to-faig
        • 4v-sexpr-restrict-with-rw
        • 4vs-constructors
        • 4v-sexpr-compose-with-rw
        • 4v-sexpr-restrict
        • 4v-sexpr-alist-extract
        • 4v-sexpr-compose
        • 4v-nsexpr-p
        • 4v-sexpr-purebool-p
        • 4v-sexpr-<=
        • Sfaig
        • Sexpr-equivs
        • 3v-syntax-sexprp
        • Sexpr-rewriting
        • 4v-sexpr-ind
        • 4v-alist-extract
      • 4v-monotonicity
      • 4v-operations
      • Why-4v-logic
      • 4v-<=
      • 4vp
      • 4vcases
      • 4v-fix
      • 4v-lookup
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• 4v-sexpr-vars

4v-sexpr-vars-list-list

Extension of 4v-sexpr-vars to a list of sexpr lists.

Definitions and Theorems

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

(defun 4v-sexpr-vars-list-list (x)
 (declare (xargs :guard t))
 (if (atom x)
     nil
  (mbe
   :logic (set::union (4v-sexpr-vars-list (car x))
                      (4v-sexpr-vars-list-list (cdr x)))
   :exec (hons-alphorder-merge (4v-sexpr-vars-list (car x))
                               (4v-sexpr-vars-list-list (cdr x))))))

Theorem: atom-listp-of-4v-sexpr-vars-list-list

(defthm atom-listp-of-4v-sexpr-vars-list-list
  (atom-listp (4v-sexpr-vars-list-list x)))

Theorem: setp-of-4v-sexpr-vars-list-list

(defthm setp-of-4v-sexpr-vars-list-list
  (set::setp (4v-sexpr-vars-list-list x)))