Assumed properties of finite maps
If two finite maps are equal at one key, they are still equal at that key after an update:
∀
fm
1
fm
2
k k' v .
{lookup
fm
1
k} === {lookup
fm
2
k} ==>
{lookup (update k' v
fm
1
) k}
=== {lookup (update k' v
fm
2
) k}
Updating a key doesn't change the values associated with other keys:
∀ fm k k' v .
True {k /= k'} ==>
{lookup k (update k' v fm)} === {lookup k fm}
This is elegantly captured as a record type in Alfa (see file FiniteMaps2.alfa)...