---

Step * 1 1 2 1 1 2 1 of Lemma consensus-safety


1. V : Type@i'
2. v1 : V@i
3. v2 : V@i
4. n : ℕ@i
5. z : consensus-state1(V)@i
6. Decided[v1] = UNDECIDED ∈ consensus-state1(V)@i
⊢ v1 = v2 ∈ V
BY
{ (RepUR ``cs-decided cs-undecided consensus-state1`` -1 THEN Auto) }

---

Latex:



1.  V  :  Type@i'
2.  v1  :  V@i
3.  v2  :  V@i
4.  n  :  \mBbbN{}@i
5.  z  :  consensus-state1(V)@i
6.  Decided[v1]  =  UNDECIDED@i
\mvdash{}  v1  =  v2


By

(RepUR  ``cs-decided  cs-undecided  consensus-state1``  -1  THEN  Auto)

---

Home Index