---

Step * of Lemma rsc4_QuorumState_nlp

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

---

\mforall{}Cmd:ValueAllType.  \mforall{}x0:\mBbbZ{}  \mtimes{}  \mBbbZ{}.    NormalLProgrammable'(Cmd  List  \mtimes{}  (Id  List);rsc4\_QuorumState(Cmd)  x0)


By

---

RepeatFor  2  MaAuto



Home Index