Do a list of FAIGs always evaluate to purely Boolean values, i.e., are they never X or Z?
(faig-purebool-list-p x) → std::bool
This is a logically nice, but non-executable way to express pure Boolean-ness. See also faig-purebool-list-check, which can be executed; it uses a SAT solver to answer the question.
Function:
(defun faig-purebool-list-p (x) (declare (xargs :guard t)) (let ((__function__ 'faig-purebool-list-p)) (declare (ignorable __function__)) (if (consp x) (and (faig-purebool-p (car x)) (faig-purebool-list-p (cdr x))) t)))