		Search-engine friendly clone of the ACL2 documentation.

Std/osets

Double-containment

A strategy for proving sets are equal because they are subsets of one another.

Double containment can be a good way to prove that two sets are equal to one another.

Unfortunately, because this rule targets equal it can get quite expensive. You may sometimes wish to disable it to speed up your proofs, as directed by accumulated-persistence.

Definitions and Theorems

Theorem: double-containment

(defthm double-containment
        (implies (and (setp x) (setp y))
                 (equal (equal x y)
                        (and (subset x y) (subset y x))))
        :rule-classes ((:rewrite :backchain-limit-lst 1)))