---

Step * of Lemma new_23_sig_quorum_fseg

∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e1,e2:E. ∀ni:ℤ × ℤ. ∀zh,z:Cmd List × (Id List).
  ((e1 <loc e2)
  ⇒ zh ∈ new_23_sig_QuorumState(Cmd;notify;propose;f) ni(e1)
  ⇒ z ∈ new_23_sig_QuorumState(Cmd;notify;propose;f) ni(e2)
  ⇒ let cmds1,locs1 = zh 
     in let cmds2,locs2 = z 
        in fseg(Cmd;cmds1;cmds2) ∧ fseg(Id;locs1;locs2))
BY
{ MemoryOrdering⋅ }

---

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,e2:E.  \mforall{}ni:\mBbbZ{}  \mtimes{}  \mBbbZ{}.  \mforall{}zh,z:Cmd  List  \mtimes{}  (Id  List).
    ((e1  <loc  e2)
    {}\mRightarrow{}  zh  \mmember{}  new\_23\_sig\_QuorumState(Cmd;notify;propose;f)  ni(e1)
    {}\mRightarrow{}  z  \mmember{}  new\_23\_sig\_QuorumState(Cmd;notify;propose;f)  ni(e2)
    {}\mRightarrow{}  let  cmds1,locs1  =  zh 
          in  let  cmds2,locs2  =  z 
                in  fseg(Cmd;cmds1;cmds2)  \mwedge{}  fseg(Id;locs1;locs2))


By

---

Latex:
MemoryOrdering\mcdot{}

---

Home Index