		Search-engine friendly clone of the ACL2 documentation.

Faig-partial-eval

Faig-partial-eval-thms

Definitions and Theorems

Theorem: faig-eval-of-faig-partial-eval

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

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

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

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

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

Theorem: faig-partial-eval-faig-partial-eval

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