law insertion_same

bend-collections-laws-math@1.0.0.0 · proofs/lib/lemmas/proofs/map_insert.bend:163

import Base

163# This actual native insertion law needs no well-formedness assumption: querying
164# the new key follows the same bits used to choose its newly inserted leaf.
165# Other-key preservation DOES require valid discriminator/difference properties.
166law insertion_same:
167  for -V: Data
168  for +d: V
169  for m: Map<&2, V>
170  for +key: String
171  for +x: V
172  for +p: Nat
173  {lookup(V, d, Map.ins(&2, V, m, key, x, p), key) == x : V}