---

Step * 3 of Lemma cs-possible-state-reachable

.....wf..... 
1. V : Type
2. A : Id List
3. W : {a:Id| (a ∈ A)}  List List
4. v : V
5. 1 < ||W||
6. two-intersection(A;W)
7. L : {a:Id| (a ∈ A)}  List
8. s : ts-type(consensus-ts5(V;A;W))
⊢ ts-init(consensus-ts5(V;A;W)) (ts-rel(consensus-ts5(V;A;W))^*) s ∈ Type
BY
{ Auto }

---

Latex:


.....wf..... 
1.  V  :  Type
2.  A  :  Id  List
3.  W  :  \{a:Id|  (a  \mmember{}  A)\}    List  List
4.  v  :  V
5.  1  <  ||W||
6.  two-intersection(A;W)
7.  L  :  \{a:Id|  (a  \mmember{}  A)\}    List
8.  s  :  ts-type(consensus-ts5(V;A;W))
\mvdash{}  ts-init(consensus-ts5(V;A;W)) 
    (ts-rel(consensus-ts5(V;A;W))\^{}*) 
    s  \mmember{}  Type


By

Auto

---

Home Index