---

Step * of Lemma rsc4_pos_rounds

es:EO'. e1:E. Cmd:ValueAllType. n,round:.  (round  rsc4_NewRoundsState(Cmd) n(e1)  (0 z round))
BY
{ MemoryInvariant }

---

\mforall{}es:EO'.  \mforall{}e1:E.  \mforall{}Cmd:ValueAllType.  \mforall{}n,round:\mBbbZ{}.
    (round  \mmember{}  rsc4\_NewRoundsState(Cmd)  n(e1)  {}\mRightarrow{}  (\muparrow{}0  \mleq{}z  round))


By

---

MemoryInvariant



Home Index