Function vstd::storage_protocol::withdraws

source · 
pub open spec fn withdraws<K, V, P: Protocol<K, V>>(p1: P, p2: P, b2: Map<K, V>) -> bool
Expand description
{
    forall |q: P, t1: Map<K, V>| {
        P::rel(P::op(p1, q), t1)
            ==> exists |t2: Map<K, V>| {
                P::rel(P::op(p2, q), t2) && t2.dom().disjoint(b2.dom())
                    && t1 =~= t2.union_prefer_right(b2)
            }
    }
}