---

Step * 1 of Lemma cs-commited-equal


1. V : Type
2. v1 : V
3. v : V
4. COMMITED[v] = COMMITED[v1] ∈ consensus-state3(V)
⊢ v = v1 ∈ V
BY
{ (RepUR ``cs-commited consensus-state3`` -1 THEN Auto) }

---

Latex:



1.  V  :  Type
2.  v1  :  V
3.  v  :  V
4.  COMMITED[v]  =  COMMITED[v1]
\mvdash{}  v  =  v1


By

(RepUR  ``cs-commited  consensus-state3``  -1  THEN  Auto)

---

Home Index