		Search-engine friendly clone of the ACL2 documentation.

Faig-restrict-alist

Faig-restrict-alist-thms

Basic theorems about faig-restrict-alist.

Definitions and Theorems

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

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

Theorem: lookup-in-faig-restrict-alist

(defthm lookup-in-faig-restrict-alist
  (equal (hons-assoc-equal k (faig-restrict-alist x env))
         (and (hons-assoc-equal k x)
              (cons k
                    (faig-restrict (cdr (hons-assoc-equal k x))
                                   env)))))

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

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

Theorem: faig-eval-alist-of-faig-restrict-alist

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

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

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

Theorem: faig-restrict-alist-faig-restrict-alist

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

Theorem: alist-keys-faig-restrict-alist

(defthm alist-keys-faig-restrict-alist
  (equal (alist-keys (faig-restrict-alist al env))
         (alist-keys al)))