---

Step * of Lemma committed-inning0-reachable

∀[V:Type]. ∀[A:Id List]. ∀[W:{a:Id| (a ∈ A)}  List List].
  ∀[v:V]. (λa.<0, 0 : v> ∈ ts-reachable(consensus-ts4(V;A;W))) supposing ||W|| ≥ 1 
BY
{ (Auto
   THEN RepUR ``consensus-ts4 ts-reachable ts-init ts-rel ts-type`` 0
   THEN MemTypeCD
   THEN Auto
   THEN Try ((RepUR ``consensus-state4`` 0 THEN Complete (Auto)))) }

1
.....set predicate..... 
1. V : Type
2. A : Id List
3. W : {a:Id| (a ∈ A)}  List List
4. ||W|| ≥ 1 
5. v : V
⊢ (λa.<-1, ⊗>) ((λx,y. CR[x,y])^*) (λa.<0, 0 : v>)

---

Latex:


\mforall{}[V:Type].  \mforall{}[A:Id  List].  \mforall{}[W:\{a:Id|  (a  \mmember{}  A)\}    List  List].
    \mforall{}[v:V].  (\mlambda{}a.ɘ,  0  :  v>  \mmember{}  ts-reachable(consensus-ts4(V;A;W)))  supposing  ||W||  \mgeq{}  1 


By

(Auto
  THEN  RepUR  ``consensus-ts4  ts-reachable  ts-init  ts-rel  ts-type``  0
  THEN  MemTypeCD
  THEN  Auto
  THEN  Try  ((RepUR  ``consensus-state4``  0  THEN  Complete  (Auto))))

---

Home Index