		Search-engine friendly clone of the ACL2 documentation.

Aig-partial-eval

Aig-partial-eval-thms

Definitions and Theorems

Theorem: aig-eval-of-aig-partial-eval

(defthm aig-eval-of-aig-partial-eval
  (equal (aig-eval (aig-partial-eval x al1) al2)
         (aig-eval x (append al1 al2))))

Theorem: aig-equiv-implies-aig-equiv-aig-partial-eval-1

(defthm aig-equiv-implies-aig-equiv-aig-partial-eval-1
  (implies (aig-equiv x x-equiv)
           (aig-equiv (aig-partial-eval x al)
                      (aig-partial-eval x-equiv al)))
  :rule-classes (:congruence))

Theorem: aig-partial-eval-aig-partial-eval

(defthm aig-partial-eval-aig-partial-eval
  (aig-equiv (aig-partial-eval (aig-partial-eval x al1)
                               al2)
             (aig-partial-eval x (append al1 al2))))

Theorem: alist-equiv-implies-equal-aig-partial-eval-2

(defthm alist-equiv-implies-equal-aig-partial-eval-2
  (implies (alist-equiv env env-equiv)
           (equal (aig-partial-eval x env)
                  (aig-partial-eval x env-equiv)))
  :rule-classes (:congruence))