Function vstd::pcm::frame_preserving_updateCopy item path

pub open spec fn frame_preserving_update<P: PCM>(a: P, b: P) -> bool

{ forall |c| P::op(a, c).valid() ==> P::op(b, c).valid() }