---

Step * of Lemma rsc4_Notify_nlp

Cmd:ValueAllType. clients:bag(Id). x0:.  NormalLProgrammable'(Id  Message;rsc4_Notify(Cmd;clients) x0)
BY
{ RepeatFor 2 MaAuto }

---

\mforall{}Cmd:ValueAllType.  \mforall{}clients:bag(Id).  \mforall{}x0:\mBbbZ{}.
    NormalLProgrammable'(Id  \mtimes{}  Message;rsc4\_Notify(Cmd;clients)  x0)


By

---

RepeatFor  2  MaAuto



Home Index