---

Step * of Lemma pv11_p1_ldr_loc_bnum

∀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,proposals = v in 
     ∃n:ℤ. (bnum = (pv11_p1_mk_bnum() n loc(e)) ∈ pv11_p1_Ballot_Num()))
BY
{ (MemoryInvariant
   THEN (ExRepD
         THEN RepUR ``pv11_p1_upd_bnum pv11_p1_mk_bnum pv11_p1_init_ballot_num pv11_p1_Ballot_Num`` 0
         THEN RW SimplifyC 0
         THEN Auto)⋅
   ) }

---

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,proposals  =  v  in 
          \mexists{}n:\mBbbZ{}.  (bnum  =  (pv11\_p1\_mk\_bnum()  n  loc(e))))


By

---

Latex:
(MemoryInvariant
  THEN  (ExRepD
              THEN  RepUR  ``pv11\_p1\_upd\_bnum  pv11\_p1\_mk\_bnum  pv11\_p1\_init\_ballot\_num  pv11\_p1\_Ballot\_Num``  0
              THEN  RW  SimplifyC  0
              THEN  Auto)\mcdot{}
  )

---

Home Index