Note that the @@ operator is "left-biased", so mappings on the left side take precedence over mappings on the right. That's why dictionary[10] /= "c".
(Also, a quick pedantic note, probably irrelevant to what you're trying to do: a
hash map is a specific data structure that implements a dictionary on real hardware. TLA+ is not a programming language and it does not have hash maps. It has
functions, which are mathematical objects that behave like dictionaries. Functions have a
domain that acts like a dictionary's keys, and they map each element in their domain to a value in their range, just like how a dictionary maps each key to a value. You can read more about functions in Section 5.2 of
Specifying Systems. Internally, TLC actually does
not use hash maps to implement
functions, so you should not expect functions to have the same
performance characteristics as hash maps during model checking.)