		Search-engine friendly clone of the ACL2 documentation.

4v-sexpr-purebool-p

4v-sexpr-purebool-list-p-to-faig-purebool-list-p

Main theorem showing that 4v-sexpr-purebool-list-p is equivalent to faig-purebool-list-p.

This is the main result that lets us develop an efficient, SAT-based way to check, all at once, the Boolean-ness of a list of 4v-sexprs.

Definitions and Theorems

Theorem: 4v-sexpr-purebool-list-p-to-faig-purebool-list-p

(defthm 4v-sexpr-purebool-list-p-to-faig-purebool-list-p
  (equal (4v-sexpr-purebool-list-p sexprs)
         (faig-purebool-list-p (sfaiglist sexprs))))