---

Step * of Lemma rsc4_Voter_nlp

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

---

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


By

---

RepeatFor  2  MaAuto



Home Index