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.