---

Step * of Lemma rsc4_Round_nlp

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

---

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


By

---

RepeatFor  2  MaAuto



Home Index