Function vstd::multiset::axiom_multiset_sub

source ·

pub broadcast proof fn axiom_multiset_sub<V>(m1: Multiset<V>, m2: Multiset<V>, v: V)

Expand description

ensures

#[trigger] m1.sub(m2).count(v)
    == if m1.count(v) >= m2.count(v) { m1.count(v) - m2.count(v) } else { 0 },

The count of value v in the multiset m1.sub(m2) is equal to the difference between the count of v in m1 and m2 individually. However, the difference is cut off at 0 and cannot be negative.