		Search-engine friendly clone of the ACL2 documentation.

Validation-information

Uid-equal

Signature
(uid-equal x y) → *
Arguments: x — Guard (uidp x).; y — Guard (uidp y).

Definitions and Theorems

Function: uid-equal$inline

(defun uid-equal$inline (x y)
  (declare (xargs :guard (and (uidp x) (uidp y))))
  (mbe :logic (uid-equiv x y)
       :exec (= (the unsigned-byte (uid->uid x))
                (the unsigned-byte (uid->uid y)))))

Theorem: uid-equal$inline-of-uid-fix-x

(defthm uid-equal$inline-of-uid-fix-x
  (equal (uid-equal$inline (uid-fix x) y)
         (uid-equal$inline x y)))

Theorem: uid-equal$inline-uid-equiv-congruence-on-x

(defthm uid-equal$inline-uid-equiv-congruence-on-x
  (implies (uid-equiv x x-equiv)
           (equal (uid-equal$inline x y)
                  (uid-equal$inline x-equiv y)))
  :rule-classes :congruence)

Theorem: uid-equal$inline-of-uid-fix-y

(defthm uid-equal$inline-of-uid-fix-y
  (equal (uid-equal$inline x (uid-fix y))
         (uid-equal$inline x y)))

Theorem: uid-equal$inline-uid-equiv-congruence-on-y

(defthm uid-equal$inline-uid-equiv-congruence-on-y
  (implies (uid-equiv y y-equiv)
           (equal (uid-equal$inline x y)
                  (uid-equal$inline x y-equiv)))
  :rule-classes :congruence)