		Search-engine friendly clone of the ACL2 documentation.

Faig-alist-equiv

Faig-alist-equiv-thms

Definitions and Theorems

Theorem: faig-alist-equiv-implies-iff-hons-assoc-equal-2

(defthm faig-alist-equiv-implies-iff-hons-assoc-equal-2
  (implies (faig-alist-equiv al al-equiv)
           (iff (hons-assoc-equal x al)
                (hons-assoc-equal x al-equiv)))
  :rule-classes (:congruence))

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

(defthm faig-alist-equiv-implies-faig-alist-equiv-append-1
  (implies (faig-alist-equiv a a-equiv)
           (faig-alist-equiv (append a b)
                             (append a-equiv b)))
  :rule-classes (:congruence))

Theorem: faig-alist-equiv-implies-faig-alist-equiv-append-2

(defthm faig-alist-equiv-implies-faig-alist-equiv-append-2
  (implies (faig-alist-equiv b b-equiv)
           (faig-alist-equiv (append a b)
                             (append a b-equiv)))
  :rule-classes (:congruence))