---

Step * 1 1 of Lemma consensus-ts3-invariant1


1. V : Type@i'
2. v : V@i
3. (CONSIDERING[v] ∈ ts-init(consensus-ts3(V))) ∨ (COMMITED[v] ∈ ts-init(consensus-ts3(V)))@i
4. v' : V@i
5. (CONSIDERING[v'] ∈ ts-init(consensus-ts3(V))) ∨ (COMMITED[v'] ∈ ts-init(consensus-ts3(V)))@i
⊢ v' = v ∈ V
BY
{ (RepUR ``consensus-ts3 ts-init`` -1 THEN D -1 THEN Auto) }

---

Latex:



1.  V  :  Type@i'
2.  v  :  V@i
3.  (CONSIDERING[v]  \mmember{}  ts-init(consensus-ts3(V)))  \mvee{}  (COMMITED[v]  \mmember{}  ts-init(consensus-ts3(V)))@i
4.  v'  :  V@i
5.  (CONSIDERING[v']  \mmember{}  ts-init(consensus-ts3(V)))  \mvee{}  (COMMITED[v']  \mmember{}  ts-init(consensus-ts3(V)))@i
\mvdash{}  v'  =  v


By

(RepUR  ``consensus-ts3  ts-init``  -1  THEN  D  -1  THEN  Auto)

---

Home Index