Skip to main content

lemma_fresh_vm_space_id_not_in_dom

ostd::specs::mm::embedding

Function lemma_fresh_vm_space_id_not_in_dom 

Source 
pub proof fn lemma_fresh_vm_space_id_not_in_dom<'a>(m: Map<VmSpaceId, VmSpaceOwner>)
Expand description
ensures
!m.contains_key(fresh_vm_space_id(m)),