---

Step * of Lemma consensus-message_wf

∀[V:Type]. ∀[A:Id List]. ∀[b:{a:Id| (a ∈ A)} ]. ∀[i:ℕ]. ∀[z:ℕi × V?].  (consensus-message(b;i;z) ∈ consensus-event(V;A))
BY
{ (RepUR ``consensus-message consensus-event`` 0 THEN Auto) }

---

Latex:


\mforall{}[V:Type].  \mforall{}[A:Id  List].  \mforall{}[b:\{a:Id|  (a  \mmember{}  A)\}  ].  \mforall{}[i:\mBbbN{}].  \mforall{}[z:\mBbbN{}i  \mtimes{}  V?].
    (consensus-message(b;i;z)  \mmember{}  consensus-event(V;A))


By

(RepUR  ``consensus-message  consensus-event``  0  THEN  Auto)

---

Home Index