		Search-engine friendly clone of the ACL2 documentation.

Faig-restrict

Faig-restrict-thms

Basic theorems about faig-restrict.

Definitions and Theorems

Theorem: faig-eval-of-faig-restrict

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

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

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

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

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

Theorem: faig-equiv-implies-faig-equiv-faig-restrict-1

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

Theorem: faig-restrict-faig-restrict

(defthm faig-restrict-faig-restrict
  (faig-equiv (faig-restrict (faig-restrict x al1)
                             al2)
              (faig-restrict x
                             (append (aig-restrict-alist al1 al2)
                                     al2))))