Function vstd::pcm::conjunct_shared

source · 
pub open spec fn conjunct_shared<P: PCM>(a: P, b: P, c: P) -> bool
Expand description
{ forall |p: P| p.valid() && incl(a, p) && incl(b, p) ==> #[trigger] incl(c, p) }