		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))))