• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
    • Std/lists
      • Std/lists/abstract
      • Rev
      • Defsort
      • List-fix
      • Std/lists/nth
      • Hons-remove-duplicates
      • Std/lists/update-nth
      • Set-equiv
        • Set-equiv-congruences
        • Set-unequal-witness
      • Duplicity
      • Prefixp
      • Std/lists/take
      • Std/lists/intersection$
      • Nats-equiv
      • Repeat
      • Index-of
      • All-equalp
      • Sublistp
      • Std/lists/nthcdr
      • Std/lists/append
      • Listpos
      • List-equiv
      • Final-cdr
      • Std/lists/remove
      • Subseq-list
      • Rcons
      • Std/lists/revappend
      • Std/lists/remove-duplicates-equal
      • Std/lists/last
      • Std/lists/reverse
      • Std/lists/resize-list
      • Flatten
      • Suffixp
      • Std/lists/set-difference
      • Std/lists/butlast
      • Std/lists/len
      • Std/lists/intersectp
      • Std/lists/true-listp
      • Intersectp-witness
      • Subsetp-witness
      • Std/lists/remove1-equal
      • Rest-n
      • First-n
      • Std/lists/union
      • Append-without-guard
      • Std/lists/subsetp
      • Std/lists/member
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
    • Std/system
    • Std/basic
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
    • Std-extensions
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Set-equiv

Set-equiv-congruences

Basic congruence rules relating set-equiv to list functions.

Definitions and Theorems

Theorem: set-equiv-implies-iff-member-2

(defthm set-equiv-implies-iff-member-2
        (implies (set-equiv y y-equiv)
                 (iff (member x y) (member x y-equiv)))
        :rule-classes (:congruence))

Theorem: set-equiv-implies-equal-subsetp-2

(defthm set-equiv-implies-equal-subsetp-2
        (implies (set-equiv y y-equiv)
                 (equal (subsetp x y)
                        (subsetp x y-equiv)))
        :rule-classes (:congruence))

Theorem: set-equiv-implies-equal-subsetp-1

(defthm set-equiv-implies-equal-subsetp-1
        (implies (set-equiv x x-equiv)
                 (equal (subsetp x y)
                        (subsetp x-equiv y)))
        :rule-classes (:congruence))

Theorem: element-list-p-set-equiv-congruence

(defthm element-list-p-set-equiv-congruence
        (implies (and (element-list-final-cdr-p t)
                      (set-equiv x y))
                 (equal (equal (element-list-p x)
                               (element-list-p y))
                        t))
        :rule-classes :rewrite)

Theorem: set-equiv-implies-equal-intersection-equal-2

(defthm set-equiv-implies-equal-intersection-equal-2
        (implies (set-equiv y y-equiv)
                 (equal (intersection-equal x y)
                        (intersection-equal x y-equiv)))
        :rule-classes (:congruence))

Theorem: set-equiv-implies-set-equiv-intersection-equal-1

(defthm set-equiv-implies-set-equiv-intersection-equal-1
        (implies (set-equiv x x-equiv)
                 (set-equiv (intersection-equal x y)
                            (intersection-equal x-equiv y)))
        :rule-classes (:congruence))

Theorem: set-equiv-implies-equal-set-difference-equal-2

(defthm set-equiv-implies-equal-set-difference-equal-2
        (implies (set-equiv y y-equiv)
                 (equal (set-difference-equal x y)
                        (set-difference-equal x y-equiv)))
        :rule-classes (:congruence))

Theorem: set-equiv-implies-set-equiv-set-difference-equal-1

(defthm set-equiv-implies-set-equiv-set-difference-equal-1
        (implies (set-equiv x x-equiv)
                 (set-equiv (set-difference-equal x y)
                            (set-difference-equal x-equiv y)))
        :rule-classes (:congruence))

Theorem: set-equiv-implies-equal-consp-1

(defthm set-equiv-implies-equal-consp-1
        (implies (set-equiv x x-equiv)
                 (equal (consp x) (consp x-equiv)))
        :rule-classes (:congruence))

Theorem: set-equiv-implies-equal-atom-1

(defthm set-equiv-implies-equal-atom-1
        (implies (set-equiv x x-equiv)
                 (equal (atom x) (atom x-equiv)))
        :rule-classes (:congruence))

Theorem: set-equiv-implies-equal-intersectp-1

(defthm set-equiv-implies-equal-intersectp-1
        (implies (set-equiv x x-equiv)
                 (equal (intersectp x y)
                        (intersectp x-equiv y)))
        :rule-classes (:congruence))

Theorem: set-equiv-implies-equal-intersectp-2

(defthm set-equiv-implies-equal-intersectp-2
        (implies (set-equiv y y-equiv)
                 (equal (intersectp x y)
                        (intersectp x y-equiv)))
        :rule-classes (:congruence))

Theorem: set-equiv-implies-set-equiv-append-2

(defthm set-equiv-implies-set-equiv-append-2
        (implies (set-equiv y y-equiv)
                 (set-equiv (append x y)
                            (append x y-equiv)))
        :rule-classes (:congruence))

Theorem: set-equiv-implies-set-equiv-append-1

(defthm set-equiv-implies-set-equiv-append-1
        (implies (set-equiv x x-equiv)
                 (set-equiv (append x y)
                            (append x-equiv y)))
        :rule-classes (:congruence))

Theorem: set-equiv-implies-equal-len-remove-duplicates-equal

(defthm set-equiv-implies-equal-len-remove-duplicates-equal
        (implies (set-equiv x y)
                 (equal (len (remove-duplicates-equal x))
                        (len (remove-duplicates-equal y))))
        :rule-classes :congruence)