---

Step * 2 1 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
⊢ cs-ref-map3(x) (ts-rel(consensus-ts2(V))^*) cs-ref-map3(y)
BY
{ ((Assert x ∈ consensus-state3(V) List BY
          (DVar `x' THEN All (RepUR ``ts-type consensus-ts3``) THEN Trivial))
   THEN (Assert y ∈ consensus-state3(V) List BY
               (DVar `y' THEN All (RepUR ``ts-type consensus-ts3``) THEN Trivial))
   THEN (InstLemma `consensus-state2-cases` [⌈V⌉;⌈cs-ref-map3(x)⌉]⋅ THENA Auto)
   THEN D -1
   THEN ExRepD
   THEN SplitOrHyps
   THEN (HypSubst' -1 0 THENA (Auto THEN RepUR ``ts-type consensus-ts2`` 0 THEN Auto))) }

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. cs-ref-map3(x) = AMBIVALENT ∈ consensus-state2(V)
⊢ AMBIVALENT (ts-rel(consensus-ts2(V))^*) cs-ref-map3(y)

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
5. x ∈ consensus-state3(V) List
6. y ∈ consensus-state3(V) List
7. v : V
8. cs-ref-map3(x) = PREDECIDED[v] ∈ consensus-state2(V)
⊢ PREDECIDED[v] (ts-rel(consensus-ts2(V))^*) cs-ref-map3(y)

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

---

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{}  cs-ref-map3(x)  rel\_star(ts-type(consensus-ts2(V));  ts-rel(consensus-ts2(V)))  cs-ref-map3(y)


By

((Assert  x  \mmember{}  consensus-state3(V)  List  BY
                (DVar  `x'  THEN  All  (RepUR  ``ts-type  consensus-ts3``)  THEN  Trivial))
  THEN  (Assert  y  \mmember{}  consensus-state3(V)  List  BY
                          (DVar  `y'  THEN  All  (RepUR  ``ts-type  consensus-ts3``)  THEN  Trivial))
  THEN  (InstLemma  `consensus-state2-cases`  [\mkleeneopen{}V\mkleeneclose{};\mkleeneopen{}cs-ref-map3(x)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  ExRepD
  THEN  SplitOrHyps
  THEN  (HypSubst'  -1  0  THENA  (Auto  THEN  RepUR  ``ts-type  consensus-ts2``  0  THEN  Auto)))

---

Home Index