Function vstd::multiset::axiom_multiset_new_not_contained

source · 
pub broadcast proof fn axiom_multiset_new_not_contained<V>(m: Map<V, nat>, v: V)
Expand description
requires
m.dom().finite(),
!m.dom().contains(v),
ensures
#[trigger] Multiset::from_map(m).count(v) == 0,

A call to Multiset::new with input map m will return a multiset that maps value v to multiplicity 0 if v is not in the domain of m.