An AIG that captures exactly when a list of FAIGs always evaluate to purely Boolean values.
(faig-purebool-list-aig x) → aig
This is useful mainly to implement faig-purebool-list-check.
Function:
(defun faig-purebool-list-aig (x) (declare (xargs :guard t)) (let ((__function__ 'faig-purebool-list-aig)) (declare (ignorable __function__)) (if (atom x) t (aig-and (faig-purebool-aig (car x)) (faig-purebool-list-aig (cdr x))))))
Theorem:
(defthm faig-purebool-list-p-as-aig-eval (equal (faig-purebool-list-p x) (aig-eval (faig-purebool-list-aig x) (faig-purebool-list-witness x))))
Theorem:
(defthm faig-purebool-list-p-monotonicity (implies (not (aig-eval (faig-purebool-list-aig x) env)) (not (aig-eval (faig-purebool-list-aig x) (faig-purebool-list-witness x)))))