---

Step * of Lemma rsc4_Replica_nlp

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

---

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


By

---

RepeatFor  2  MaAuto



Home Index