• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
    • Std/lists
    • Omaps
    • Std/alists
      • Alist-keys
      • Remove-assocs
      • Alist-vals
      • Alist-map-vals
      • Alist-map-keys
      • Std/alists/strip-cdrs
      • Hons-rassoc-equal
      • Std/alists/hons-assoc-equal
      • Std/alists/strip-cars
      • Fal-find-any
      • Fal-extract
      • Std/alists/abstract
      • Fal-extract-vals
      • Fal-all-boundp
      • Std/alists/alistp
      • Append-alist-vals
      • Append-alist-keys
      • Alist-equiv
        • Basic-alist-equiv-congruences
        • Alist-equiv-bad-guy
      • Hons-remove-assoc
      • Std/alists/pairlis$
      • Worth-hashing
      • Alists-agree
      • Sub-alistp
      • Alist-fix
      • Std/alists/remove-assoc-equal
      • Std/alists/assoc-equal
    • Obags
    • Std/util
    • Std/strings
    • Std/osets
    • Std/io
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Alist-equiv

Basic-alist-equiv-congruences

Some congruence rules about alist-equiv for basic alist functions.

Definitions and Theorems

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

(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: alist-equiv-implies-equal-alists-agree-2

(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: alist-equiv-implies-equal-alists-agree-3

(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: alist-equiv-implies-equal-sub-alistp-1

(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: alist-equiv-implies-equal-sub-alistp-2

(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: set-equiv-implies-set-equiv-alist-keys-1

(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: set-equiv-implies-set-equiv-alist-vals-1

(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: alist-equiv-implies-set-equiv-alist-keys-1

(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: alist-equiv-implies-alist-equiv-cons-2

(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: alist-equiv-implies-alist-equiv-append-1

(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: alist-equiv-implies-alist-equiv-append-2

(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))