---

Step * 2 1 3 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
5. x ∈ consensus-state3(V) List
6. y ∈ consensus-state3(V) List
7. v : V
8. cs-ref-map3(x) = Decided[v] ∈ consensus-state2(V)
⊢ Decided[v] (ts-rel(consensus-ts2(V))^*) cs-ref-map3(y)
BY
{ (BLemma `rel_star_weakening`
   THEN Auto
   THEN (RepUR ``consensus-ts2 ts-type`` 0
         THEN Auto
         THEN (FLemma `cs-ref-map3-decided` [-1] THENA Auto)
         THEN Symmetry
         THEN (BLemma `cs-ref-map3-decided`  THENA Auto)
         THEN Thin (-2))⋅) }

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
5. x ∈ consensus-state3(V) List
6. y ∈ consensus-state3(V) List
7. v : V
8. (COMMITED[v] ∈ x)
⊢ (COMMITED[v] ∈ y)

---

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
5.  x  \mmember{}  consensus-state3(V)  List
6.  y  \mmember{}  consensus-state3(V)  List
7.  v  :  V
8.  cs-ref-map3(x)  =  Decided[v]
\mvdash{}  Decided[v]  rel\_star(ts-type(consensus-ts2(V));  ts-rel(consensus-ts2(V)))  cs-ref-map3(y)


By

(BLemma  `rel\_star\_weakening`
  THEN  Auto
  THEN  (RepUR  ``consensus-ts2  ts-type``  0
              THEN  Auto
              THEN  (FLemma  `cs-ref-map3-decided`  [-1]  THENA  Auto)
              THEN  Symmetry
              THEN  (BLemma  `cs-ref-map3-decided`    THENA  Auto)
              THEN  Thin  (-2))\mcdot{})

---

Home Index