---

Step * of Lemma pv11_p1_inv_acc

∀Cmd:ValueAllType. ∀ldrs_uid:Id ⟶ ℤ. ∀mf:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(mf)). ∀e1:E.
∀z:pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List).
  (z ∈ pv11_p1_AcceptorState(Cmd;ldrs_uid;mf)(e1)
  ⇒ let ballot_num,accepted = z 
     in (∀bnum:pv11_p1_Ballot_Num(). ∀p:ℤ × Cmd.
           ((<bnum, p> ∈ accepted) ⇒ (↑(pv11_p1_leq_bnum(ldrs_uid) bnum ballot_num))))
        ∧ l-ordered(pv11_p1_Ballot_Num() × ℤ × Cmd;pv1,pv2.↑(pv11_p1_leq_bnum(ldrs_uid) (fst(pv1)) (fst(pv2)));accepted)
        ∧ no_repeats(pv11_p1_Ballot_Num() × ℤ × Cmd;accepted))
BY
{ MemoryInvariant }

---

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:E.  \mforall{}z:pv11\_p1\_Ballot\_Num()  \mtimes{}  ((pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List).
    (z  \mmember{}  pv11\_p1\_AcceptorState(Cmd;ldrs$_{uid}$;mf)(e1)
    {}\mRightarrow{}  let  ballot$_{num}$,accepted  =  z 
          in  (\mforall{}bnum:pv11\_p1\_Ballot\_Num().  \mforall{}p:\mBbbZ{}  \mtimes{}  Cmd.
                      ((<bnum,  p>  \mmember{}  accepted)  {}\mRightarrow{}  (\muparrow{}(pv11\_p1\_leq\_bnum(ldrs$_{uid}$)  bnum  bal\000Clot$_{num}$))))
                \mwedge{}  l-ordered(pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd;pv1,pv2.\muparrow{}(pv11\_p1\_leq\_bnum(ldrs$_{uid\000C}$)  (fst(pv1)) 
                                                                                                                          (fst(pv2)));accepted)
                \mwedge{}  no\_repeats(pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd;accepted))


By

---

Latex:
MemoryInvariant

---

Home Index