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.