---

Step * of Lemma pv11_p1_ord_scout

∀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(). ∀zo,z:bag(Id) × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List).
  ((e1 <loc e2)
  ⇒ zo ∈ pv11_p1_ScoutState(Cmd;accpts;mf) b(e1)
  ⇒ z ∈ pv11_p1_ScoutState(Cmd;accpts;mf) b(e2)
  ⇒ let waitfor1,pvalues1 = zo 
     in let waitfor2,pvalues2 = z 
        in sub-bag(Id;waitfor2;waitfor1) ∧ pvalues1 ⊆ pvalues2)
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{}zo,z:bag(Id)  \mtimes{}  ((pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List).
    ((e1  <loc  e2)
    {}\mRightarrow{}  zo  \mmember{}  pv11\_p1\_ScoutState(Cmd;accpts;mf)  b(e1)
    {}\mRightarrow{}  z  \mmember{}  pv11\_p1\_ScoutState(Cmd;accpts;mf)  b(e2)
    {}\mRightarrow{}  let  waitfor1,pvalues1  =  zo 
          in  let  waitfor2,pvalues2  =  z 
                in  sub-bag(Id;waitfor2;waitfor1)  \mwedge{}  pvalues1  \msubseteq{}  pvalues2)


By

---

Latex:
MemoryOrdering

---

Home Index