		Search-engine friendly clone of the ACL2 documentation.

Omaps

Rlookup*

Set of keys to which any value in a set is associated.

Signature
(rlookup* vals map) → keys
Arguments: vals — Guard (setp vals).; map — Guard (mapp map).
Returns: keys — Type (setp keys).

This lifts rlookup* to sets of values.

Definitions and Theorems

Function: rlookup*

(defun rlookup* (vals map)
  (declare (xargs :guard (and (setp vals) (mapp map))))
  (let ((__function__ 'rlookup*))
    (declare (ignorable __function__))
    (cond ((set::emptyp vals) nil)
          (t (union (rlookup (set::head vals) map)
                    (rlookup* (set::tail vals) map))))))

Theorem: setp-of-rlookup*

(defthm setp-of-rlookup*
  (b* ((keys (rlookup* vals map)))
    (setp keys))
  :rule-classes :rewrite)

Theorem: rlookup*-when-left-emptyp

(defthm rlookup*-when-left-emptyp
  (implies (set::emptyp vals)
           (equal (rlookup* vals map) nil))
  :rule-classes (:rewrite :type-prescription))

Theorem: rlookup*-when-right-emptyp

(defthm rlookup*-when-right-emptyp
  (implies (emptyp map)
           (equal (rlookup* vals map) nil))
  :rule-classes (:rewrite :type-prescription))