---

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


1. V : Type@i'
2. v1 : V@i
3. v2 : V@i
4. n : ℕ@i
5. λx,y. ((x = UNDECIDED ∈ consensus-state1(V)) ∧ (∃v:V. (y = Decided[v] ∈ consensus-state1(V))))^n Decided[v1] 
   Decided[v2]@i
⊢ v1 = v2 ∈ V
BY
{ (RecUnfold `rel_exp` (-1) THEN (SplitOnHypITE -1  THENA Auto) THEN All Reduce) }

1
1. V : Type@i'
2. v1 : V@i
3. v2 : V@i
4. n : ℕ@i
5. Decided[v1] = Decided[v2] ∈ consensus-state1(V)@i
6. n = 0 ∈ ℤ
⊢ v1 = v2 ∈ V

2
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

---

Latex:



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


By

(RecUnfold  `rel\_exp`  (-1)  THEN  (SplitOnHypITE  -1    THENA  Auto)  THEN  All  Reduce)

---

Home Index