		Search-engine friendly clone of the ACL2 documentation.

Faig-equiv

Faig-equiv-thms

Basic theorems about faig-equiv.

Definitions and Theorems

Theorem: aig-equiv-implies-faig-equiv-cons-1

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

Theorem: aig-equiv-implies-faig-equiv-cons-2

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