Function vstd::pcm_lib::lemma_pcm_properties
source · pub proof fn lemma_pcm_properties<P: PCM>()Expand description
ensures
forall |a: P, b: P| (#[trigger] P::op(a, b)).valid() ==> a.valid(),forall |a: P, b: P| (#[trigger] P::op(a, b)) == P::op(b, a),forall |a: P| (#[trigger] P::op(a, P::unit())) == a,P::valid(P::unit()),Provides four quantified facts about a partially commutative monoid: that it’s closed under inclusion, that it’s commutative, that it’s a monoid, and that its unit element is valid. Note that, to avoid trigger loops, it doesn’t provide associativity.