Skip to main content

lemma_fresh_frame_id_not_in_dom

ostd::specs::mm::embedding

Function lemma_fresh_frame_id_not_in_dom 

Source 
pub proof fn lemma_fresh_frame_id_not_in_dom(m: Map<FrameId, FrameEntry>)
Expand description
ensures
!m.dom().contains(fresh_frame_id(m)),