Numbered names in use.
A table keeps track of the numbered names “in use”. The table must be updated explicitly every time a new numbered name is used (e.g. introduced into the ACL2 world).
The table maps bases of numbered names
to non-empty sets (encoded as lists) of positive integers.
If