Basic list-equiv congruence theorems for built-in functions.
Theorem:
(defthm list-equiv-implies-equal-list-fix-1 (implies (list-equiv x x-equiv) (equal (list-fix x) (list-fix x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm list-equiv-implies-equal-car-1 (implies (list-equiv x x-equiv) (equal (car x) (car x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm list-equiv-implies-list-equiv-cdr-1 (implies (list-equiv x x-equiv) (list-equiv (cdr x) (cdr x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm list-equiv-implies-list-equiv-cons-2 (implies (list-equiv y y-equiv) (list-equiv (cons x y) (cons x y-equiv))) :rule-classes (:congruence))
Theorem:
(defthm list-equiv-implies-equal-nth-2 (implies (list-equiv x x-equiv) (equal (nth n x) (nth n x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm list-equiv-implies-list-equiv-nthcdr-2 (implies (list-equiv x x-equiv) (list-equiv (nthcdr n x) (nthcdr n x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm list-equiv-implies-list-equiv-update-nth-3 (implies (list-equiv x x-equiv) (list-equiv (update-nth n v x) (update-nth n v x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm list-equiv-implies-equal-consp-1 (implies (list-equiv x x-equiv) (equal (consp x) (consp x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm list-equiv-implies-equal-len-1 (implies (list-equiv x x-equiv) (equal (len x) (len x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm list-equiv-implies-equal-append-1 (implies (list-equiv x x-equiv) (equal (append x y) (append x-equiv y))) :rule-classes (:congruence))
Theorem:
(defthm list-equiv-implies-list-equiv-append-2 (implies (list-equiv y y-equiv) (list-equiv (append x y) (append x y-equiv))) :rule-classes (:congruence))
Theorem:
(defthm list-equiv-implies-list-equiv-member-2 (implies (list-equiv x x-equiv) (list-equiv (member k x) (member k x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm list-equiv-implies-iff-member-2 (implies (list-equiv x x-equiv) (iff (member k x) (member k x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm list-equiv-implies-equal-subsetp-1 (implies (list-equiv x x-equiv) (equal (subsetp x y) (subsetp x-equiv y))) :rule-classes (:congruence))
Theorem:
(defthm list-equiv-implies-equal-subsetp-2 (implies (list-equiv y y-equiv) (equal (subsetp x y) (subsetp x y-equiv))) :rule-classes (:congruence))
Theorem:
(defthm list-equiv-implies-equal-remove-2 (implies (list-equiv x x-equiv) (equal (remove a x) (remove a x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm list-equiv-implies-equal-resize-list-1 (implies (list-equiv lst lst-equiv) (equal (resize-list lst n default) (resize-list lst-equiv n default))) :rule-classes (:congruence))
Theorem:
(defthm list-equiv-implies-equal-revappend-1 (implies (list-equiv x x-equiv) (equal (revappend x y) (revappend x-equiv y))) :rule-classes (:congruence))
Theorem:
(defthm list-equiv-implies-list-equiv-revappend-2 (implies (list-equiv y y-equiv) (list-equiv (revappend x y) (revappend x y-equiv))) :rule-classes (:congruence))
Theorem:
(defthm list-equiv-implies-list-equiv-last-1 (implies (list-equiv x x-equiv) (list-equiv (last x) (last x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm list-equiv-implies-list-equiv-make-list-ac-3 (implies (list-equiv ac ac-equiv) (list-equiv (make-list-ac n val ac) (make-list-ac n val ac-equiv))) :rule-classes (:congruence))
Theorem:
(defthm list-equiv-implies-equal-no-duplicatesp-equal-1 (implies (list-equiv x x-equiv) (equal (no-duplicatesp-equal x) (no-duplicatesp-equal x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm list-equiv-implies-equal-string-append-lst-1 (implies (list-equiv x x-equiv) (equal (string-append-lst x) (string-append-lst x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm list-equiv-implies-equal-assoc-equal-2 (implies (list-equiv l l-equiv) (equal (assoc-equal x l) (assoc-equal x l-equiv))) :rule-classes (:congruence))
Theorem:
(defthm list-equiv-implies-equal-strip-cars-1 (implies (list-equiv x x-equiv) (equal (strip-cars x) (strip-cars x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm list-equiv-implies-equal-remove-assoc-equal-2 (implies (list-equiv l l-equiv) (equal (remove-assoc-equal x l) (remove-assoc-equal x l-equiv))) :rule-classes (:congruence))
Theorem:
(defthm list-equiv-implies-list-equiv-put-assoc-equal-3 (implies (list-equiv alist alist-equiv) (list-equiv (put-assoc-equal name val alist) (put-assoc-equal name val alist-equiv))) :rule-classes (:congruence))