---

Step * of Lemma rsc4_QuorumState_wf

[Cmd:ValueAllType]. (rsc4_QuorumState(Cmd)      EClass'(Cmd List  (Id List)))
BY
{ Try (Unfold `vatype` 0) THEN ProveWfLemma'' }

---

\mforall{}[Cmd:ValueAllType].  (rsc4\_QuorumState(Cmd)  \mmember{}  \mBbbZ{}  \mtimes{}  \mBbbZ{}  {}\mrightarrow{}  EClass'(Cmd  List  \mtimes{}  (Id  List)))


By

---

Try  (Unfold  `vatype`  0)  THEN  ProveWfLemma''



Home Index