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.