---

Step * 1 of Lemma consensus-refinement5


1. [V] : Type
2. A : Id List@i
3. W : {a:Id| (a ∈ A)}  List List@i
4. 1 < ||W||@i
5. two-intersection(A;W)@i
⊢ ts-init(consensus-ts5(V;A;W)) 
  (ts-rel(consensus-ts5(V;A;W))^*) 
  ((λs.cs-events-to-state(A; s)) ts-init(consensus-ts6(V;A;W)))
BY
{ ((RepUR ``consensus-ts6 consensus-ts5 ts-init ts-type ts-rel consensus-state4`` 0
    THEN RepUR ``cs-events-to-state consensus-state5 consensus-accum-state bfalse`` 0
    )
   THEN RepeatFor 2 (Auto)
   ) }

---

Latex:



1.  [V]  :  Type
2.  A  :  Id  List@i
3.  W  :  \{a:Id|  (a  \mmember{}  A)\}    List  List@i
4.  1  <  ||W||@i
5.  two-intersection(A;W)@i
\mvdash{}  ts-init(consensus-ts5(V;A;W)) 
    rel\_star(ts-type(consensus-ts5(V;A;W));  ts-rel(consensus-ts5(V;A;W))) 
    ((\mlambda{}s.cs-events-to-state(A;  s))  ts-init(consensus-ts6(V;A;W)))


By

((RepUR  ``consensus-ts6  consensus-ts5  ts-init  ts-type  ts-rel  consensus-state4``  0
    THEN  RepUR  ``cs-events-to-state  consensus-state5  consensus-accum-state  bfalse``  0
    )
  THEN  RepeatFor  2  (Auto)
  )

---

Home Index