Function vstd::map_lib::lemma_disjoint_union_size

source · 
pub proof fn lemma_disjoint_union_size<K, V>(m1: Map<K, V>, m2: Map<K, V>)
Expand description
requires
m1.dom().disjoint(m2.dom()),
m1.dom().finite(),
m2.dom().finite(),
ensures
m1.union_prefer_right(m2).dom().len() == m1.dom().len() + m2.dom().len(),

The size of the union of two disjoint maps is equal to the sum of the sizes of the individual maps