---

Step * of Lemma consensus-ts3-invariant1

∀[V:Type]. ∀[L:ts-reachable(consensus-ts3(V))]. ∀[v:V].
  ∀[v':V]. v' = v ∈ V supposing (CONSIDERING[v'] ∈ L) ∨ (COMMITED[v'] ∈ L) 
  supposing (CONSIDERING[v] ∈ L) ∨ (COMMITED[v] ∈ L)
BY
{ RemoveUniform (Auto THEN Try ((D 2 THEN RepUR ``ts-type consensus-ts3`` 2 THEN Auto))) 
(Auto THEN Try ((D 2 THEN RepUR ``ts-type consensus-ts3`` 2 THEN Auto)))⋅ }

1
∀V:Type. ∀L:ts-reachable(consensus-ts3(V)). ∀v:V.
  (((CONSIDERING[v] ∈ L) ∨ (COMMITED[v] ∈ L))
  ⇒ (∀v':V. (((CONSIDERING[v'] ∈ L) ∨ (COMMITED[v'] ∈ L)) ⇒ (v' = v ∈ V))))

---

Latex:


\mforall{}[V:Type].  \mforall{}[L:ts-reachable(consensus-ts3(V))].  \mforall{}[v:V].
    \mforall{}[v':V].  v'  =  v  supposing  (CONSIDERING[v']  \mmember{}  L)  \mvee{}  (COMMITED[v']  \mmember{}  L) 
    supposing  (CONSIDERING[v]  \mmember{}  L)  \mvee{}  (COMMITED[v]  \mmember{}  L)


By

RemoveUniform  (Auto  THEN  Try  ((D  2  THEN  RepUR  ``ts-type  consensus-ts3``  2  THEN  Auto))) 
(Auto  THEN  Try  ((D  2  THEN  RepUR  ``ts-type  consensus-ts3``  2  THEN  Auto)))\mcdot{}

---

Home Index