---

Step * of Lemma pv11_p1_ldr_ord

∀Cmd:ValueAllType. ∀ldrs_uid:Id ⟶ ℤ. ∀mf:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(mf)). ∀e1,e2:E.
∀zs,z:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List).
  ((e1 <loc e2)
  ⇒ zs ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;mf)(e1)
  ⇒ z ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;mf)(e2)
  ⇒ let bnum1,active1,proposals1 = zs in 
     let bnum2,active2,proposals2 = z in 
     ↑(pv11_p1_leq_bnum(ldrs_uid) bnum1 bnum2))
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{}zs,z:pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbB{}  \mtimes{}  ((\mBbbZ{}  \mtimes{}  Cmd)  List).
    ((e1  <loc  e2)
    {}\mRightarrow{}  zs  \mmember{}  pv11\_p1\_LeaderState(Cmd;ldrs$_{uid}$;mf)(e1)
    {}\mRightarrow{}  z  \mmember{}  pv11\_p1\_LeaderState(Cmd;ldrs$_{uid}$;mf)(e2)
    {}\mRightarrow{}  let  bnum1,active1,proposals1  =  zs  in 
          let  bnum2,active2,proposals2  =  z  in 
          \muparrow{}(pv11\_p1\_leq\_bnum(ldrs$_{uid}$)  bnum1  bnum2))


By

---

Latex:
MemoryOrdering

---

Home Index