---

Step * of Lemma new_23_sig_quorum_invariant

∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e1:E. ∀ni:ℤ × ℤ. ∀z:Cmd List × (Id List).
  (z ∈ new_23_sig_QuorumState(Cmd;notify;propose;f) ni(e1)
  ⇒ let cmds,locs = z 
     in no_repeats(Id;locs) ∧ (||locs|| = ||cmds|| ∈ ℤ))
BY
{ MemoryInvariant }

---

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{}e1:E.  \mforall{}ni:\mBbbZ{}  \mtimes{}  \mBbbZ{}.  \mforall{}z:Cmd  List  \mtimes{}  (Id  List).
    (z  \mmember{}  new\_23\_sig\_QuorumState(Cmd;notify;propose;f)  ni(e1)
    {}\mRightarrow{}  let  cmds,locs  =  z 
          in  no\_repeats(Id;locs)  \mwedge{}  (||locs||  =  ||cmds||))


By

---

Latex:
MemoryInvariant

---

Home Index