grogers0

FiniteSeq(S) == UNION {[1..n -> S] : n \in 1..Cardinality(S)}
SeqAsSet(S) == {S[i] : i \in DOMAIN S}

HistoryIsLinearizable == \E order \in {<<>>} \union FiniteSeq(Timestamps) :
    /\ \A H \in SeqAsSet(history) : H.type = "response" => H.ts \in SeqAsSet(order)
    /\ \A H1_i, H2_i \in DOMAIN history :
        (history[H1_i].type = "response" /\ history[H2_i].type = "invoke" /\ H1_i < H2_i) =>
            (
                history[H2_i].ts \in SeqAsSet(order) =>
                    \E i1, i2 \in DOMAIN order :