---

Step * of Lemma consensus-refinement2

∀[V:Type]. ts-refinement(consensus-ts2(V);consensus-ts3(V);λL.cs-ref-map3(L))
BY
{ (Auto THEN D 0 THEN Auto) }

1
1. [V] : Type
⊢ ts-init(consensus-ts2(V)) (ts-rel(consensus-ts2(V))^*) ((λL.cs-ref-map3(L)) ts-init(consensus-ts3(V)))

2
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)

3
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. ts-final(consensus-ts2(V)) x@i
⊢ ∃y:ts-reachable(consensus-ts3(V))
   ((ts-final(consensus-ts3(V)) y) ∧ (((λL.cs-ref-map3(L)) y) = x ∈ ts-type(consensus-ts2(V))))

---

Latex:


\mforall{}[V:Type].  ts-refinement(consensus-ts2(V);consensus-ts3(V);\mlambda{}L.cs-ref-map3(L))


By

(Auto  THEN  D  0  THEN  Auto)

---

Home Index