		Search-engine friendly clone of the ACL2 documentation.

4v-sexpr-to-faig

Faig-const-p

Recognizer for constant faigs.

Signature
(faig-const-p x) → *

(faig-const-p x) recognizes conses whose car/cdr are Booleans, i.e., the four possible constant FAIGs.

This is the FAIG equivalent of 4vp

Definitions and Theorems

Function: faig-const-p

(defun faig-const-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'faig-const-p))
    (declare (ignorable __function__))
    (and (consp x)
         (booleanp (car x))
         (booleanp (cdr x)))))

Theorem: faig-const-p-of-faig-eval

(defthm faig-const-p-of-faig-eval
  (faig-const-p (faig-eval x env)))