---

Step * of Lemma rsc4_main_programmable

Cmd:ValueAllType. clients:bag(Id). cmdeq:EqDecider(Cmd). coeff,flrs:. locs:bag(Id).
  Programmable'(Id  Message;rsc4_Main)
BY
{ RepeatFor 2 MaAuto }

---

\mforall{}Cmd:ValueAllType.  \mforall{}clients:bag(Id).  \mforall{}cmdeq:EqDecider(Cmd).  \mforall{}coeff,flrs:\mBbbZ{}.  \mforall{}locs:bag(Id).
    Programmable'(Id  \mtimes{}  Message;rsc4\_Main)


By

---

RepeatFor  2  MaAuto



Home Index