Function vstd::multiset::axiom_filter_count
source · pub broadcast proof fn axiom_filter_count<V>(m: Multiset<V>, f: FnSpec<(V,), bool>, v: V)Expand description
ensures
(#[trigger] m.filter(f).count(v)) == if f(v) { m.count(v) } else { 0 },For a given value v and boolean predicate f, if f(v) is true, then the count of v in
m.filter(f) is the same as the count of v in m. Otherwise, the count of v in m.filter(f) is 0.