Function vstd::pcm::frame_preserving_update_nondeterministic

source · 
pub open spec fn frame_preserving_update_nondeterministic<P: PCM>(
    a: P,
    bs: Set<P>
) -> bool
Expand description
{
    forall |c| {
        P::op(a, c).valid()
            ==> exists |b| #[trigger] bs.contains(b) && P::op(b, c).valid()
    }
}