---

Step * of Lemma rsc4_vote'msg_wf

[Cmd:ValueAllType]. [vote:    Cmd  Id].  (rsc4_vote'msg(Cmd;vote)  Message)
BY
{ ProveWfLemma' }

---

\mforall{}[Cmd:ValueAllType].  \mforall{}[vote:\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id].    (rsc4\_vote'msg(Cmd;vote)  \mmember{}  Message)


By

---

ProveWfLemma'



Home Index