---

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


1. V : Type@i'
2. v1 : V@i
3. v2 : V@i
4. n : ℕ@i
5. ∃z:consensus-state1(V)
    (((Decided[v1] = UNDECIDED ∈ consensus-state1(V)) ∧ (∃v:V. (z = Decided[v] ∈ consensus-state1(V))))
    ∧ (z 
       λx,y. ((x = UNDECIDED ∈ consensus-state1(V)) ∧ (∃v:V. (y = Decided[v] ∈ consensus-state1(V))))^n - 1 
       Decided[v2]))@i
6. ¬(n = 0 ∈ ℤ)
⊢ v1 = v2 ∈ V
BY
{ (ExRepD THEN RepeatFor 4 (Thin (-1))) }

1
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

---

Latex:



1.  V  :  Type@i'
2.  v1  :  V@i
3.  v2  :  V@i
4.  n  :  \mBbbN{}@i
5.  \mexists{}z:consensus-state1(V)
        (((Decided[v1]  =  UNDECIDED)  \mwedge{}  (\mexists{}v:V.  (z  =  Decided[v])))
        \mwedge{}  (z 
              \mlambda{}x,y.  ((x  =  UNDECIDED)  \mwedge{}  (\mexists{}v:V.  (y  =  Decided[v])))\^{}n  -  1 
              Decided[v2]))@i
6.  \mneg{}(n  =  0)
\mvdash{}  v1  =  v2


By

(ExRepD  THEN  RepeatFor  4  (Thin  (-1)))

---

Home Index