---

Step * of Lemma pv11_p1_ord_comm

∀Cmd:ValueAllType. ∀accpts:bag(Id). ∀mf:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(mf)). ∀e1,e2:E.
∀b:pv11_p1_Ballot_Num(). ∀s:ℤ. ∀waitfor1,waitfor2:bag(Id).
  ((e1 <loc e2)
  ⇒ waitfor1 ∈ pv11_p1_CommanderState(Cmd;accpts;mf) b s(e1)
  ⇒ waitfor2 ∈ pv11_p1_CommanderState(Cmd;accpts;mf) b s(e2)
  ⇒ sub-bag(Id;waitfor2;waitfor1))
BY
{ MemoryOrdering }

---

Latex:

---

Latex:
\mforall{}Cmd:ValueAllType.  \mforall{}accpts:bag(Id).  \mforall{}mf:pv11\_p1\_headers\_type\{i:l\}(Cmd).  \mforall{}es:EO+(Message(mf)).
\mforall{}e1,e2:E.  \mforall{}b:pv11\_p1\_Ballot\_Num().  \mforall{}s:\mBbbZ{}.  \mforall{}waitfor1,waitfor2:bag(Id).
    ((e1  <loc  e2)
    {}\mRightarrow{}  waitfor1  \mmember{}  pv11\_p1\_CommanderState(Cmd;accpts;mf)  b  s(e1)
    {}\mRightarrow{}  waitfor2  \mmember{}  pv11\_p1\_CommanderState(Cmd;accpts;mf)  b  s(e2)
    {}\mRightarrow{}  sub-bag(Id;waitfor2;waitfor1))


By

---

Latex:
MemoryOrdering

---

Home Index