pub broadcast proof fn lemma_hashmap_deepview_properties<K: DeepView, V: DeepView>(
m: HashMap<K, V>,
)
Expand description
requires
crate::relations::injective(|k: K| k.deep_view()),
ensuresforall |k: K| (
#[trigger] m@.contains_key(k)
==> m.deep_view().contains_key(k.deep_view())
&& m.deep_view()[k.deep_view()] == m@[k].deep_view()
),
forall |dk: <K as DeepView>::V| {
#[trigger] m.deep_view().contains_key(dk)
==> exists |k: K| k.deep_view() == dk && #[trigger] m@.contains_key(k)
},