---

Step * 1 of Lemma consensus-refinement2


1. [V] : Type
⊢ ts-init(consensus-ts2(V)) (ts-rel(consensus-ts2(V))^*) ((λL.cs-ref-map3(L)) ts-init(consensus-ts3(V)))
BY
{ (BLemma `rel_star_weakening`
   THEN Auto
   THEN RepUR ``consensus-ts2 consensus-ts3 ts-init ts-type cs-ref-map3 let`` 0
   THEN Auto) }

---

Latex:



1.  [V]  :  Type
\mvdash{}  ts-init(consensus-ts2(V)) 
    rel\_star(ts-type(consensus-ts2(V));  ts-rel(consensus-ts2(V))) 
    ((\mlambda{}L.cs-ref-map3(L))  ts-init(consensus-ts3(V)))


By

(BLemma  `rel\_star\_weakening`
  THEN  Auto
  THEN  RepUR  ``consensus-ts2  consensus-ts3  ts-init  ts-type  cs-ref-map3  let``  0
  THEN  Auto)

---

Home Index