---

Step * 3 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. 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))))
BY
{ (RepUR ``ts-final consensus-ts2`` -1 THEN Reduce 0 THEN ExRepD THEN InstConcl [⌈[COMMITED[v]]⌉]⋅ THEN Auto) }

1
.....wf..... 
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
⊢ [COMMITED[v]] ∈ ts-reachable(consensus-ts3(V))

2
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
⊢ ts-final(consensus-ts3(V)) [COMMITED[v]]

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. v : V@i
5. x = Decided[v] ∈ consensus-state2(V)@i
6. ts-final(consensus-ts3(V)) [COMMITED[v]]
⊢ cs-ref-map3([COMMITED[v]]) = x ∈ ts-type(consensus-ts2(V))

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

---

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.  ts-final(consensus-ts2(V))  x@i
\mvdash{}  \mexists{}y:ts-reachable(consensus-ts3(V))
      ((ts-final(consensus-ts3(V))  y)  \mwedge{}  (((\mlambda{}L.cs-ref-map3(L))  y)  =  x))


By

(RepUR  ``ts-final  consensus-ts2``  -1
  THEN  Reduce  0
  THEN  ExRepD
  THEN  InstConcl  [\mkleeneopen{}[COMMITED[v]]\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index