---

Step * 3 4 of Lemma consensus-refinement2


1. V : Type
2. ∀x,y:ts-reachable(consensus-ts3(V)).
     ((x ts-rel(consensus-ts3(V)) y) ⇒ (((λL.cs-ref-map3(L)) x) (ts-rel(consensus-ts2(V))^*) ((λL.cs-ref-map3(L)) y)))
3. x : ts-reachable(consensus-ts2(V))@i
4. v : V@i
5. x = Decided[v] ∈ consensus-state2(V)@i
6. y : ts-reachable(consensus-ts3(V))
7. ts-final(consensus-ts3(V)) y
⊢ cs-ref-map3(y) ∈ ts-type(consensus-ts2(V))
BY
{ (D -2 THEN (RepUR ``consensus-ts2 ts-type`` 0 THEN Auto) THEN RepUR ``consensus-ts3 ts-type`` -3 THEN Auto) }

---

Latex:



1.  V  :  Type
2.  \mforall{}x,y:ts-reachable(consensus-ts3(V)).
          ((x  ts-rel(consensus-ts3(V))  y)
          {}\mRightarrow{}  (((\mlambda{}L.cs-ref-map3(L))  x)  (ts-rel(consensus-ts2(V))\^{}*)  ((\mlambda{}L.cs-ref-map3(L))  y)))
3.  x  :  ts-reachable(consensus-ts2(V))@i
4.  v  :  V@i
5.  x  =  Decided[v]@i
6.  y  :  ts-reachable(consensus-ts3(V))
7.  ts-final(consensus-ts3(V))  y
\mvdash{}  cs-ref-map3(y)  \mmember{}  ts-type(consensus-ts2(V))


By

(D  -2
  THEN  (RepUR  ``consensus-ts2  ts-type``  0  THEN  Auto)
  THEN  RepUR  ``consensus-ts3  ts-type``  -3
  THEN  Auto)

---

Home Index