---

Step * of Lemma pv11_p1_ldr_pos

∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀ldrs_uid:Id ⟶ ℤ.
∀v:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List).
  (v ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e)
  ⇒ let bnum,active,proposals1 = v in 
     ↑(pv11_p1_leq_bnum(ldrs_uid) (pv11_p1_init_ballot_num() loc(e)) bnum))
BY
{ MemoryInvariant }

---

Latex:

---

Latex:
\mforall{}Cmd:ValueAllType.  \mforall{}f:pv11\_p1\_headers\_type\{i:l\}(Cmd).  \mforall{}es:EO+(Message(f)).  \mforall{}e:E.  \mforall{}ldrs$_\mbackslash{}ff7\000Cbuid}$:Id  {}\mrightarrow{}  \mBbbZ{}.
\mforall{}v:pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbB{}  \mtimes{}  ((\mBbbZ{}  \mtimes{}  Cmd)  List).
    (v  \mmember{}  pv11\_p1\_LeaderState(Cmd;ldrs$_{uid}$;f)(e)
    {}\mRightarrow{}  let  bnum,active,proposals1  =  v  in 
          \muparrow{}(pv11\_p1\_leq\_bnum(ldrs$_{uid}$)  (pv11\_p1\_init\_ballot\_num()  loc(e))  bnum))


By

---

Latex:
MemoryInvariant

---

Home Index