---

Step * 2 of Lemma consensus-refinement2


1. [V] : Type
2. x : ts-reachable(consensus-ts3(V))@i
3. y : ts-reachable(consensus-ts3(V))@i
4. x ts-rel(consensus-ts3(V)) y@i
⊢ ((λL.cs-ref-map3(L)) x) (ts-rel(consensus-ts2(V))^*) ((λL.cs-ref-map3(L)) y)
BY
{ Reduce 0 }

1
1. [V] : Type
2. x : ts-reachable(consensus-ts3(V))@i
3. y : ts-reachable(consensus-ts3(V))@i
4. x ts-rel(consensus-ts3(V)) y@i
⊢ cs-ref-map3(x) (ts-rel(consensus-ts2(V))^*) cs-ref-map3(y)

---

Latex:

---

Latex:

1.  [V]  :  Type
2.  x  :  ts-reachable(consensus-ts3(V))@i
3.  y  :  ts-reachable(consensus-ts3(V))@i
4.  x  ts-rel(consensus-ts3(V))  y@i
\mvdash{}  ((\mlambda{}L.cs-ref-map3(L))  x) 
    (ts-rel(consensus-ts2(V))\^{}*) 
    ((\mlambda{}L.cs-ref-map3(L))  y)


By

---

Latex:
Reduce  0

---

Home Index