		Search-engine friendly clone of the ACL2 documentation.

Faig-compose

Faig-compose-thms

Basic theorems about faig-compose.

Definitions and Theorems

Theorem: faig-eval-of-faig-compose

(defthm faig-eval-of-faig-compose
  (equal (faig-eval (faig-compose x al1) al2)
         (faig-eval x (aig-eval-alist al1 al2))))

Theorem: faig-equiv-implies-faig-equiv-faig-compose-1

(defthm faig-equiv-implies-faig-equiv-faig-compose-1
  (implies (faig-equiv x x-equiv)
           (faig-equiv (faig-compose x al)
                       (faig-compose x-equiv al)))
  :rule-classes (:congruence))

Theorem: aig-alist-equiv-implies-faig-equiv-faig-compose-2

(defthm aig-alist-equiv-implies-faig-equiv-faig-compose-2
  (implies (aig-alist-equiv al al-equiv)
           (faig-equiv (faig-compose x al)
                       (faig-compose x al-equiv)))
  :rule-classes (:congruence))

Theorem: alist-equiv-implies-equal-faig-compose-2

(defthm alist-equiv-implies-equal-faig-compose-2
  (implies (alist-equiv env env-equiv)
           (equal (faig-compose x env)
                  (faig-compose x env-equiv)))
  :rule-classes (:congruence))