---

Step * of Lemma rsc4_Quorum_nlp

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

---

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


By

---

RepeatFor  2  MaAuto



Home Index