		Search-engine friendly clone of the ACL2 documentation.

Faig-constructors

F-aig-xor

(f-aig-xor a b) xors together the FAIGs a and b.

Signature
(f-aig-xor a b) → *

Definitions and Theorems

Function: f-aig-xor

(defun f-aig-xor (a b)
  (declare (xargs :guard t))
  (let ((__function__ 'f-aig-xor))
    (declare (ignorable __function__))
    (b* ((a (f-aig-unfloat a))
         (b (f-aig-unfloat b)))
      (t-aig-xor a b))))

Theorem: faig-eval-of-f-aig-xor

(defthm faig-eval-of-f-aig-xor
  (equal (faig-eval (f-aig-xor a b) env)
         (f-aig-xor (faig-eval a env)
                    (faig-eval b env))))

Theorem: faig-fix-equiv-implies-equal-f-aig-xor-1

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

Theorem: faig-fix-equiv-implies-equal-f-aig-xor-2

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

Theorem: faig-equiv-implies-faig-equiv-f-aig-xor-2

(defthm faig-equiv-implies-faig-equiv-f-aig-xor-2
  (implies (faig-equiv b b-equiv)
           (faig-equiv (f-aig-xor a b)
                       (f-aig-xor a b-equiv)))
  :rule-classes (:congruence))

Theorem: faig-equiv-implies-faig-equiv-f-aig-xor-1

(defthm faig-equiv-implies-faig-equiv-f-aig-xor-1
  (implies (faig-equiv a a-equiv)
           (faig-equiv (f-aig-xor a b)
                       (f-aig-xor a-equiv b)))
  :rule-classes (:congruence))