		Search-engine friendly clone of the ACL2 documentation.

Faig-constructors

T-aig-iff

(t-aig-iff a b) iffs together the FAIGs a and b, assuming they cannot evaluate to Z.

Signature
(t-aig-iff a b) → *

Definitions and Theorems

Function: t-aig-iff

(defun t-aig-iff (a b)
  (declare (xargs :guard t))
  (let ((__function__ 't-aig-iff))
    (declare (ignorable __function__))
    (t-aig-or (t-aig-and a b)
              (t-aig-and (t-aig-not a)
                         (t-aig-not b)))))

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

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

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

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

Theorem: faig-fix-equiv-implies-equal-t-aig-iff-2

(defthm faig-fix-equiv-implies-equal-t-aig-iff-2
  (implies (faig-fix-equiv b b-equiv)
           (equal (t-aig-iff a b)
                  (t-aig-iff a b-equiv)))
  :rule-classes (:congruence))

Theorem: faig-equiv-implies-faig-equiv-t-aig-iff-2

(defthm faig-equiv-implies-faig-equiv-t-aig-iff-2
  (implies (faig-equiv b b-equiv)
           (faig-equiv (t-aig-iff a b)
                       (t-aig-iff a b-equiv)))
  :rule-classes (:congruence))

Theorem: faig-equiv-implies-faig-equiv-t-aig-iff-1

(defthm faig-equiv-implies-faig-equiv-t-aig-iff-1
  (implies (faig-equiv a a-equiv)
           (faig-equiv (t-aig-iff a b)
                       (t-aig-iff a-equiv b)))
  :rule-classes (:congruence))