Function vstd::pcm::frame_preserving_update_nondeterministic

pub open spec fn frame_preserving_update_nondeterministic<P: PCM>(
    a: P,
    bs: Set<P>
) -> bool