Skip to main content

lemma_wf_union

ostd::specs::mm::page_table::mapping_set_lemmas

Function lemma_wf_union 

Source 
pub proof fn lemma_wf_union(a: Set<Mapping>, b: Set<Mapping>)
Expand description
requires
wf_mapping_set(a),
wf_mapping_set(b),
forall |m: Mapping, n: Mapping| {
    #[trigger] a.contains(m) && #[trigger] b.contains(n)
        ==> m.va_range.end <= n.va_range.start || n.va_range.end <= m.va_range.start
},
ensures
wf_mapping_set(a.union(b)),

A union of two wf sets is wf if every element of one is VA-disjoint from every element of the other.