Skip to main content

axiom_fresh_frame_id_not_in_dom

ostd::specs::mm::embedding

Function axiom_fresh_frame_id_not_in_dom 

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