		Search-engine friendly clone of the ACL2 documentation.

True-set-equiv-relation

True-set-equiv

Signature
(true-set-equiv list1 list2) → p
Arguments: list1 — Guard (true-listp list1).; list2 — Guard (true-listp list2).
Returns: p — Type (booleanp p).

Definitions and Theorems

Function: true-set-equiv

(defun true-set-equiv (list1 list2)
  (declare (xargs :guard (and (true-listp list1)
                              (true-listp list2))))
  (let ((acl2::__function__ 'true-set-equiv))
    (declare (ignorable acl2::__function__))
    (if (equal (true-listp list1)
               (true-listp list2))
        (acl2::set-equiv list1 list2)
      nil)))

Theorem: booleanp-of-true-set-equiv

(defthm booleanp-of-true-set-equiv
  (b* ((p (true-set-equiv list1 list2)))
    (booleanp p))
  :rule-classes :rewrite)

Theorem: set-equiv-if-true-set-equiv

(defthm set-equiv-if-true-set-equiv
  (b* ((p (true-set-equiv list1 list2)))
    (implies p (acl2::set-equiv list1 list2)))
  :rule-classes :rewrite)

Theorem: subsetp-if-true-set-equiv

(defthm subsetp-if-true-set-equiv
  (b* ((p (true-set-equiv list1 list2)))
    (implies p
             (and (subsetp list1 list2 :test 'equal)
                  (subsetp list2 list1 :test 'equal))))
  :rule-classes :rewrite)

Theorem: true-set-equiv-is-for-true-lists

(defthm true-set-equiv-is-for-true-lists
  (b* ((p (true-set-equiv list1 list2)))
    (implies p
             (equal (true-listp list1)
                    (true-listp list2))))
  :rule-classes :rewrite)