		Search-engine friendly clone of the ACL2 documentation.

Faig-constructors

T-aig-xdet

(t-aig-xdet a) constructs an FAIG for 4v-xdet, assuming that the argument a cannot evaluate to Z.

Signature
(t-aig-xdet a) → *

Definitions and Theorems

Function: t-aig-xdet$inline

(defun t-aig-xdet$inline (a)
  (declare (xargs :guard t))
  (let ((__function__ 't-aig-xdet))
    (declare (ignorable __function__))
    (b* (((faig a1 a0) a))
      (cons (aig-and a1 a0) t))))

Theorem: faig-eval-of-t-aig-xdet

(defthm faig-eval-of-t-aig-xdet
  (equal (faig-eval (t-aig-xdet a) env)
         (t-aig-xdet (faig-eval a env))))

Theorem: faig-fix-equiv-implies-equal-t-aig-xdet-1

(defthm faig-fix-equiv-implies-equal-t-aig-xdet-1
  (implies (faig-fix-equiv a a-equiv)
           (equal (t-aig-xdet a)
                  (t-aig-xdet a-equiv)))
  :rule-classes (:congruence))