---

Step * of Lemma one-consensus-event_wf

∀[V:Type]. ∀[A:Id List]. ∀[a:{a:Id| (a ∈ A)} ]. ∀[e:consensus-event(V;A)]. ∀[x,y:consensus-state6(V;A)].
  (y = x after e@a ∈ ℙ)
BY
{ ProveWfLemma }

---

Latex:


\mforall{}[V:Type].  \mforall{}[A:Id  List].  \mforall{}[a:\{a:Id|  (a  \mmember{}  A)\}  ].  \mforall{}[e:consensus-event(V;A)].
\mforall{}[x,y:consensus-state6(V;A)].
    (y  =  x  after  e@a  \mmember{}  \mBbbP{})


By

ProveWfLemma

---

Home Index