		Search-engine friendly clone of the ACL2 documentation.

Undocumented

Svex-alist-same-keys

This is a universal equivalence, introduced using def-universal-equiv.

Function: svex-alist-same-keys

(defun svex-alist-same-keys (x y)
       (and (set-equiv (svex-alist-keys x)
                       (svex-alist-keys y))))

Definitions and Theorems

Function: svex-alist-same-keys

(defun svex-alist-same-keys (x y)
       (and (set-equiv (svex-alist-keys x)
                       (svex-alist-keys y))))

Theorem: svex-alist-same-keys-is-an-equivalence

(defthm svex-alist-same-keys-is-an-equivalence
        (and (booleanp (svex-alist-same-keys x y))
             (svex-alist-same-keys x x)
             (implies (svex-alist-same-keys x y)
                      (svex-alist-same-keys y x))
             (implies (and (svex-alist-same-keys x y)
                           (svex-alist-same-keys y z))
                      (svex-alist-same-keys x z)))
        :rule-classes (:equivalence))