Function vstd::multiset::axiom_multiset_add

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

Expand description

ensures

#[trigger] m1.add(m2).count(v) == m1.count(v) + m2.count(v),

The count of value v in the multiset m1.add(m2) is equal to the sum of the counts of v in m1 and m2 individually.

Function vstd::multiset::axiom_multiset_addCopy item path