---

Step * of Lemma cs-rcv-vote_wf

∀[V:Type]. ∀[A:Id List]. ∀[a:{a:Id| (a ∈ A)} ]. ∀[i:ℕ]. ∀[v:V].  (Vote[a;i;v] ∈ consensus-rcv(V;A))
BY
{ (Unfolds ``cs-rcv-vote consensus-rcv`` 0 THEN Auto) }

---

Latex:


\mforall{}[V:Type].  \mforall{}[A:Id  List].  \mforall{}[a:\{a:Id|  (a  \mmember{}  A)\}  ].  \mforall{}[i:\mBbbN{}].  \mforall{}[v:V].    (Vote[a;i;v]  \mmember{}  consensus-rcv(V;A))


By

(Unfolds  ``cs-rcv-vote  consensus-rcv``  0  THEN  Auto)

---

Home Index