---

Step * of Lemma rsc4_increasing_rounds

es:EO'. e1,e2:E. Cmd:ValueAllType. n,round1,round2:.
  ((e1 <loc e2)
   round1  rsc4_NewRoundsState(Cmd) n(e1)
   round2  rsc4_NewRoundsState(Cmd) n(e2)
   (round1 z round2))
BY
{ MemoryOrdering }

---

\mforall{}es:EO'.  \mforall{}e1,e2:E.  \mforall{}Cmd:ValueAllType.  \mforall{}n,round1,round2:\mBbbZ{}.
    ((e1  <loc  e2)
    {}\mRightarrow{}  round1  \mmember{}  rsc4\_NewRoundsState(Cmd)  n(e1)
    {}\mRightarrow{}  round2  \mmember{}  rsc4\_NewRoundsState(Cmd)  n(e2)
    {}\mRightarrow{}  (\muparrow{}round1  \mleq{}z  round2))


By

---

MemoryOrdering



Home Index