---

Step * of Lemma pv11_p1_inc_acc

∀Cmd:ValueAllType. ∀ldrs_uid:Id ─→ ℤ. ∀mf:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(mf)). ∀e1,e2:E.
∀zh,z:pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List).
  ((e1 <loc e2)
  ⇒ zh ∈ pv11_p1_AcceptorState(Cmd;ldrs_uid;mf)(e1)
  ⇒ z ∈ pv11_p1_AcceptorState(Cmd;ldrs_uid;mf)(e2)
  ⇒ let ballot_num1,accepted1 = zh 
     in let ballot_num2,accepted2 = z 
        in (↑(pv11_p1_leq_bnum(ldrs_uid) ballot_num1 ballot_num2)) ∧ accepted1 ≤ accepted2)
BY
{ MemoryOrdering }

---

Latex:

---

Latex:
\mforall{}Cmd:ValueAllType.  \mforall{}ldrs$_{uid}$:Id  {}\mrightarrow{}  \mBbbZ{}.  \mforall{}mf:pv11\_p1\_headers\_type\{i:l\}(Cmd).  \mforall{}e\000Cs:EO+(Message(mf)).
\mforall{}e1,e2:E.  \mforall{}zh,z:pv11\_p1\_Ballot\_Num()  \mtimes{}  ((pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List).
    ((e1  <loc  e2)
    {}\mRightarrow{}  zh  \mmember{}  pv11\_p1\_AcceptorState(Cmd;ldrs$_{uid}$;mf)(e1)
    {}\mRightarrow{}  z  \mmember{}  pv11\_p1\_AcceptorState(Cmd;ldrs$_{uid}$;mf)(e2)
    {}\mRightarrow{}  let  ballot$_{num1}$,accepted1  =  zh 
          in  let  ballot$_{num2}$,accepted2  =  z 
                in  (\muparrow{}(pv11\_p1\_leq\_bnum(ldrs$_{uid}$)  ballot$_{num1}$\000C  ballot$_{num2}$))  \mwedge{}  accepted1  \mleq{}  accepted2)


By

---

Latex:
MemoryOrdering

---

Home Index