Function wf_mapping_set 

pub open spec fn wf_mapping_set(s: Set<Mapping>) -> bool

{
    &&& mappings_well_formed(s)
    &&& mappings_disjoint_vaddrs(s)

}

Well-formed mapping set: all inv(), pairwise VA-disjoint.