---

Step * of Lemma cs-commited-equal

∀[V:Type]. ∀[v1,v:V].  uiff(COMMITED[v] = COMMITED[v1] ∈ consensus-state3(V);v = v1 ∈ V)
BY
{ Auto }

1
1. V : Type
2. v1 : V
3. v : V
4. COMMITED[v] = COMMITED[v1] ∈ consensus-state3(V)
⊢ v = v1 ∈ V

---

Latex:


\mforall{}[V:Type].  \mforall{}[v1,v:V].    uiff(COMMITED[v]  =  COMMITED[v1];v  =  v1)


By

Auto

---

Home Index