---

Step * of Lemma rsc4_Notify_wf

[Cmd:ValueAllType]. [clients:bag(Id)].  (rsc4_Notify(Cmd;clients)    EClass'(Id  Message))
BY
{ Try (Unfold `vatype` 0) THEN ProveWfLemma'' }

---

\mforall{}[Cmd:ValueAllType].  \mforall{}[clients:bag(Id)].    (rsc4\_Notify(Cmd;clients)  \mmember{}  \mBbbZ{}  {}\mrightarrow{}  EClass'(Id  \mtimes{}  Message))


By

---

Try  (Unfold  `vatype`  0)  THEN  ProveWfLemma''



Home Index