Set of keys to which a value is associated.
The resulting set is empty if the value is not in the omap. The resulting set is a singleton if the value is associated to exactly one key. Otherwise, the resulting set contains two or more keys.
This is the ``reverse'' of lookup,
which motivates the
(defun rlookup (val map) (declare (xargs :guard (mapp map))) (let ((__function__ 'rlookup)) (declare (ignorable __function__)) (cond ((empty map) nil) (t (mv-let (key0 val0) (head map) (if (equal val val0) (insert key0 (rlookup val (tail map))) (rlookup val (tail map))))))))
(defthm setp-of-rlookup (b* ((keys (rlookup val map))) (setp keys)) :rule-classes :rewrite)
(defthm rlookup-when-empty (implies (empty map) (equal (rlookup val map) nil)) :rule-classes (:rewrite :type-prescription))