		Search-engine friendly clone of the ACL2 documentation.

Set-equiv

Equivalence up to sfix.

Signature
(set-equiv x y) → *
Arguments: x — Guard (setp x).; y — Guard (setp y).

Definitions and Theorems

Function: set-equiv$inline

(defun set-equiv$inline (x y)
  (declare (xargs :guard (and (setp x) (setp y))))
  (declare (xargs :type-prescription (booleanp (set-equiv x y))))
  (equal (sfix x) (sfix y)))

Theorem: set-equiv-is-an-equivalence

(defthm set-equiv-is-an-equivalence
  (and (booleanp (set-equiv x y))
       (set-equiv x x)
       (implies (set-equiv x y)
                (set-equiv y x))
       (implies (and (set-equiv x y) (set-equiv y z))
                (set-equiv x z)))
  :rule-classes (:equivalence))