		Search-engine friendly clone of the ACL2 documentation.

Double-containment

Prove set equalities via subset antisymmetry.

This mirrors the ACL2::std/osets rule, set::double-containment. Here, we disable it by default.

The proof of antisymmetry is nontrivial. The intuition is that for an arbitrary nonempty set, the root of the tree is necessarily the maximum element with respect to heap<. Then which of the remaining elements are in the left and right subtrees is determined by the binary search tree property. This reasoning requires and induction over the tree structure of both sets simultaneously.

Definitions and Theorems

Theorem: equal-becomes-subset-when-setp

(defthm equal-becomes-subset-when-setp
  (implies (and (setp x) (setp y))
           (equal (equal x y)
                  (and (subset x y) (subset y x)))))

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