		Search-engine friendly clone of the ACL2 documentation.

Validation-information

Uid-increment

Create a fresh unique identifier.

Signature
(uid-increment uid) → new-uid
Arguments: uid — Guard (uidp uid).
Returns: new-uid — Type (uidp new-uid).

This simply increments the numerical value of the unique identifier.

Definitions and Theorems

Function: uid-increment

(defun uid-increment (uid)
  (declare (xargs :guard (uidp uid)))
  (b* (((uid uid) uid))
    (uid (1+ uid.uid))))

Theorem: uidp-of-uid-increment

(defthm uidp-of-uid-increment
  (b* ((new-uid (uid-increment uid)))
    (uidp new-uid))
  :rule-classes :rewrite)

Theorem: uid-increment-of-uid-fix-uid

(defthm uid-increment-of-uid-fix-uid
  (equal (uid-increment (uid-fix uid))
         (uid-increment uid)))

Theorem: uid-increment-uid-equiv-congruence-on-uid

(defthm uid-increment-uid-equiv-congruence-on-uid
  (implies (uid-equiv uid uid-equiv)
           (equal (uid-increment uid)
                  (uid-increment uid-equiv)))
  :rule-classes :congruence)