---

Step * of Lemma pv11_p1_inv_comm

∀Cmd:ValueAllType. ∀accpts:bag(Id). ∀mf:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(mf)). ∀e1:E.
∀b:pv11_p1_Ballot_Num(). ∀s:ℤ. ∀waitfor:bag(Id).
  (waitfor ∈ pv11_p1_CommanderState(Cmd;accpts;mf) b s(e1) ⇒ sub-bag(Id;waitfor;accpts))
BY
{ MemoryInvariant }

---

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:E.
\mforall{}b:pv11\_p1\_Ballot\_Num().  \mforall{}s:\mBbbZ{}.  \mforall{}waitfor:bag(Id).
    (waitfor  \mmember{}  pv11\_p1\_CommanderState(Cmd;accpts;mf)  b  s(e1)  {}\mRightarrow{}  sub-bag(Id;waitfor;accpts))


By

---

Latex:
MemoryInvariant

---

Home Index