---

Step * of Lemma new_23_sig_quorum_inv_vote

∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e:E. ∀ni:ℤ × ℤ. ∀p:Cmd List × (Id List).
  (p ∈ new_23_sig_QuorumState(Cmd;notify;propose;f) ni(e)
  ⇒ let cmds,locs = p 
     in no_repeats(Id;locs)
        ∧ (||locs|| = ||cmds|| ∈ ℤ)
        ∧ (∀i:ℕ||locs||
             (↓∃e':E. ((e' <loc e) ∧ <<ni, cmds[i]>, locs[i]> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e')))))
BY
{ (MemoryInvariant
   THEN (Decide ⌜i = 0 ∈ ℤ⌝⋅ THENA Auto)
   THEN (RW ListC 0 THENA Auto)
   THEN AutoSplit
   THEN D 0
   THEN InstConcl [⌜e'⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}Cmd:ValueAllType.  \mforall{}notify,propose:Atom  List.  \mforall{}f:new\_23\_sig\_headers\_type\{i:l\}(Cmd;notify;propose).
\mforall{}es:EO+(Message(f)).  \mforall{}e:E.  \mforall{}ni:\mBbbZ{}  \mtimes{}  \mBbbZ{}.  \mforall{}p:Cmd  List  \mtimes{}  (Id  List).
    (p  \mmember{}  new\_23\_sig\_QuorumState(Cmd;notify;propose;f)  ni(e)
    {}\mRightarrow{}  let  cmds,locs  =  p 
          in  no\_repeats(Id;locs)
                \mwedge{}  (||locs||  =  ||cmds||)
                \mwedge{}  (\mforall{}i:\mBbbN{}||locs||
                          (\mdownarrow{}\mexists{}e':E
                                ((e'  <loc  e)
                                \mwedge{}  <<ni,  cmds[i]>,  locs[i]>  \mmember{}  new\_23\_sig\_vote'base(Cmd;notify;propose;f)(e')))))


By

---

Latex:
(MemoryInvariant
  THEN  (Decide  \mkleeneopen{}i  =  0\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (RW  ListC  0  THENA  Auto)
  THEN  AutoSplit
  THEN  D  0
  THEN  InstConcl  [\mkleeneopen{}e'\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index