Some congruence rules about alist-equiv for basic alist functions.
Theorem:
(defthm alist-equiv-implies-equal-hons-assoc-equal-2 (implies (alist-equiv a a-equiv) (equal (hons-assoc-equal x a) (hons-assoc-equal x a-equiv))) :rule-classes (:congruence))
Theorem:
(defthm alist-equiv-implies-equal-alists-agree-2 (implies (alist-equiv a a-equiv) (equal (alists-agree keys a b) (alists-agree keys a-equiv b))) :rule-classes (:congruence))
Theorem:
(defthm alist-equiv-implies-equal-alists-agree-3 (implies (alist-equiv b b-equiv) (equal (alists-agree keys a b) (alists-agree keys a b-equiv))) :rule-classes (:congruence))
Theorem:
(defthm alist-equiv-implies-equal-sub-alistp-1 (implies (alist-equiv x x-equiv) (equal (sub-alistp x y) (sub-alistp x-equiv y))) :rule-classes (:congruence))
Theorem:
(defthm alist-equiv-implies-equal-sub-alistp-2 (implies (alist-equiv y y-equiv) (equal (sub-alistp x y) (sub-alistp x y-equiv))) :rule-classes (:congruence))
Theorem:
(defthm set-equiv-implies-set-equiv-alist-keys-1 (implies (set-equiv x x-equiv) (set-equiv (alist-keys x) (alist-keys x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm set-equiv-implies-set-equiv-alist-vals-1 (implies (set-equiv x x-equiv) (set-equiv (alist-vals x) (alist-vals x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm alist-equiv-implies-set-equiv-alist-keys-1 (implies (alist-equiv x x-equiv) (set-equiv (alist-keys x) (alist-keys x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm alist-equiv-implies-alist-equiv-cons-2 (implies (alist-equiv b b-equiv) (alist-equiv (cons a b) (cons a b-equiv))) :rule-classes (:congruence))
Theorem:
(defthm alist-equiv-implies-alist-equiv-append-1 (implies (alist-equiv a a-equiv) (alist-equiv (append a b) (append a-equiv b))) :rule-classes (:congruence))
Theorem:
(defthm alist-equiv-implies-alist-equiv-append-2 (implies (alist-equiv b b-equiv) (alist-equiv (append a b) (append a b-equiv))) :rule-classes (:congruence))