Skip to main content

axiom_fresh_segment_id_not_in_dom

ostd::specs::mm::embedding

Function axiom_fresh_segment_id_not_in_dom 

Source 
pub proof fn axiom_fresh_segment_id_not_in_dom(m: Map<SegmentId, SegmentEntry>)
Expand description
ensures
!m.dom().contains(fresh_segment_id(m)),