---

Step * of Lemma pv11_p1_inv_scout

∀Cmd:ValueAllType. ∀accpts:bag(Id). ∀mf:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(mf)). ∀e1:E.
∀b:pv11_p1_Ballot_Num(). ∀z:bag(Id) × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List).
  (z ∈ pv11_p1_ScoutState(Cmd;accpts;mf) b(e1) ⇒ let waitfor,pvalues = z in 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{}z:bag(Id)  \mtimes{}  ((pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List).
    (z  \mmember{}  pv11\_p1\_ScoutState(Cmd;accpts;mf)  b(e1)
    {}\mRightarrow{}  let  waitfor,pvalues  =  z 
          in  sub-bag(Id;waitfor;accpts))


By

---

Latex:
MemoryInvariant

---

Home Index