---

Step * of Lemma rsc4_NewRoundsState_nlp

Cmd:ValueAllType. x0:.  NormalLProgrammable'(;rsc4_NewRoundsState(Cmd) x0)
BY
{ RepeatFor 2 MaAuto }

---

\mforall{}Cmd:ValueAllType.  \mforall{}x0:\mBbbZ{}.    NormalLProgrammable'(\mBbbZ{};rsc4\_NewRoundsState(Cmd)  x0)


By

---

RepeatFor  2  MaAuto



Home Index