Function vstd::storage_protocol::updates

source · 
pub open spec fn updates<K, V, P: Protocol<K, V>>(p1: P, p2: P) -> bool
Expand description
{ forall |q: P, t1: Map<K, V>| P::rel(P::op(p1, q), t1) ==> P::rel(P::op(p2, q), t1) }