---

Step * 1 1 2 1 of Lemma consensus-safety


∀V:Type. ∀v1,v2:V.
  ((Decided[v1] 
    ((λx,y. ((x = UNDECIDED ∈ consensus-state1(V)) ∧ (∃v:V. (y = Decided[v] ∈ consensus-state1(V)))))^*) 
    Decided[v2])
  ⇒ (v1 = v2 ∈ V))
BY
{ (Auto THEN RepUR ``infix_ap rel_star`` -1 THEN D -1) }

1
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

---

Latex:



\mforall{}V:Type.  \mforall{}v1,v2:V.
    ((Decided[v1]  ((\mlambda{}x,y.  ((x  =  UNDECIDED)  \mwedge{}  (\mexists{}v:V.  (y  =  Decided[v]))))\^{}*)  Decided[v2])  {}\mRightarrow{}  (v1  =  v2))


By

(Auto  THEN  RepUR  ``infix\_ap  rel\_star``  -1  THEN  D  -1)

---

Home Index